Changeset 3435


Ignore:
Timestamp:
Feb 14, 2014, 5:37:31 PM (5 years ago)
Author:
campbell
Message:

Revise section 4.4.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3434 r3435  
    887887connection is established, any cost model computed on the object code can be
    888888transferred to the source code, without affecting the code of the compiler or
    889 its proof. In particular, it is immediate that we can also transport cost models
    890 that associate to each label functions from hardware state to natural numbers.
    891 However, a problem arises during the instrumentation phase that replaces cost
    892 emission statements with increments of global cost variables. The global cost
    893 variable must be incremented with the result of applying the function associated
    894 to the label to the hardware state at the time of execution of the block.
    895 The hardware state comprises both the functional state that affects the
     889its proof. In particular, we can also transport cost models
     890that associate to each label a \emph{function} from the hardware state
     891to a natural number.
     892However, a problem arises during the instrumentation phase that replaces label
     893emission statements with increments of global cost variables. They are
     894incremented by the result of applying the label's cost function
     895to the hardware state at the time of execution of the block. However,
     896the hardware state comprises both the functional state that affects the
    896897computation (the value of the registers and memory) and the non-functional
    897 state that does not (the pipeline and cache contents, for example). The former is
    898 in correspondence with the source code state, but reconstructing the
     898state that does not (the pipeline and cache contents, for example).
     899We can find corresponding information for the former in the source code state, but constructing the
    899900correspondence may be hard and lifting the cost model to work on the source code
    900901state is likely to produce cost expressions that are too complex to understand and reason about.
    901 Fortunately, in all modern architectures the cost of executing single
     902Fortunately, in modern architectures the cost of executing single
    902903instructions is either independent of the functional state or the jitter---the
    903904difference between the worst and best case execution times---is small enough
     
    914915state and another one that remembers the last few labels emitted. The
    915916state variable must be updated at every label emission statement,
    916 using an update function which is computed during static analysis
    917 too. The update function associates to each label a function from the
     917using an update function which is computed during the processor timing
     918analysis.
     919This update function assigns to each label a function from the
    918920recently emitted labels and old state to the new state. It is computed
    919 by composing the semantics of every instruction in a basic block and
    920 restricting it to the non-functional part of the state.
     921by composing the semantics of every instruction in a basic block
     922restricted to the non-functional part of the state.
    921923
    922924Not all the details of the non-functional state needs to be exposed, and the
     
    927929for the user to understand the meaning of the state to reason over the properties
    928930of the
    929 program. Moreover, at any moment the user, or the invariant generator tools that
     931program. Moreover, the user, or the invariant generator tools that
    930932analyse the instrumented source code produced by the compiler, can decide to
    931933trade precision of the analysis for simplicity by approximating the
    932 cost with safe bounds that do not depend on the processor state. Interestingly, the functional analysis of
     934cost by safe bounds that do not depend on the processor state. Interestingly, the functional analysis of
    933935the code could determine which blocks are executed more frequently in order to
    934 use more aggressive approximations for the ones that are executed least.
     936use more aggressive approximations for those that are executed least.
    935937
    936938Dependent labelling can also be applied to allow the compiler to duplicate
     
    945947By introducing a variable that keeps track of the iteration number, we can
    946948associate to the label a cost that is a function of the iteration number. The
    947 same technique works for loop unrolling without modifications: the function will
    948 assign a cost to the even iterations and another cost to the odd ones. The
    949 actual work to be done consists of introducing within the source code, and for each
    950 loop, a variable that counts the number of iterations. The loop optimisation code
     949same technique works for loop unrolling without modification: the function will
     950assign one cost to the even iterations and another cost to the odd
     951ones.  The loop optimisation code
    951952that duplicate the loop bodies must also modify the code to correctly propagate
    952 the update of the iteration numbers. The technical details are more complex and
     953the update of the iteration numbers. The technical details are more complicated and
    953954can be found in the CerCo reports and publications. The implementation, however,
    954955is quite simple (and forms part of our OCaml version of the compiler)
Note: See TracChangeset for help on using the changeset viewer.