Changeset 3460 for Papers


Ignore:
Timestamp:
Feb 21, 2014, 11:24:39 AM (5 years ago)
Author:
mulligan
Message:

more fiddling, commit to avoid conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3459 r3460  
    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 a small trusted code base. We developed a certified compiler that translates C source code to object code, producing a copy of the source code embellished with cost annotations as an additional side-effect. These annotations expose and track precisely the actual (non-asymptotic)
     100and a small trusted code base. We developed a C compiler, verified in Matita, that translates source code to object code, producing a copy of the source code embellished with cost annotations as an additional side-effect. These annotations expose and track precisely the actual (non-asymptotic)
    101101computational cost of the input program at
    102102the source level. Untrusted invariant generators and trusted theorem provers
     
    238238optimisations may completely transform source level loops. Despite the lack of a uniform, compilation- and
    239239program-independent cost model on the source language, the literature on the
    240 analysis of non-asymptotic execution time on high level languages that assumes
     240analysis of non-asymptotic execution time on high level languages assuming
    241241such a model is growing and gaining momentum. However, unless we provide a
    242242replacement for such cost models, this literature's future practical impact looks
     
    258258To calculate the cost of an execution, value and control flow analyses
    259259are required to bound the number of times each basic block is
    260 executed.  Current state
    261 of the art WCET technology such as AbsInt's aiT analysis tools~\cite{absint} performs these analyses on the
     260executed.  Currently, state
     261of the art WCET analysis tools, such as AbsInt's aiT toolset~\cite{absint}, perform these analyses on
    262262object code, where the logic of the program is harder to reconstruct
    263263and most information available at the source code level has been lost;
     
    279279\subsection{CerCo's approach}
    280280
    281 In CerCo we propose a radically new approach to the problem: we reject the idea
     281In CerCo we propose a new approach to the problem: we abandon the idea
    282282of a uniform cost model and we propose that the compiler, which knows how the
    283283code is translated, must return the cost model for basic blocks of high level
     
    285285to reverse them and by interfacing with processor timing analysis.
    286286
    287 By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
     287By embracing the knowledge implicit in the compilation process, instead of avoiding it like EmBounded did, a CerCo
    288288compiler can both produce efficient code and return costs that are
    289289as precise as the processor timing analysis can be. Moreover, our costs can be
     
    295295which can be exposed in the source code and updated at each basic block exit. It
    296296is parametricity that allows one to analyse small code fragments without losing
    297 precision: in the analysis of the code fragment we do not have to ignore the
    298 initial hardware state. On the contrary, we can assume that we know exactly which
     297precision. In the analysis of the code fragment we do not have to ignore the
     298initial hardware state, rather, we may assume that we know exactly which
    299299state (or mode, as the WCET literature calls it) we are in.
    300300
    301 The CerCo approach has the potential to dramatically improve the state of the
     301The CerCo approach has the potential to substantially improve upon the current state of the
    302302art. By performing control and data flow analyses on the source code, the error
    303 prone translation of invariants is completely avoided. Instead, this
     303prone translation of invariants is avoided. Instead, this
    304304work is done at the source level using tools of the user's choice.
    305305Any available technique for the verification of functional properties
     
    307307infer and certify cost invariants for the program.  There are no
    308308limitations on the types of loops or data structures involved. Parametric cost analysis
    309 becomes the default one, with non-parametric bounds used as a last resort when
    310 trading the complexity of the analysis with its precision. \emph{A priori}, no
     309becomes the default one, with non-parametric bounds used as a last resort when the user
     310decides to trade the complexity of the analysis with its precision. \emph{A priori}, no
    311311technique previously used in traditional WCET is lost: processor
    312312timing analyses can be used by the compiler on the object code, and the rest can be applied
     
    316316
    317317
    318 All software used to verify properties of programs must be as bug free as
     318We take as granted the position that all software used to verify properties of programs must be as bug free as
    319319possible. The trusted code base for verification consists of the code that needs
    320320to be trusted to believe that the property holds. The trusted code base of
    321321state-of-the-art WCET tools is very large: one needs to trust the control flow
    322 analyser and the linear programming libraries it uses and also the formal models
    323 of the hardware under analysis. In CerCo we are moving the control flow analysis to the source
     322analyser, the linear programming libraries used, and also the formal models
     323of the hardware under analysis, for example. In CerCo we are moving the control flow analysis to the source
    324324code and we are introducing a non-standard compiler too. To reduce the trusted
    325325code base, we implemented a prototype and a static analyser in an interactive
Note: See TracChangeset for help on using the changeset viewer.