Changeset 3639


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

more fiddling

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

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/conclusions.tex

    r3638 r3639  
    3434The 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.
    3535This 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
     36
     37\paragraph{Vision}
     38
     39We 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.
     40With 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}.
     41
     42The 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.
     43In cases where our approach produces overly complex cost models, safe approximations can be used to trade complexity for precision.
     44
     45Finally, 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.
    3646
    3747\subsection{Related work}
  • Papers/jar-cerco-2017/introduction.tex

    r3638 r3639  
    5757In 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.
    5858
    59 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}.
    60 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.
    61 
    62 To establish that our approach works, and scales beyond `toy' languages to more realistic programming languages, we have implemented a compiler using this technique.
     59The 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.
     60This 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.
     61However, 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.
     62
     63Accordingly, 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}.
     64To 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.
     65
     66To 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.
    6367The \emph{CerCo verified C compiler} compiles the CerCo C language fragment to object binaries for the MCS-51 8-bit embedded microcontroller.
    6468This is a well-known and still popular processor in the embedded systems community.
    65 Our compiler lifts a cost-model induced on machine code that it produces, back through the compilation chain, to the source-level.
     69Our 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.
    6670At 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.
    6771These annotations may be used by the programmer to predict concrete execution time and stack space usage.
     
    7680The compiler is verified using the Matita interactive theorem prover, an implementation of the Calculus of Coinductive Constructions, developed at the University of Bologna.
    7781
    78 \paragraph{Vision.}
    79 
    80 
    81 We envision a new generation of compilers that track program structure through
    82 compilation and optimisation and exploit this information to define a precise,
    83 non-uniform cost model for source code that accounts for runtime state. With
    84 such a cost model we can perform non-functional verification in a similar way
    85 to functional verification and exploit the state of the art in automated
    86 high-level verification~\cite{survey}.
    87 
    88 The techniques currently used by the Worst Case Execution Time (WCET) community,
    89 which perform analysis on object code, are still applicable but can be coupled
    90 with additional source-level analysis. In cases where our approach produces
    91 overly complex cost models, safe approximations can be used to trade complexity
    92 for precision.
    93 
    94 Finally, source code analysis can be used early in the development process,
    95 when components have been specified but not implemented, as modularity means
    96 that it is enough to specify the non-functional behaviour of missing components.
    97 
    98 \subsection{The CerCo approach}
    99 
    100 In CerCo we propose a radically new approach to the problem: we reject the idea
    101 of a uniform cost model and we propose that the compiler, which knows how the
    102 code is translated, must return the cost model for basic blocks of high level
    103 instructions. It must do so by keeping track of the control flow modifications
    104 to reverse them and by interfacing with processor timing analysis.
     82\subsection{The CerCo approach, in more detail}
     83
     84As mentioned above, in CerCo we reject the idea of a uniform (compositional) cost model for a high-level programming language.
     85We view any uniform  cost model as being hopelessly imprecise, as modern compilers themselves are highly non-compositional in their translations.
     86Far 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.
     87To 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.
    10588
    10689By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
Note: See TracChangeset for help on using the changeset viewer.