Changeset 3639

Ignore:
Timestamp:
Mar 8, 2017, 1:01:44 PM (5 months ago)
Message:

more fiddling

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
 r3638 The techniques that we have presented are not tied to any particular programming language, and are in fact amenable to arbitrary imperative and functional programming languages. This last claim is bolstered by a pen-and-paper proof of the correctness of the labelling approach applied to a toy' compiler for an applicative language. %cite \paragraph{Vision} 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 perform non-functional verification in a similar way to functional verification 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 perform analysis on object code, are still applicable but can be coupled with additional source-level analysis. In cases where our approach produces overly complex cost models, safe approximations can be used to trade complexity for 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. \subsection{Related work}
 r3638 In this paper, we report on the scientific and technical contributions of the Certified Complexity (CerCo') project~\cite{cerco}, an EU FET-Open funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7. We first present a uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is based on early versions of \emph{CompCert C}~\cite{compcert}. To define this cost model, we have developed a technical device, which we have dubbed \emph{the labelling approach}~\cite{labelling}, a technique to implement compilers that induce cost models on source programs by a very lightweight tracking of code changes through the compilation pipeline. To establish that our approach works, and scales beyond toy' languages to more realistic programming languages, we have implemented a compiler using this technique. The central insight of the CerCo project is that a cost model for a high-level programming language can be defined using a compiler's implicit knowledge of how expressions and statements are translated to machine code. This implicit knowledge of how a compiler translates source-language phrases has to date been largely ignored when designing static analysis tools for concrete complexity measures. However, by embracing the compilation process itself, one is able to define a non-uniform (non-compositional) cost model that is customised to the exact translation process that was subjected to the source-language program by the compiler. Accordingly, we first present a non-uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is based on early versions of \emph{CompCert C}~\cite{compcert}. To define this cost model, we have developed a technical device---dubbed \emph{the labelling approach}~\cite{labelling}---which is a technique to implement compilers that induce cost models on source programs by a very lightweight tracking of code changes through the compilation pipeline. To establish that this tracking works, and scales beyond toy' languages to more realistic programming languages, we have implemented a lightly-optimising compiler employing this technique. The \emph{CerCo verified C compiler} compiles the CerCo C language fragment to object binaries for the MCS-51 8-bit embedded microcontroller. This is a well-known and still popular processor in the embedded systems community. Our compiler lifts a cost-model induced on machine code that it produces, back through the compilation chain, to the source-level. Our compiler lifts a cost-model induced on the machine code that it produces, back through the compilation chain, to the source-level, making use of the labelling approach to effect the tracking and lifting. At the source level, this cost model is made manifest as parametric cost-annotations, inserted into the original source code file of the program being compiled. These annotations may be used by the programmer to predict concrete execution time and stack space usage. The compiler is verified using the Matita interactive theorem prover, an implementation of the Calculus of Coinductive Constructions, developed at the University of Bologna. \paragraph{Vision.} 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 perform non-functional verification in a similar way to functional verification 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 perform analysis on object code, are still applicable but can be coupled with additional source-level analysis. In cases where our approach produces overly complex cost models, safe approximations can be used to trade complexity for 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. \subsection{The CerCo approach} In CerCo we propose a radically new approach to the problem: we reject the idea of a uniform cost model and we propose that the compiler, which knows how the code is translated, must return the cost model for basic blocks of high level instructions. It must do so by keeping track of the control flow modifications to reverse them and by interfacing with processor timing analysis. \subsection{The CerCo approach, in more detail} As mentioned above, in CerCo we reject the idea of a uniform (compositional) cost model for a high-level programming language. We view any uniform  cost model as being hopelessly imprecise, as modern compilers themselves are highly non-compositional in their translations. Far better is to try to engineer the compiler---which knows how the code is translated---to return the cost model for basic blocks of high level instructions. To do this, the compiler must track modifications to the control flow of the program, in order to reverse them, and interface with a processor timing analysis. By embracing compilation, instead of avoiding it like EmBounded did, a CerCo