Changeset 3422 for Papers/fopara2013/fopara13.tex

Timestamp:

Feb 10, 2014, 6:45:54 PM (7 years ago)

Author:

campbell

Message:

Basic restructuring of section 2.

File:

• Papers/fopara2013/fopara13.tex (modified) (5 diffs)

Papers/fopara2013/fopara13.tex

@@ -219 +219 @@
 clock-precise hardware models.
 
+\subsection{Current object-code methods}
+
 Analysis currently takes place on object code for two main reasons. 
-First, there is a lack of a uniform, precise cost model for source 
+First, there cannot be a uniform, precise cost model for source 
 code instructions (or even basic blocks). During compilation, high level 
 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 
 emulator with guarantees on the maximal execution time spent for each byte code 
-instruction. The approach provides a uniform model at the price of the model's
+instruction. That approach provides a uniform model at the price of the model's
 precision (each cost is a pessimistic upper bound) and performance of the
 executed code (because the byte code is emulated  compositionally instead of
 performing a fully non-compositional compilation).
-%
+
 The second reason to perform the analysis on the object code is that bounding 
 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 
 of knowledge on the initial state has less of an effect on longer computations.
-
-In CerCo we propose a radically new approach to the problem: we reject the idea 
-of a uniform cost model and we propose that the compiler, which knows how the 
-code is translated, must return the cost model for basic blocks of high level 
-instructions. It must do so by keeping track of the control flow modifications 
-to reverse them and by interfacing with static analysers.
-
-By embracing compilation, instead of avoiding it like EmBounded did, a CerCo 
-compiler can at the same time produce efficient code and return costs that are 
-as precise as the static analysis can be. Moreover, we allow our costs to be 
-parametric: the cost of a block can depend on actual program data or on a 
-summary of the execution history or on an approximated representation of the 
-hardware state. For example, loop optimizations may assign to a loop body a cost 
-that is a function of the number of iterations performed. As another example, 
-the cost of a block may be a function of the vector of stalled pipeline states, 
-which can be exposed in the source code and updated at each basic block exit. It 
-is parametricity that allows one to analyse small code fragments without losing 
-precision: in the analysis of the code fragment we do not have to ignore the 
-initial hardware state. On the contrary, we can assume that we know exactly which 
-state (or mode, as the WCET literature calls it) we are in.
 
 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.
 
+Traditional techniques for WCET that work on object code are also affected by 
+another problem: they cannot be applied before the generation of the object 
+code. Functional properties can be analysed in early development stages, while 
+analysis of non-functional properties may come too late to avoid expensive 
+changes to the program architecture.
+
+\subsection{CerCo}
+
+In CerCo we propose a radically new approach to the problem: we reject the idea 
+of a uniform cost model and we propose that the compiler, which knows how the 
+code is translated, must return the cost model for basic blocks of high level 
+instructions. It must do so by keeping track of the control flow modifications 
+to reverse them and by interfacing with static analysers.
+
+By embracing compilation, instead of avoiding it like EmBounded did, a CerCo 
+compiler can at the same time produce efficient code and return costs that are 
+as precise as the static analysis can be. Moreover, we allow our costs to be 
+parametric: the cost of a block can depend on actual program data or on a 
+summary of the execution history or on an approximated representation of the 
+hardware state. For example, loop optimizations may assign to a loop body a cost 
+that is a function of the number of iterations performed. As another example, 
+the cost of a block may be a function of the vector of stalled pipeline states, 
+which can be exposed in the source code and updated at each basic block exit. It 
+is parametricity that allows one to analyse small code fragments without losing 
+precision: in the analysis of the code fragment we do not have to ignore the 
+initial hardware state. On the contrary, we can assume that we know exactly which 
+state (or mode, as the WCET literature calls it) we are in.
+
 The CerCo approach has the potential to dramatically improve the state of the 
 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 
 at the source code level.
-
-Traditional techniques for WCET that work on object code are also affected by 
-another problem: they cannot be applied before the generation of the object 
-code. Functional properties can be analysed in early development stages, while 
-analysis of non-functional properties may come too late to avoid expensive 
-changes to the program architecture. Our approach already works in early 
-development stages by axiomatically attaching costs to unimplemented components.
+ Our approach can also work in the early 
+stages of development by axiomatically attaching costs to unimplemented components.
+
 
 All software used to verify properties of programs must be as bug free as