Changeset 3636


Ignore:
Timestamp:
Mar 8, 2017, 12:03:20 PM (2 weeks ago)
Author:
mulligan
Message:

more rewriting, fiddling, rephrasing etc.

File:
1 edited

Legend:

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

    r3635 r3636  
    2121A program's non-functional constraints may be given \emph{concretely}, or \emph{asymptotically}.
    2222Asymptotic complexity, as every Computer Science undergraduate knows, is important---but so too is concrete complexity for many applications, including the three we highlighted above as examples.
    23 A real-time system's response time is measured in seconds, milliseconds, or some other fundamental unit of time; a cryptographic library must have all execution paths execute in the same number of processor cycles, independent of any input passed by the client; and the size of an embedded controller for a pacemaker is measured in bits, bytes, or some other unit of memory capacity.
    24 In all cases, resource consumption is measured in some basal, concrete unit of measure.
     23A real-time system's response time is measured in seconds, milliseconds, or some other fundamental unit of time; a cryptographic library must have all execution paths execute in the same number of processor cycles, independent of any input passed by the client; and the size of an embedded controller for a pacemaker is measured in bits, bytes, or some other unit of computer memory capacity.
     24In all cases, resource consumption is measured (and is specified) in some basal, concrete unit of measure.
    2525
    2626Currently, a program's functional properties can be established by combining user annotations---preconditions, invariants, and so on---with various automated and semi-automated analyses---invariant generators, type systems, abstract interpretations, applications of theorem proving, and so on---on the high-level source code of the program.
    27 Functional properties of a program are therefore established by reasoning about the source code that the application programmer actually sees.
     27Functional properties of a program are therefore established by reasoning about the source code that the application programmer actually sees and writes.
    2828Further, the results of any analysis can be communicated to the programmer in terms of abstractions, control flow, and an overall system design that they are familiar with.
    2929
    30 By contrast, a program's non-functional properties are established by reasoning on low-level object code produced not by a programmer, but by a compiler.
     30By contrast, a program's concrete, non-functional properties are established by reasoning on low-level object code produced not by a programmer, but by a compiler.
    3131Whilst analyses operating at this level can and do produce very accurate results---Worst Case Execution Time (WCET) analysis can be extraordinarily accurate, for example---analysis at such a low-level of abstraction invariably has disadvantages:
    3232\begin{itemize}
     
    4848\end{itemize}
    4949
    50 More ideal would be a combination of high-level reasoning coupled with the accuracy one would expect of WCET, or other static analyses of non-functional properties.
    51 This paper presents such a combination.
    52 
    53 What has previously prevented high-level reasoning about non-functional properties is the lack of a uniform and precise cost model for programs written in programming languages like C.
     50More ideal would be a high-level analysis of concrete, non-functional properties, coupled with the accuracy one would expect of e.g. existing WCET analysers.
     51This would lead to a reconciliation of functional and non-functional analyses.
     52Information could be shared between the two analyses, and both could be performed concurrently on the same high-level source code.
     53
     54What has previously prevented high-level reasoning about non-functional properties is the lack of a uniform and precise cost model for programs written in programming languages, such as C.
    5455Since modern compilers---as discussed previously---may compile each expression and statement occurrence in radically different ways, 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, none of which are visible in the source code, it has not been clear how one could go about defining such a cost model.
    5556
     57In this paper, we report on the scientific and technical contributions of the Certified Complexity (`CerCo') project, an EU-funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7.
     58
     59We first present a uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is similar to early versions of \emph{CompCert C}.
     60To 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
     62To establish that our approach works, and scales beyond `toy' languages to more realistic programming languages, we have implemented a compiler using this technique.
     63The \emph{CerCo verified C compiler} compiles the CerCo C language fragment to object binaries for the MCS-51 8-bit embedded microcontroller.
     64This is a well-known and still popular processor in the embedded systems community.
     65Our compiler lifts a cost-model induced on machine code that it produces, back through the compilation chain, to the source-level.
     66At 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.
     67These annotations may be used by the programmer to predict concrete execution time and stack space usage.
     68
     69As we are targeting an embedded microcontroller we have not considered dynamic memory allocation.
     70However, we believe that our labelling approach is general enough to handle resources other than execution time and stack space usage, including dynamic memory allocation.
     71
     72To demonstrate source-level verification of costs we have implemented a Frama-C plugin~\cite{framac} that invokes our compiler on a source program and uses it to generate invariants on the high-level source that correctly model low-level costs.
     73The plugin certifies that the program respects these costs by calling automated theorem provers, an innovative and novel technique in the field of static analysis for non-functional properties.
     74Using this plugin, we have conducted case studies, including showing that the plugin can automatically compute and certify the exact reaction time of Lustre~\cite{lustre} data flow programs compiled into C.
     75
     76The compiler is verified using the Matita interactive theorem prover, an implementation of the Calculus of Coinductive Constructions, developed at the University of Bologna.
     77
    5678\paragraph{Vision.}
    57 We want to reconcile functional and non-functional analysis: to share
    58 information between them and perform both at the same time on high-level source
    59 code.
    6079
    6180
     
    7695when components have been specified but not implemented, as modularity means
    7796that it is enough to specify the non-functional behaviour of missing components.
    78 
    79 \paragraph{Contributions.}
    80 We have developed \emph{the labelling approach}~\cite{labelling}, a technique
    81 to implement compilers that induce cost models on source programs by very
    82 lightweight tracking of code changes through the compilation pipeline.
    83 
    84 We have implemented a compiler from C to object binaries for the 8051
    85 microcontroller which uses this technique. The compiler predicts
    86 execution time and stack space usage. We have also verified the compile using
    87 an interactive theorem prover. As we are targeting an embedded microcontroller
    88 we have not considered dynamic memory allocation.
    89 
    90 To demonstrate source-level verification of costs we have implemented a Frama-C
    91 plugin~\cite{framac} that invokes the compiler on a source program and uses it
    92 to generate invariants on the high-level source that correctly model low-level
    93 costs. The plugin certifies that the program respects these costs by calling
    94 automated theorem provers, a new and innovative technique in the field of cost
    95 analysis.
    96 
    97 Finally, we have conducted several case studies, including showing that the
    98 plugin can automatically compute and certify the exact reaction time of
    99 Lustre~\cite{lustre} data flow programs compiled into C.
    10097
    10198\subsection{Project context and approach}
Note: See TracChangeset for help on using the changeset viewer.