Changeset 3435

Timestamp:

Feb 14, 2014, 5:37:31 PM (7 years ago)

Author:

campbell

Message:

Revise section 4.4.

File:

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

Papers/fopara2013/fopara13.tex

@@ -887 +887 @@
 connection is established, any cost model computed on the object code can be 
 transferred to the source code, without affecting the code of the compiler or 
-its proof. In particular, it is immediate that we can also transport cost models 
-that associate to each label functions from hardware state to natural numbers. 
-However, a problem arises during the instrumentation phase that replaces cost 
-emission statements with increments of global cost variables. The global cost 
-variable must be incremented with the result of applying the function associated 
-to the label to the hardware state at the time of execution of the block.
-The hardware state comprises both the functional state that affects the 
+its proof. In particular, we can also transport cost models 
+that associate to each label a \emph{function} from the hardware state
+to a natural number. 
+However, a problem arises during the instrumentation phase that replaces label
+emission statements with increments of global cost variables. They are
+incremented by the result of applying the label's cost function
+to the hardware state at the time of execution of the block. However,
+the hardware state comprises both the functional state that affects the 
 computation (the value of the registers and memory) and the non-functional
-state that does not (the pipeline and cache contents, for example). The former is 
-in correspondence with the source code state, but reconstructing the 
+state that does not (the pipeline and cache contents, for example).
+We can find corresponding information for the former in the source code state, but constructing the 
 correspondence may be hard and lifting the cost model to work on the source code 
 state is likely to produce cost expressions that are too complex to understand and reason about. 
-Fortunately, in all modern architectures the cost of executing single 
+Fortunately, in modern architectures the cost of executing single 
 instructions is either independent of the functional state or the jitter---the 
 difference between the worst and best case execution times---is small enough 
@@ -914 +915 @@
 state and another one that remembers the last few labels emitted. The
 state variable must be updated at every label emission statement,
-using an update function which is computed during static analysis
-too. The update function associates to each label a function from the
+using an update function which is computed during the processor timing
+analysis.
+This update function assigns to each label a function from the
 recently emitted labels and old state to the new state. It is computed
-by composing the semantics of every instruction in a basic block and
-restricting it to the non-functional part of the state.
+by composing the semantics of every instruction in a basic block
+restricted to the non-functional part of the state.
 
 Not all the details of the non-functional state needs to be exposed, and the 
@@ -927 +929 @@
 for the user to understand the meaning of the state to reason over the properties
 of the 
-program. Moreover, at any moment the user, or the invariant generator tools that 
+program. Moreover, the user, or the invariant generator tools that 
 analyse the instrumented source code produced by the compiler, can decide to 
 trade precision of the analysis for simplicity by approximating the
-cost with safe bounds that do not depend on the processor state. Interestingly, the functional analysis of 
+cost by safe bounds that do not depend on the processor state. Interestingly, the functional analysis of 
 the code could determine which blocks are executed more frequently in order to 
-use more aggressive approximations for the ones that are executed least.
+use more aggressive approximations for those that are executed least.
 
 Dependent labelling can also be applied to allow the compiler to duplicate 
@@ -945 +947 @@
 By introducing a variable that keeps track of the iteration number, we can 
 associate to the label a cost that is a function of the iteration number. The 
-same technique works for loop unrolling without modifications: the function will 
-assign a cost to the even iterations and another cost to the odd ones. The 
-actual work to be done consists of introducing within the source code, and for each 
-loop, a variable that counts the number of iterations. The loop optimisation code 
+same technique works for loop unrolling without modification: the function will 
+assign one cost to the even iterations and another cost to the odd
+ones.  The loop optimisation code 
 that duplicate the loop bodies must also modify the code to correctly propagate
-the update of the iteration numbers. The technical details are more complex and 
+the update of the iteration numbers. The technical details are more complicated and 
 can be found in the CerCo reports and publications. The implementation, however, 
 is quite simple (and forms part of our OCaml version of the compiler)