Changeset 3453 for Papers

Timestamp:

Feb 20, 2014, 12:38:06 PM (5 years ago)

Author:

mulligan

Message:

reworking up to Section 2

File:

• Papers/fopara2013/fopara13.tex (modified) (4 diffs)

Papers/fopara2013/fopara13.tex

@@ -98 +98 @@
 the development of a technique for analysing non-functional
 properties of programs (time, space) at the source level, with little or no loss of accuracy,
-and with a small trusted code base. We developed a certified compiler that translates C source code to object code, producing a copy of the source code instrumented with cost annotations as an additional side-effect. These instrumentations expose at
+and with a small trusted code base. We developed a certified compiler that translates C source code to object code, producing a copy of the source code embellished with cost annotations as an additional side-effect. These annotations expose at
 the source level---and track precisely---the actual (non-asymptotic)
 computational cost of the input program. Untrusted invariant generators and trusted theorem provers
@@ -124 +124 @@
 but these analyses may then need information 
 about the high-level functional behaviour of the program that must then be reconstructed.
-
-The analysis of non-functional constraints on low-level object code presents several problems:
-\begin{enumerate}
+This analysis on low-level object code has several problems:
+\begin{itemize*}
 \item
-It can be hard to deduce the high-level structure of the program in the presence of compiler optimisations.
+It can be hard to deduce the high-level structure of the program after compiler optimisations.
 The object code produced by an optimising compiler may have radically different control flow to the original source code program.
 \item
-Techniques that operate on object code are not useful early in the development cycle of a program, yet problems with a program's design or implementation are cheaper to resolve earlier rather than later.
+Techniques that operate on object code are not useful early in the development process of a program, yet problems with a program's design or implementation are cheaper to resolve earlier in the process, rather than later.
 \item
 Parametric cost analysis is very hard: how can we reflect a cost that depends on the execution state, for example the 
@@ -138 +137 @@
 \item
 Performing functional analyses on object code makes it hard for the programmer to provide information about the program and its expected execution, leading to a loss of precision in the resulting analyses.
-\end{enumerate}
-
+\end{itemize*}
 \paragraph{Vision and approach.}
- We want to reconcile functional and 
+We wish to reconcile functional and 
 non-functional analyses: to share information and perform both at the same time 
-on source code.
+on high-level source code.
 %
 What has previously prevented this approach is the lack of a uniform and precise 
-cost model for high-level code: 1) each statement occurrence is compiled 
-differently and optimisations may change control flow; 2) the cost of an object 
+cost model for high-level code as each statement occurrence is compiled 
+differently, optimisations may change control flow, and the cost of an object 
 code instruction may depend on the runtime state of hardware components like 
 pipelines and caches, all of which are not visible in the source code.
 
-To solve the issue, we envision a new generation of compilers able to keep track 
-of program structure through compilation and optimisation, and to exploit that 
-information to define a cost model for source code that is precise, non-uniform, 
-and which accounts for runtime state. With such a source-level cost model we can 
+We envision a new generation of compilers that track program structure through compilation and optimisation and exploit this 
+information to define a precise, non-uniform cost model for source code that accounts for runtime state. With such a cost model we can 
 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, who perform analyses 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. 
-Finally, source code analysis can be used during the early stages of development, when 
-components have been specified but not implemented: source code modularity means 
-that it is enough to specify the non-functional behaviour of unimplemented 
+are still available but can be coupled with additional source-level 
+analyses. Where our approach produces overly complex cost models, safe approximations can be used to trade complexity with precision. 
+Finally, source code analysis can be used early in the development process, when 
+components have been specified but not implemented, as modularity means 
+that it is enough to specify the non-functional behaviour of missing 
 components.
-
 \paragraph{Contributions.}
-We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a 
+We have developed \emph{the labelling approach}~\cite{labelling}, a 
 technique to implement compilers that induce cost models on source programs by 
 very lightweight tracking of code changes through compilation. We have studied 
-how to formally prove the correctness of compilers implementing this technique. 
-We have implemented such a compiler from C to object binaries for the MCS-51 
-micro-controller for predicting execution time and stack space usage,
-and verified it in an interactive theorem prover.  As we are targeting
-an embedded micro-controller we do not consider dynamic memory allocation.
+how to formally prove the correctness of compilers implementing this technique, and
+have implemented such a compiler from C to object binaries for the MCS-51 
+microcontroller for predicting execution time and stack space usage,
+verifying it in an interactive theorem prover.  As we are targeting
+an embedded microcontroller we do not consider dynamic memory allocation.
 
 To demonstrate source-level verification of costs we have implemented
-a Frama-C plugin \cite{framac} that invokes the compiler on a source
-program and uses this to generate invariants on the high-level source
+a Frama-C plugin~\cite{framac} that invokes the compiler on a source
+program and uses it to generate invariants on the high-level source
 that correctly model low-level costs. The plugin certifies that the
 program respects these costs by calling automated theorem provers, a
@@ -187 +181 @@
 
 \section{Project context and approach}
-Formal methods for the verification of functional properties of programs have 
-now reached a level of maturity and automation that is facilitating a slow but 
-increasing adoption in production environments. For safety critical code, it is 
+Formal methods for the verification of functional properties of programs are now sufficiently mature to find increasing application in production environments. For safety critical code, it is 
 becoming commonplace to combine rigorous software engineering methodologies and testing 
 with static analysis, taking the strong points of each approach and mitigating