Changeset 3422 for Papers/fopara2013


Ignore:
Timestamp:
Feb 10, 2014, 6:45:54 PM (6 years ago)
Author:
campbell
Message:

Basic restructuring of section 2.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3420 r3422  
    219219clock-precise hardware models.
    220220
     221\subsection{Current object-code methods}
     222
    221223Analysis currently takes place on object code for two main reasons.
    222 First, there is a lack of a uniform, precise cost model for source
     224First, there cannot be a uniform, precise cost model for source
    223225code instructions (or even basic blocks). During compilation, high level
    224226instructions are torn apart and reassembled in context-specific ways so that
     
    234236compositionally compiles high-level code to a byte code that is executed by an
    235237emulator with guarantees on the maximal execution time spent for each byte code
    236 instruction. The approach provides a uniform model at the price of the model's
     238instruction. That approach provides a uniform model at the price of the model's
    237239precision (each cost is a pessimistic upper bound) and performance of the
    238240executed code (because the byte code is emulated  compositionally instead of
    239241performing a fully non-compositional compilation).
    240 %
     242
    241243The second reason to perform the analysis on the object code is that bounding
    242244the worst case execution time of small code fragments in isolation (e.g. loop
     
    245247analysing longer runs the bound obtained becomes more precise because the lack
    246248of knowledge on the initial state has less of an effect on longer computations.
    247 
    248 In CerCo we propose a radically new approach to the problem: we reject the idea
    249 of a uniform cost model and we propose that the compiler, which knows how the
    250 code is translated, must return the cost model for basic blocks of high level
    251 instructions. It must do so by keeping track of the control flow modifications
    252 to reverse them and by interfacing with static analysers.
    253 
    254 By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
    255 compiler can at the same time produce efficient code and return costs that are
    256 as precise as the static analysis can be. Moreover, we allow our costs to be
    257 parametric: the cost of a block can depend on actual program data or on a
    258 summary of the execution history or on an approximated representation of the
    259 hardware state. For example, loop optimizations may assign to a loop body a cost
    260 that is a function of the number of iterations performed. As another example,
    261 the cost of a block may be a function of the vector of stalled pipeline states,
    262 which can be exposed in the source code and updated at each basic block exit. It
    263 is parametricity that allows one to analyse small code fragments without losing
    264 precision: in the analysis of the code fragment we do not have to ignore the
    265 initial hardware state. On the contrary, we can assume that we know exactly which
    266 state (or mode, as the WCET literature calls it) we are in.
    267249
    268250The cost of an execution is the sum of the cost of basic blocks multiplied by
     
    281263hard, especially in the presence of complex compiler optimisations.
    282264
     265Traditional techniques for WCET that work on object code are also affected by
     266another problem: they cannot be applied before the generation of the object
     267code. Functional properties can be analysed in early development stages, while
     268analysis of non-functional properties may come too late to avoid expensive
     269changes to the program architecture.
     270
     271\subsection{CerCo}
     272
     273In CerCo we propose a radically new approach to the problem: we reject the idea
     274of a uniform cost model and we propose that the compiler, which knows how the
     275code is translated, must return the cost model for basic blocks of high level
     276instructions. It must do so by keeping track of the control flow modifications
     277to reverse them and by interfacing with static analysers.
     278
     279By embracing compilation, instead of avoiding it like EmBounded did, a CerCo
     280compiler can at the same time produce efficient code and return costs that are
     281as precise as the static analysis can be. Moreover, we allow our costs to be
     282parametric: the cost of a block can depend on actual program data or on a
     283summary of the execution history or on an approximated representation of the
     284hardware state. For example, loop optimizations may assign to a loop body a cost
     285that is a function of the number of iterations performed. As another example,
     286the cost of a block may be a function of the vector of stalled pipeline states,
     287which can be exposed in the source code and updated at each basic block exit. It
     288is parametricity that allows one to analyse small code fragments without losing
     289precision: in the analysis of the code fragment we do not have to ignore the
     290initial hardware state. On the contrary, we can assume that we know exactly which
     291state (or mode, as the WCET literature calls it) we are in.
     292
    283293The CerCo approach has the potential to dramatically improve the state of the
    284294art. By performing control and data flow analyses on the source code, the error
     
    292302technique previously used in traditional WCET is lost: they can just be applied
    293303at the source code level.
    294 
    295 Traditional techniques for WCET that work on object code are also affected by
    296 another problem: they cannot be applied before the generation of the object
    297 code. Functional properties can be analysed in early development stages, while
    298 analysis of non-functional properties may come too late to avoid expensive
    299 changes to the program architecture. Our approach already works in early
    300 development stages by axiomatically attaching costs to unimplemented components.
     304 Our approach can also work in the early
     305stages of development by axiomatically attaching costs to unimplemented components.
     306
    301307
    302308All software used to verify properties of programs must be as bug free as
Note: See TracChangeset for help on using the changeset viewer.