Changeset 3442
- Timestamp:
- Feb 17, 2014, 11:40:57 AM (7 years ago)
- Location:
- Papers/fopara2013
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.bib
r3439 r3442 278 278 pages={167-181} 279 279 } 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 185 185 186 186 \section{Project context and approach} 187 Formal methods for verification of functional properties of programs have187 Formal methods for the verification of functional properties of programs have 188 188 now reached a level of maturity and automation that is facilitating a slow but 189 189 increasing adoption in production environments. For safety critical code, it is … … 196 196 becomes an assumption for later analysis. 197 197 198 The scenario for the verification of non-functional properties (time spent,198 The outlook for verifying non-functional properties of programs (time spent, 199 199 memory used, energy consumed) is bleaker. 200 200 % and the future seems to be getting even worse. … … 220 220 from the research community towards the introduction of alternative 221 221 hardware with more predictable behaviour, which would be more suitable 222 for static analysis. One example being investigated by the Proartis223 project~\cite{proartis} is to decouple execution time from execution222 for static analysis. One example, being investigated by the Proartis 223 project~\cite{proartis}, is to decouple execution time from execution 224 224 history by introducing randomisation. 225 225 226 226 In the CerCo project \cite{cerco} we do not try to address this problem, optimistically 227 227 assuming that improvements in low-level timing analysis or architecture will make 228 verification feasible in the longer term. The main objective of our work is229 instead to bring togetherstatic analysis of functional and non-functional228 verification feasible in the longer term. Instead, the main objective of our work is 229 to bring together the static analysis of functional and non-functional 230 230 properties, which, according to the current state of the art, are completely 231 231 independent activities with limited exchange of information: while the … … 258 258 The second reason to perform the analysis on the object code is that bounding 259 259 the 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 becauseno261 knowledge of the hardware state onexecuting the fragment can be assumed. By260 bodies) and then adding up the bounds yields very poor estimates as no 261 knowledge of the hardware state prior to executing the fragment can be assumed. By 262 262 analysing longer runs the bound obtained becomes more precise because the lack 263 263 of information about the initial state has a relatively small impact. … … 266 266 are required to bound the number of times each basic block is 267 267 executed. Current state 268 of the art WCET technology such as AbsInt performs these analyses on the268 of the art WCET technology such as AbsInt's aiT analysis tools~\cite{absint} performs these analyses on the 269 269 object code, where the logic of the program is harder to reconstruct 270 270 and most information available at the source code level has been lost; … … 297 297 parametric: the cost of a block can depend on actual program data, on a 298 298 summary of the execution history, or on an approximated representation of the 299 hardware state. For example, loop optimi zations may assign to a loop body a cost299 hardware state. For example, loop optimisations may assign a cost to a loop body 300 300 that is a function of the number of iterations performed. As another example, 301 301 the cost of a block may be a function of the vector of stalled pipeline states, … … 328 328 state-of-the-art WCET tools is very large: one needs to trust the control flow 329 329 analyser 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 source330 of the hardware under analysis. In CerCo we are moving the control flow analysis to the source 331 331 code and we are introducing a non-standard compiler too. To reduce the trusted 332 332 code base, we implemented a prototype and a static analyser in an interactive
Note: See TracChangeset
for help on using the changeset viewer.