Changeset 3442


Ignore:
Timestamp:
Feb 17, 2014, 11:40:57 AM (6 years ago)
Author:
mulligan
Message:

Changes up to Section 3. Added missing reference to AbsInt?'s aiT tools.

Location:
Papers/fopara2013
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • Papers/fopara2013/fopara13.bib

    r3439 r3442  
    278278  pages={167-181}
    279279}
     280
     281@misc
     282{ absint,
     283  year = {2014},
     284  url = {http://www.absint.com/ait/},
     285  author = {{AbsInt}},
     286  title = {{aiT WCET} analysis tools}
     287}

  • Papers/fopara2013/fopara13.tex

    r3441 r3442  
    185185
    186186\section{Project context and approach}
    187 Formal methods for verification of functional properties of programs have
     187Formal methods for the verification of functional properties of programs have
    188188now reached a level of maturity and automation that is facilitating a slow but
    189189increasing adoption in production environments. For safety critical code, it is
    … …  
    196196becomes an assumption for later analysis.
    197197
    198 The scenario for the verification of non-functional properties (time spent,
     198The outlook for verifying non-functional properties of programs (time spent,
    199199memory used, energy consumed) is bleaker.
    200200% and the future seems to be getting even worse.
    … …  
    220220from the research community towards the introduction of alternative
    221221hardware with more predictable behaviour, which would be more suitable
    222 for static analysis.  One example being investigated by the Proartis
    223 project~\cite{proartis} is to decouple execution time from execution
     222for static analysis.  One example, being investigated by the Proartis
     223project~\cite{proartis}, is to decouple execution time from execution
    224224history by introducing randomisation.
    225225
    226226In the CerCo project \cite{cerco} we do not try to address this problem, optimistically
    227227assuming that improvements in low-level timing analysis or architecture will make
    228 verification feasible in the longer term. The main objective of our work is
    229 instead to bring together static analysis of functional and non-functional
     228verification feasible in the longer term. Instead, the main objective of our work is
     229to bring together the static analysis of functional and non-functional
    230230properties, which, according to the current state of the art, are completely
    231231independent activities with limited exchange of information: while the
    … …  
    258258The second reason to perform the analysis on the object code is that bounding
    259259the worst case execution time of small code fragments in isolation (e.g. loop
    260 bodies) and then adding up the bounds yields very poor estimates because no
    261 knowledge of the hardware state on executing the fragment can be assumed. By
     260bodies) and then adding up the bounds yields very poor estimates as no
     261knowledge of the hardware state prior to executing the fragment can be assumed. By
    262262analysing longer runs the bound obtained becomes more precise because the lack
    263263of information about the initial state has a relatively small impact.
    … …  
    266266are required to bound the number of times each basic block is
    267267executed.  Current state
    268 of the art WCET technology such as AbsInt performs these analyses on the
     268of the art WCET technology such as AbsInt's aiT analysis tools~\cite{absint} performs these analyses on the
    269269object code, where the logic of the program is harder to reconstruct
    270270and most information available at the source code level has been lost;
    … …  
    297297parametric: the cost of a block can depend on actual program data, on a
    298298summary of the execution history, or on an approximated representation of the
    299 hardware state. For example, loop optimizations may assign to a loop body a cost
     299hardware state. For example, loop optimisations may assign a cost to a loop body
    300300that is a function of the number of iterations performed. As another example,
    301301the cost of a block may be a function of the vector of stalled pipeline states,
    … …  
    328328state-of-the-art WCET tools is very large: one needs to trust the control flow
    329329analyser and the linear programming libraries it uses and also the formal models
    330 of the hardware. In CerCo we are moving the control flow analysis to the source
     330of the hardware under analysis. In CerCo we are moving the control flow analysis to the source
    331331code and we are introducing a non-standard compiler too. To reduce the trusted
    332332code base, we implemented a prototype and a static analyser in an interactive
Note: See TracChangeset for help on using the changeset viewer.