Changeset 3430 for Papers


Ignore:
Timestamp:
Feb 13, 2014, 2:12:30 PM (5 years ago)
Author:
campbell
Message:

Revisions up to the end of section 3.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3429 r3430  
    9898the development of a technique for analysing non-functional
    9999properties of programs (time, space) at the source level, with little or no loss of accuracy
    100 and with a small, trusted code base. The main software component
     100and with a small trusted code base. The main software component
    101101developed is a certified compiler producing cost annotations. The compiler
    102102translates source code to object code and produces an instrumented copy of the
     
    113113\section{Introduction}
    114114
    115 \paragraph{Problem statement.} Computer programs can be specified with both
     115%\paragraph{Problem statement.}
     116Computer programs can be specified with both
    116117functional constraints (what a program must do) and non-functional constraints
    117 (e.g. what resources---time, space, etc.---the program may use).  In the current
     118(what resources---time, space, etc.---the program may use).  In the current
    118119state of the art, functional properties are verified for high-level source code
    119120by combining user annotations (e.g. preconditions and invariants) with a
     
    121122interpretation, theorem proving, and so on). By contrast, non-functional properties
    122123are generally checked on low-level object code, but also demand information
    123 about high-level functional behaviour that must somehow be recreated.
     124about high-level functional behaviour that must somehow be reconstructed.
    124125
    125126This situation presents several problems: 1) it can be hard to infer this
     
    129130hard: how can we reflect a cost that depends on the execution state (e.g. the
    130131value of a register or a carry bit) to a cost that the user can understand
    131 looking at source code? 4) functional analysis performed only on object code
    132 makes any contribution from the programmer hard, leading to less precision in
     132looking at source code? 4) performing functional analysis on the object code
     133makes it hard for the programmer to provide information, leading to less precision in
    133134the estimates.
    134135
     
    146147of program structure through compilation and optimisation, and to exploit that
    147148information to define a cost model for source code that is precise, non-uniform,
    148 and accounts for runtime state. With such a source-level cost model we can
     149and which accounts for runtime state. With such a source-level cost model we can
    149150reduce non-functional verification to the functional case and exploit the state
    150151of the art in automated high-level verification~\cite{survey}. The techniques
     
    153154analysis. Where the approach produces precise cost models too complex to reason
    154155about, safe approximations can be used to trade complexity with precision.
    155 Finally, source code analysis can be made during early development stages, when
     156Finally, source code analysis can be used during the early stages of development, when
    156157components have been specified but not implemented: source code modularity means
    157158that it is enough to specify the non-functional behaviour of unimplemented
     
    163164how to formally prove the correctness of compilers implementing this technique.
    164165We have implemented such a compiler from C to object binaries for the 8051
    165 micro-controller, and verified it in an interactive theorem prover. We have
    166 implemented a Frama-C plugin \cite{framac} that invokes the compiler on a source
    167 program and uses this to generate invariants on the high-level source that
    168 correctly model low-level costs. Finally, the plugin certifies that the program
    169 respects these costs by calling automated theorem provers, a new and innovative
    170 technique in the field of cost analysis. As a case study, we show how the
    171 plugin can automatically compute and certify the exact reaction time of Lustre
    172 \cite{lustre} data flow programs compiled into C.
    173 
    174 \section{Project context and objectives}
     166micro-controller, and verified it in an interactive theorem prover.
     167
     168To demonstrate source-level verification of costs we have implemented
     169a Frama-C plugin \cite{framac} that invokes the compiler on a source
     170program and uses this to generate invariants on the high-level source
     171that correctly model low-level costs. The plugin certifies that the
     172program respects these costs by calling automated theorem provers, a
     173new and innovative technique in the field of cost analysis. Finally,
     174we have conduct several case studies, including showing that the
     175plugin can automatically compute and certify the exact reaction time
     176of Lustre~\cite{lustre} data flow programs compiled into C.
     177
     178\section{Project context and approach}
    175179Formal methods for verification of functional properties of programs have
    176180now reached a level of maturity and automation that is facilitating a slow but
     
    185189
    186190The scenario for the verification of non-functional properties (time spent,
    187 memory used, energy consumed) is bleaker and the future seems to be getting even
    188 worse. Most industries verify that real time systems meet their deadlines
     191memory used, energy consumed) is bleaker.
     192% and the future seems to be getting even worse.
     193Most industries verify that real time systems meet their deadlines
    189194by simply performing many runs of the system and timing their execution,  computing the
    190195maximum time and adding an empirical safety margin, claiming the result to be a
    191196bound for the WCET of the program. Formal methods and software to statically
    192197analyse the WCET of programs exist, but they often produce bounds that are too
    193 pessimistic to be useful. Recent advancements in hardware architectures are all
     198pessimistic to be useful. Recent advancements in hardware architecture
     199have been
    194200focused on the improvement of the average case performance, not the
    195201predictability of the worst case. Execution time is becoming increasingly
     
    199205static analysis in isolation, because programs are less and less time
    200206composable. Clock-precise hardware models are necessary for static analysis, and
    201 obtaining them is becoming harder as a consequence of the increased sophistication
     207obtaining them is becoming harder due to the increased sophistication
    202208of hardware design.
    203209
    204 Despite the aforementioned problems, the need for reliable real time systems and programs is
    205 increasing, and there is increasing pressure from the research community towards
    206 the differentiation of hardware. The aim is to introduce alternative
    207 hardware with more predictable behaviour and hence more suitability for static
    208 analyses, for example, the decoupling of execution time from execution history
    209 by introducing randomisation \cite{proartis}.
     210Despite the aforementioned problems, the need for reliable real time
     211systems and programs is increasing, and there is increasing pressure
     212from the research community towards the introduction of alternative
     213hardware with more predictable behaviour, which would be more suitable
     214for static analysis.  One example being investigated by the Proartis
     215project~\cite{proartis} is to decouple execution time from execution
     216history by introducing randomisation.
    210217
    211218In the CerCo project \cite{cerco} we do not try to address this problem, optimistically
    212 assuming that static analysis of non-functional properties of programs will
    213 become feasible in the longer term. The main objective of our work is
     219assuming that improvements in low-level timing analysis or architecture will make
     220verification feasible in the longer term. The main objective of our work is
    214221instead to bring together static analysis of functional and non-functional
    215222properties, which, according to the current state of the art, are completely
     
    231238program-independent cost model on the source language, the literature on the
    232239analysis of non-asymptotic execution time on high level languages that assumes
    233 such a model is growing and gaining momentum. However, unless we can provide a
     240such a model is growing and gaining momentum. However, unless we provide a
    234241replacement for such cost models, this literature's future practical impact looks
    235242to be minimal. Some hope has been provided by the EmBounded project \cite{embounded}, which
    236243compositionally compiles high-level code to a byte code that is executed by an
    237 emulator with guarantees on the maximal execution time spent for each byte code
    238 instruction. That approach provides a uniform model at the price of the model's
    239 precision (each cost is a pessimistic upper bound) and performance of the
    240 executed code (because the byte code is emulated compositionally instead of
     244interpreter with guarantees on the maximal execution time spent for each byte code
     245instruction. This provides a uniform model at the expense of the model's
     246precision (each cost is a pessimistic upper bound) and the performance of the
     247executed code (because the byte code is interpreted compositionally instead of
    241248performing a fully non-compositional compilation).
    242249
     
    244251the worst case execution time of small code fragments in isolation (e.g. loop
    245252bodies) and then adding up the bounds yields very poor estimates because no
    246 knowledge on the hardware state can be assumed when executing the fragment. By
     253knowledge of the hardware state on executing the fragment can be assumed. By
    247254analysing longer runs the bound obtained becomes more precise because the lack
    248 of knowledge on the initial state has less of an effect on longer computations.
    249 
    250 The cost of an execution is the sum of the cost of basic blocks multiplied by
    251 the number of times they are executed, which is a functional property of the
    252 program. Therefore, in order to perform (parametric) time analysis of programs,
    253 it is necessary to combine a cost model with control and data flow analysis.
    254 Current state of the art WCET technology such as AbsInt
    255 (see~\cite{stateart} for a survey) performs the analysis on the object code, where the logic of the
    256 program is harder to reconstruct and most information available at the source
    257 code level has been lost. Imprecision in the analysis leads to useless bounds. To
    258 augment precision, the tools ask the user to provide constraints on the object
    259 code control flow, usually in the form of bounds on the number of iterations of
    260 loops or linear inequalities on them. This requires the user to manually link
    261 the source and object code, translating his assumptions on the source code
    262 (which may be wrong) to object code constraints. The task is error prone and
    263 hard, especially in the presence of complex compiler optimisations.
     255of information about the initial state has a relatively small impact.
     256
     257To calculate the cost of an execution, value and control flow analyses
     258are required to bound the number of times each basic block is
     259executed.  Current state
     260of the art WCET technology such as AbsInt performs these analyses on the
     261object code, where the logic of the program is harder to reconstruct
     262and most information available at the source code level has been lost;
     263see~\cite{stateart} for a survey. Imprecision in the analysis can lead to useless bounds. To
     264augment precision, the tools ask the user to provide constraints on
     265the object code control flow, usually in the form of bounds on the
     266number of iterations of loops or linear inequalities on them. This
     267requires the user to manually link the source and object code,
     268translating his assumptions on the source code (which may be wrong) to
     269object code constraints. The task is error prone and hard, especially
     270in the presence of complex compiler optimisations.
    264271
    265272Traditional techniques for WCET that work on object code are also affected by
     
    275282code is translated, must return the cost model for basic blocks of high level
    276283instructions. It must do so by keeping track of the control flow modifications
    277 to reverse them and by interfacing with static analysers.
     284to reverse them and by interfacing with processor timing analysis.
    278285
    279286By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
    280 compiler can at the same time produce efficient code and return costs that are
    281 as precise as the static analysis can be. Moreover, we allow our costs to be
    282 parametric: the cost of a block can depend on actual program data or on a
    283 summary of the execution history or on an approximated representation of the
     287compiler can both produce efficient code and return costs that are
     288as precise as the processor timing analysis can be. Moreover, our costs can be
     289parametric: the cost of a block can depend on actual program data, on a
     290summary of the execution history, or on an approximated representation of the
    284291hardware state. For example, loop optimizations may assign to a loop body a cost
    285292that is a function of the number of iterations performed. As another example,
     
    298305can be immediately reused and multiple techniques can collaborate together to
    299306infer and certify cost invariants for the program. Parametric cost analysis
    300 becomes the default one, with non parametric bounds used as last resorts when
     307becomes the default one, with non-parametric bounds used as a last resort when
    301308trading the complexity of the analysis with its precision. \emph{A priori}, no
    302 technique previously used in traditional WCET is lost: they can just be applied
     309technique previously used in traditional WCET is lost: processor
     310timing analyses can be used by the compiler on the object code, and the rest can be applied
    303311at the source code level.
    304312 Our approach can also work in the early
     
    307315
    308316All software used to verify properties of programs must be as bug free as
    309 possible. The trusted code base for verification is made by the code that needs
     317possible. The trusted code base for verification consists of the code that needs
    310318to be trusted to believe that the property holds. The trusted code base of
    311319state-of-the-art WCET tools is very large: one needs to trust the control flow
     
    314322code and we are introducing a non-standard compiler too. To reduce the trusted
    315323code base, we implemented a prototype and a static analyser in an interactive
    316 theorem prover, which was used to certify that the cost computed on the source
    317 code is indeed the one actually spent by the hardware. Formal models of the
     324theorem prover, which was used to certify that the costs added to the source
     325code are indeed those incurred by the hardware. Formal models of the
    318326hardware and of the high level source languages were also implemented in the
    319327interactive theorem prover. Control flow analysis on the source code has been
     
    442450execution time and the stack space usage.  The red lines in
    443451\autoref{itest1} introducing variables, functions and function calls
    444 starting \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the
    445 compiler.
     452starting with \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the
     453compiler.  For example, the two calls at the start of
     454\lstinline'count' say that 4 bytes of stack are required, and that it
     455takes 111 cycles to reach the next cost annotation (in the loop body).
     456The compiler measures these on the labeled object code that it generates.
    446457
    447458 The annotated program can then be enriched with complexity
    448459assertions in the style of Hoare logic, that are passed to a deductive
    449460platform (in our case Frama-C). We provide as a Frama-C cost plugin a
    450 simple automatic synthesiser for complexity assertions (the blue
    451 comments starting with \lstinline'/*@' in \autoref{itest1}), which can
    452 be overridden by the user to increase or decrease accuracy. From the
     461simple automatic synthesiser for complexity assertions which can
     462be overridden by the user to increase or decrease accuracy.  These are the blue
     463comments starting with \lstinline'/*@' in \autoref{itest1}. From the
    453464assertions, a general purpose deductive platform produces proof
    454465obligations which in turn can be closed by automatic or interactive
     
    461472to prove that the whole program execution takes at most 1358 cycles,
    462473etc.).  Note that the synthesised time bound for \lstinline'count',
    463 $178+214*(1+\lstinline'len')$ cycles, is parametric in the length of
     474$178+214*(1+\text{\lstinline'len'})$ cycles, is parametric in the length of
    464475the array. The CVC3 prover
    465476closes all obligations within half a minute on routine commodity
     
    489500      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
    490501*/
    491 int count(unsigned char *p, int len) {
     502int count(char *p, int len) {
    492503  char j;  int found = 0;
    493504  |__stack_incr(4);  __cost_incr(111);|
     
    772783many changes and more compiler code, but it is not fundamentally more
    773784complex. The proof of correctness, however, becomes much harder.
    774 \item We target a microprocessor that has a non uniform memory model, which is
     785\item We target a microprocessor that has a non-uniform memory model, which is
    775786still often the case for microprocessors used in embedded systems and that is
    776787becoming common again in multi-core processors. Therefore the compiler has to
Note: See TracChangeset for help on using the changeset viewer.