Changeset 3422 for Papers/fopara2013/fopara13.tex
- Timestamp:
- Feb 10, 2014, 6:45:54 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3420 r3422 219 219 clock-precise hardware models. 220 220 221 \subsection{Current object-code methods} 222 221 223 Analysis currently takes place on object code for two main reasons. 222 First, there is a lack ofa uniform, precise cost model for source224 First, there cannot be a uniform, precise cost model for source 223 225 code instructions (or even basic blocks). During compilation, high level 224 226 instructions are torn apart and reassembled in context-specific ways so that … … 234 236 compositionally compiles high-level code to a byte code that is executed by an 235 237 emulator with guarantees on the maximal execution time spent for each byte code 236 instruction. Th eapproach provides a uniform model at the price of the model's238 instruction. That approach provides a uniform model at the price of the model's 237 239 precision (each cost is a pessimistic upper bound) and performance of the 238 240 executed code (because the byte code is emulated compositionally instead of 239 241 performing a fully non-compositional compilation). 240 % 242 241 243 The second reason to perform the analysis on the object code is that bounding 242 244 the worst case execution time of small code fragments in isolation (e.g. loop … … 245 247 analysing longer runs the bound obtained becomes more precise because the lack 246 248 of 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 idea249 of a uniform cost model and we propose that the compiler, which knows how the250 code is translated, must return the cost model for basic blocks of high level251 instructions. It must do so by keeping track of the control flow modifications252 to reverse them and by interfacing with static analysers.253 254 By embracing compilation, instead of avoiding it like EmBounded did, a CerCo255 compiler can at the same time produce efficient code and return costs that are256 as precise as the static analysis can be. Moreover, we allow our costs to be257 parametric: the cost of a block can depend on actual program data or on a258 summary of the execution history or on an approximated representation of the259 hardware state. For example, loop optimizations may assign to a loop body a cost260 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. It263 is parametricity that allows one to analyse small code fragments without losing264 precision: in the analysis of the code fragment we do not have to ignore the265 initial hardware state. On the contrary, we can assume that we know exactly which266 state (or mode, as the WCET literature calls it) we are in.267 249 268 250 The cost of an execution is the sum of the cost of basic blocks multiplied by … … 281 263 hard, especially in the presence of complex compiler optimisations. 282 264 265 Traditional techniques for WCET that work on object code are also affected by 266 another problem: they cannot be applied before the generation of the object 267 code. Functional properties can be analysed in early development stages, while 268 analysis of non-functional properties may come too late to avoid expensive 269 changes to the program architecture. 270 271 \subsection{CerCo} 272 273 In CerCo we propose a radically new approach to the problem: we reject the idea 274 of a uniform cost model and we propose that the compiler, which knows how the 275 code is translated, must return the cost model for basic blocks of high level 276 instructions. It must do so by keeping track of the control flow modifications 277 to reverse them and by interfacing with static analysers. 278 279 By 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 284 hardware state. For example, loop optimizations may assign to a loop body a cost 285 that is a function of the number of iterations performed. As another example, 286 the cost of a block may be a function of the vector of stalled pipeline states, 287 which can be exposed in the source code and updated at each basic block exit. It 288 is parametricity that allows one to analyse small code fragments without losing 289 precision: in the analysis of the code fragment we do not have to ignore the 290 initial hardware state. On the contrary, we can assume that we know exactly which 291 state (or mode, as the WCET literature calls it) we are in. 292 283 293 The CerCo approach has the potential to dramatically improve the state of the 284 294 art. By performing control and data flow analyses on the source code, the error … … 292 302 technique previously used in traditional WCET is lost: they can just be applied 293 303 at 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 305 stages of development by axiomatically attaching costs to unimplemented components. 306 301 307 302 308 All software used to verify properties of programs must be as bug free as
Note: See TracChangeset
for help on using the changeset viewer.