Changeset 3334


Ignore:
Timestamp:
Jun 7, 2013, 11:36:25 AM (4 years ago)
Author:
mulligan
Message:

About half way through

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3333 r3334  
    9292\begin{abstract}
    9393This paper provides an overview of the FET-Open Project CerCo
    94 (`Certified Complexity'). The project's main achievement has been
     94(`Certified Complexity'). The project's main achievement is
    9595the development of a technique for performing static analyses of non-functional
    96 properties of programs (time, space) at the source level, without losing
    97 accuracy and with a small, trusted code base. The main software component
     96properties of programs (time, space) at the source level, without loss of accuracy
     97and with a small, trusted code base. The main software component
    9898developed is a formally certified complexity certifying compiler. The compiler
    9999translates source code to object code and produces an instrumented copy of the
    100 source code. The latter exposes at
     100source code. This instrumentation exposes at
    101101the source level---and tracks precisely---the actual (non-asymptotic)
    102102computational cost of the input program. Untrusted invariant generators and trusted theorem provers
     
    110110\section{Introduction}
    111111
    112 \paragraph{Problem statement.} Computer programs can be specified with both
     112\paragraph{Problem statement} Computer programs can be specified with both
    113113functional constraints (what a program must do) and non-functional constraints
    114 (e.g. what resources – time, space, etc. – the program may use).  In the current
     114(e.g. what resources---time, space, etc.---the program may use).  In the current
    115115state of the art, functional properties are verified for high-level source code
    116116by combining user annotations (e.g. preconditions and invariants) with a
    117117multitude of automated analyses (invariant generators, type systems, abstract
    118 interpretation, theorem proving, etc.). By contrast, non-functional properties
     118interpretation, theorem proving, and so on). By contrast, non-functional properties
    119119are generally checked on low-level object code, but also demand information
    120120about high-level functional behaviour that must somehow be recreated.
    121121
    122122This situation presents several problems: 1) it can be hard to infer this
    123 high-level structure in the presence of compiler optimizations; 2) techniques
    124 working on object code are not useful in early development; yet problems
     123high-level structure in the presence of compiler optimisations; 2) techniques
     124working on object code are not useful in early development, yet problems
    125125detected later are more expensive to tackle; 3) parametric cost analysis is very
    126126hard: how can we reflect a cost that depends on the execution state (e.g. the
    127127value of a register or a carry bit) to a cost that the user can understand
    128 looking at source code?; 4) functional analysis performed only on object code
     128looking at source code? 4) functional analysis performed only on object code
    129129makes any contribution from the programmer hard, leading to less precision in
    130130the estimates.
    131131
    132 \paragraph{Vision and approach.} We want to reconcile functional and
    133 non-functional analysis: to share information and perform both at the same time
     132\paragraph{Vision and approach} We want to reconcile functional and
     133non-functional analyses: to share information and perform both at the same time
    134134on source code.
    135135%
    136136What has previously prevented this approach is the lack of a uniform and precise
    137137cost model for high-level code: 1) each statement occurrence is compiled
    138 differently and optimizations may change control flow; 2) the cost of an object
     138differently and optimisations may change control flow; 2) the cost of an object
    139139code instruction may depend on the runtime state of hardware components like
    140 pipelines and caches, which is not visible in the source code.
     140pipelines and caches, all of which are not visible in the source code.
    141141
    142142To solve the issue, we envision a new generation of compilers able to keep track
     
    145145and accounts for runtime state. With such a source-level cost model we can
    146146reduce non-functional verification to the functional case and exploit the state
    147 of the art in automated high-level verification \cite{survey}. The techniques
    148 previously used by Worst Case Execution Time (WCET) analysers on the object code
    149 are still available, but can now be coupled with additional source-level
     147of the art in automated high-level verification~\cite{survey}. The techniques
     148currently used by the Worst Case Execution Time (WCET) community, which performs its analysis on object code
     149, are still available but can now be coupled with an additional source-level
    150150analysis. Where the approach produces precise cost models too complex to reason
    151151about, safe approximations can be used to trade complexity with precision.
     
    155155components.
    156156
    157 \paragraph{Contributions.} We have developed the labeling approach \cite{labeling}, a
     157\paragraph{Contributions} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a
    158158technique to implement compilers that induce cost models on source programs by
    159159very lightweight tracking of code changes through compilation. We have studied
     
    171171\section{Project context and objectives}
    172172Formal methods for verification of functional properties of programs have
    173 reached a level of maturity and automation that is allowing a slow but
     173now reached a level of maturity and automation that is facilitating a slow but
    174174increasing adoption in production environments. For safety critical code, it is
    175 getting usual to combine rigorous software engineering methodologies and testing
    176 with static analysis in order to benefit from the strong points of every
    177 approach and mitigate the weaknesses. Of particular interest are open frameworks
     175becoming commonplace to combine rigorous software engineering methodologies and testing
     176with static analysis, taking the strong points of each approach and mitigating
     177their weaknesses. Of particular interest are open frameworks
    178178for the combination of different formal methods, where the programs can be
    179179progressively specified and are continuously enriched with new safety
     
    183183The scenario for the verification of non-functional properties (time spent,
    184184memory used, energy consumed) is bleaker and the future seems to be getting even
    185 worse. Most industries verify that real time systems meets their deadlines
    186 simply measuring the time spent in many runs of the systems,  computing the
     185worse. Most industries verify that real time systems meet their deadlines
     186by simply performing many runs of the system and timing their execution,  computing the
    187187maximum time and adding an empirical safety margin, claiming the result to be a
    188188bound for the WCET of the program. Formal methods and software to statically
    189189analyse the WCET of programs exist, but they often produce bounds that are too
    190 pessimistic to be useful. Recent advancements in hardware architectures is all
     190pessimistic to be useful. Recent advancements in hardware architectures are all
    191191focused on the improvement of the average case performance, not the
    192 predictability of the worst case. Execution time is getting more and more
    193 dependent from the execution history, that determines the internal state of
    194 hardware components like pipelines and caches. Multi-core processors and non 
    195 uniform memory models are drastically reducing the possibility of performing
     192predictability of the worst case. Execution time is becoming increasingly
     193dependent on execution history and the internal state of
     194hardware components like pipelines and caches. Multi-core processors and non-uniform
     195memory models are drastically reducing the possibility of performing
    196196static analysis in isolation, because programs are less and less time
    197 composable. Clock precise hardware models are necessary to static analysis, and
    198 getting them is becoming harder as a consequence of the increased hardware
    199 complexity.
    200 
    201 Despite all the above, the need for reliable real time systems and programs is
    202 increasing, and there is a raising pressure from the research community towards
    203 the differentiation of hardware. The aim is the introduction of alternative
    204 hardware with a more predictable behaviour, more suitable to be statically
    205 analysed. An example is the decoupling execution time from the execution history
    206 by introducing randomization \cite{proartis}.
     197composable. Clock-precise hardware models are necessary for static analysis, and
     198obtaining them is becoming harder as a consequence of the increased sophistication
     199of hardware design.
     200
     201Despite the aforementioned problems, the need for reliable real time systems and programs is
     202increasing, and there is increasing pressure from the research community towards
     203the differentiation of hardware. The aim is to introduce alternative
     204hardware with more predictable behaviour and hence more suitability for static
     205analyses, for example, the decoupling of execution time from execution history
     206by introducing randomisation \cite{proartis}.
    207207
    208208In the CerCo project \cite{cerco} we do not try to address this problem, optimistically
    209209assuming that static analysis of non-functional properties of programs will
    210 return to be feasible in the long term. The main objective of our work is
     210become feasible in the longer term. The main objective of our work is
    211211instead to bring together static analysis of functional and non-functional
    212212properties, which, according to the current state of the art, are completely
     
    214214functional properties are verified on the source code, the analysis of
    215215non-functional properties is entirely performed on the object code to exploit
    216 clock precise hardware models.
    217 
    218 There are two main reasons to currently perform the analysis on the object code.
    219 The first one is the obvious lack of a uniform, precise cost model for source
     216clock-precise hardware models.
     217
     218Analysis currently takes place on object code for two main reasons.
     219First, there is a lack of a uniform, precise cost model for source
    220220code instructions (or even basic blocks). During compilation, high level
    221221instructions are torn apart and reassembled in context-specific ways so that
    222 identifying a fragment of object code with a single high level instruction is
     222identifying a fragment of object code and a single high level instruction is
    223223infeasible. Even the control flow of the object and source code can be very
    224 different as a result of optimizations, for example due to aggressive loop
    225 optimisations. Despite the lack of a uniform, compilation- and
     224different as a result of optimisations, for example aggressive loop
     225optimisations may completely transform source level loops. Despite the lack of a uniform, compilation- and
    226226program-independent cost model on the source language, the literature on the
    227 analysis of non asymptotic execution time on high level languages that assumes
    228 such a model is growing and getting momentum. Its practical usefulness is doomed
    229 to be minimal, unless we can provide a replacement for such cost models. Some
    230 hope has been provided by the EmBounded project \cite{embounded}, which
    231 compositionally compiles high level code to a byte code that is executed by an
     227analysis of non-asymptotic execution time on high level languages that assumes
     228such a model is growing and gaining momentum. However, unless we can provide a
     229replacement for such cost models, this literature's future practical impact looks
     230to be minimal. Some hope has been provided by the EmBounded project \cite{embounded}, which
     231compositionally compiles high-level code to a byte code that is executed by an
    232232emulator with guarantees on the maximal execution time spent for each byte code
    233 instruction. The approach indeed provides a uniform model, at the price of
    234 loosing precision of the model (each cost is a pessimistic upper bound) and
    235 performance of the executed code (because the byte code is emulated
    236 compositionally instead of performing a fully non compositional compilation).
     233instruction. The approach provides a uniform model at the price of the model's
     234precision (each cost is a pessimistic upper bound) and performance of the
     235executed code (because the byte code is emulated  compositionally instead of
     236performing a fully non-compositional compilation).
    237237%
    238238The second reason to perform the analysis on the object code is that bounding
     
    241241knowledge on the hardware state can be assumed when executing the fragment. By
    242242analysing longer runs the bound obtained becomes more precise because the lack
    243 of knowledge on the initial state has less effects on longer computations.
     243of knowledge on the initial state has less of an effect on longer computations.
    244244
    245245In CerCo we propose a radically new approach to the problem: we reject the idea
     
    258258the cost of a block may be a function of the vector of stalled pipeline states,
    259259which can be exposed in the source code and updated at each basic block exit. It
    260 is parametricity that allows to analyse small code fragments without loosing
     260is parametricity that allows one to analyse small code fragments without losing
    261261precision: in the analysis of the code fragment we do not have to ignore the
    262 initial hardware state. On the contrary, we can assume to know exactly which
    263 state (or mode, as WCET literature calls it) we are in.
     262initial hardware state. On the contrary, we can assume that we know exactly which
     263state (or mode, as the WCET literature calls it) we are in.
    264264
    265265The cost of an execution is the sum of the cost of basic blocks multiplied by
     
    269269Current state of the art WCET technology
    270270\cite{stateart} performs the analysis on the object code, where the logic of the
    271 program is harder to reconstruct and most information available on the source
    272 code has been lost. Imprecision in the analysis leads to useless bounds. To
     271program is harder to reconstruct and most information available at the source
     272code level has been lost. Imprecision in the analysis leads to useless bounds. To
    273273augment precision, the tools ask the user to provide constraints on the object
    274274code control flow, usually in the form of bounds on the number of iterations of
     
    276276the source and object code, translating his assumptions on the source code
    277277(which may be wrong) to object code constraints. The task is error prone and
    278 hard, in presence of complex optimizations.
    279 
    280 The CerCo approach has the potentiality to dramatically improve the state of the
    281 art. By performing control and data flow analysis on the source code, the error
     278hard, especially in the presence of complex compiler optimisations.
     279
     280The CerCo approach has the potential to dramatically improve the state of the
     281art. By performing control and data flow analyses on the source code, the error
    282282prone translation of invariants is completely avoided. It is in fact performed
    283283by the compiler itself when it induces the cost model on the source language.
     
    286286infer and certify cost invariants for the program. Parametric cost analysis
    287287becomes the default one, with non parametric bounds used as last resorts when
    288 trading the complexity of the analysis with its precision. A priori, no
     288trading the complexity of the analysis with its precision. \emph{A priori}, no
    289289technique previously used in traditional WCET is lost: they can just be applied
    290 on the source code.
     290at the source code level.
    291291
    292292Traditional techniques for WCET that work on object code are also affected by
     
    303303analyser and the linear programming libraries it uses and also the formal models
    304304of the hardware. In CerCo we are moving the control flow analysis to the source
    305 code and we are introducing a non standard compiler too. To reduce the trusted
     305code and we are introducing a non-standard compiler too. To reduce the trusted
    306306code base, we implemented a prototype and a static analyser in an interactive
    307307theorem prover, which was used to certify that the cost computed on the source
     
    315315base is an off-the-shelf invariant generator which, in turn, can be proved
    316316correct using an interactive theorem prover. Therefore we achieve the double
    317 objective of allowing to use more off-the-shelf components (e.g. provers and
    318 invariant generators) while reducing the trusted code base at the same time.
     317objective of allowing the use more off-the-shelf components (e.g. provers and
     318invariant generators) whilst reducing the trusted code base at the same time.
    319319
    320320%\paragraph{Summary of the CerCo objectives.} To summarize, the goal of CerCo is
     
    344344% of a cost model inducing compiler.
    345345
    346 \section{The typical CerCo work-flow}
     346\section{The typical CerCo workflow}
    347347\begin{figure}[!t]
    348348\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
     
    419419\end{tabular}
    420420\caption{On the left: code to count the array's elements
    421  greater or equal to the treshold. On the right: CerCo's interaction
     421 that are greater or equal to the treshold. On the right: CerCo's interaction
    422422 diagram. CerCo's components are drawn solid.}
    423423\label{test1}
    424424\end{figure}
    425 We illustrate the work-flow we envision (on the right of \autoref{test1})
    426 on an example program (on the left of \autoref{test1}).
     425We illustrate the workflow we envisage (on the right of~\autoref{test1})
     426on an example program (on the left of~\autoref{test1}).
    427427The user writes the program and feeds it to the CerCo compiler, which outputs
    428428an instrumented version of the same program that updates global variables
     
    431431compiler. The annotated program can then be enriched with complexity assertions
    432432in the style of Hoare logic, that are passed to a deductive platform (in our
    433 case Frama-C). We provide as a Frama-c cost plugin a simple automatic
     433case Frama-C). We provide as a Frama-C cost plugin a simple automatic
    434434synthesiser for complexity assertions (the blue lines in \autoref{itest1}),
    435435which can be overridden by the user to increase or decrease accuracy. From the
     
    440440one execution if it holds before, to prove that the whole program execution
    441441takes at most 1228 cycles, etc.). The CVC3 prover closes all obligations
    442 in a few seconds on standard hardware.
     442in a few seconds on routine commodity hardware.
    443443%
    444444\fvset{commandchars=\\\{\}}
Note: See TracChangeset for help on using the changeset viewer.