Changeset 3417

Timestamp:

Feb 10, 2014, 11:47:15 AM (6 years ago)

Author:

campbell

Message:

Many of the minor reviewer comments about FOPARA paper.

Location:

Papers/fopara2013

Files:

• appendix.tex (added)
• fopara13.tex (modified) (14 diffs)

Papers/fopara2013/fopara13.tex

@@ -146 +146 @@
 reduce non-functional verification to the functional case and exploit the state 
 of the art in automated high-level verification~\cite{survey}. The techniques 
-currently used by the Worst Case Execution Time (WCET) community, which performs its analysis on object code 
-, are still available but can now be coupled with an additional source-level 
+currently used by the Worst Case Execution Time (WCET) community, which perform the analysis on object code,
+are still available but can now be coupled with an additional source-level 
 analysis. Where the approach produces precise cost models too complex to reason 
 about, safe approximations can be used to trade complexity with precision. 
@@ -315 +315 @@
 base is an off-the-shelf invariant generator which, in turn, can be proved 
 correct using an interactive theorem prover. Therefore we achieve the double 
-objective of allowing the use more off-the-shelf components (e.g. provers and 
+objective of allowing the use of more off-the-shelf components (e.g. provers and 
 invariant generators) whilst reducing the trusted code base at the same time.
 
@@ -419 +419 @@
 \end{tabular}
 \caption{On the left: code to count the array's elements
- that are greater or equal to the treshold. On the right: CerCo's interaction
+ that are less than or equal to the treshold. On the right: CerCo's interaction
  diagram. CerCo's components are drawn solid.}
 \label{test1}
@@ -594 +594 @@
 % set of requirements will be added later.
 
-The third component is a static object code analyser. It takes in input a labeled
+The third component is a static object code analyser. It takes as input a labeled
 object code and it computes the scope of each of its label emission statements,
 i.e.\ the tree of instructions that may be executed after the statement and before
@@ -642 +642 @@
 loop optimisations like peeling or unrolling are prevented. Moreover, precision 
 of the object code labeling is not sufficient \emph{per se} to obtain global 
-precision: we also implicitly assumed the static analysis to be able to 
-associate a precise constant cost to every instruction. This is not possible in 
+precision: we implicitly assumed that a precise constant cost can be assigned
+to every instruction. This is not possible in 
 the presence of stateful hardware whose state influences the cost of operations, 
 like pipelines and caches. In the next subsection we will see an extension of the 
@@ -662 +662 @@
 scopes.
 
-Phases 1, 2 and 3 can be applied as well to logic languages (e.g. Prolog). 
-However, the instrumentation phase cannot: in standard Prolog there is no notion 
-of (global) variable whose state is not retracted during backtracking. 
-Therefore, the cost of executing computations that are later backtracked would 
-not be correctly counted in. Any extension of logic languages with 
-non-backtrackable state could support our labeling approach.
+% Brian: one of the reviewers pointed out that standard Prolog implementations
+% do have some global state that apparently survives backtracking and might be
+% used.  As we haven't experimented with this, I think it's best to elide it
+% entirely.
+
+% Phases 1, 2 and 3 can be applied as well to logic languages (e.g. Prolog). 
+% However, the instrumentation phase cannot: in standard Prolog there is no notion 
+% of (global) variable whose state is not retracted during backtracking. 
+% Therefore, the cost of executing computations that are later backtracked would 
+% not be correctly counted in. Any extension of logic languages with 
+% non-backtrackable state could support our labeling approach.
 
 \subsection{Dependent labeling}
@@ -710 +715 @@
 in a simple data structure. For example, to handle simple but realistic 
 pipelines it is sufficient to remember a short integer that encodes the position 
-of bubbles (stuck instructions) in the pipeline. In any case, the user does not 
-need to understand the meaning of the state to reason over the properties of the 
-program. Moreover, at any moment the user or the invariant generator tools that 
-analyse the instrumented source code produced by the compiler can decide to 
-trade precision of the analysis with simplicity by approximating the parametric 
+of bubbles (stuck instructions) in the pipeline. In any case, it is not necessary
+for the user to understand the meaning of the state to reason over the properties
+of the 
+program. Moreover, at any moment the user, or the invariant generator tools that 
+analyse the instrumented source code produced by the compiler, can decide to 
+trade precision of the analysis for simplicity by approximating the parametric 
 cost with safe non parametric bounds. Interestingly, the functional analysis of 
 the code can determine which blocks are executed more frequently in order to 
@@ -728 +734 @@
 taking more time.
 
-By introducing a variable that keep tracks of the iteration number, we can 
+By introducing a variable that keeps track of the iteration number, we can 
 associate to the label a cost that is a function of the iteration number. The 
 same technique works for loop unrolling without modifications: the function will 
@@ -742 +748 @@
 We review the cost synthesis techniques developed in the project.
 The starting hypothesis is that we have a certified methodology to annotate 
-blocks in the source code with constants which provide a sound and possibly 
+blocks in the source code with constants which provide a sound and sufficiently
 precise upper bound on the cost of executing the blocks after compilation to 
 object code.
@@ -772 +778 @@
 We developed the CerCo Cost plugin for the Frama-C platform as a proof of 
 concept of an automatic environment exploiting the cost annotations produced by 
-the CerCo compiler. It consists of an OCaml program which in first approximation 
+the CerCo compiler. It consists of an OCaml program which essentially
 takes the following actions: 1) it receives as input a C program, 2) it 
 applies the CerCo compiler to produce a related C program with cost annotations, 
@@ -799 +805 @@
 analysis of the VCs associated with branching may lead to a complexity blow up.
 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
-synchronous systems, with the language coming with a compiler to C. We designed a 
+synchronous systems, with a compiler which targets C. We designed a 
 wrapper for supporting Lustre files.
 The C function produced by the compiler implements the step function of the 
@@ -907 +913 @@
 compilation and external calls. Adding them is a transparent 
 process to the labeling approach and should create no unknown problem.
-\item We target an 8-bit processor. Targeting an 8-bit processor requires 
+\item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. Targeting an 8-bit processor requires 
 several changes and increased code size, but it is not fundamentally more 
 complex. The proof of correctness, however, becomes much harder.
@@ -968 +974 @@
 that is computed by the compiler.
 
-The statement that we formally proved is that for each C run with a measurable 
-sub-run there exists an object code run with a sub-run such that the observables 
+The statement that we formally proved is: for each C run with a measurable 
+sub-run, there exists an object code run with a sub-run, such that the observables 
 of the pairs of prefixes and sub-runs are the same and the time spent by the 
 object code in the sub-run is the same as the one predicted on the source code 
@@ -994 +1000 @@
 not I/O times, as it should be. 
 
-\section{Future work}
+\section{Conclusions and future work}
 
 All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}.