Changeset 3336


Ignore:
Timestamp:
Jun 7, 2013, 2:32:38 PM (4 years ago)
Author:
mulligan
Message:

80% done, synch. commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3335 r3336  
    552552
    553553\subsection{The (basic) labeling approach}
    554 The labeling approach is the main technique that
    555 underlies all the developments in CerCo. It allows to track the evolution of
    556 basic blocks during compilation in order to propagate the cost model from the
    557 object code to the source code without loosing precision in the process.
     554The labeling approach is the foundational insight that underlies all the developments in CerCo.
     555It allows the tracking of the evolution of
     556basic blocks during the compilation process in order to propagate the cost model from the
     557object code to the source code without losing precision in the process.
    558558\paragraph{Problem statement.} Given a source program $P$, we want to obtain an
    559559instrumented source program $P'$,  written in the same programming language, and
     
    567567to perform the corresponding operations (soundness property); 5) the difference
    568568between the costs computed by $P'$ and the execution costs of $O$ must be
    569 bounded by a program dependent constant (precision property).
    570 
    571 \paragraph{The labeling software components.} We solve the problem in four
     569bounded by a program-dependent constant (precision property).
     570
     571\paragraph{The labeling software components} We solve the problem in four
    572572stages \cite{labeling}, implemented by four software components that are used
    573573in sequence.
     
    615615The obtained source code is the instrumented source code.
    616616
    617 \paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement
     617\paragraph{Correctness} Requirements 1, 2 and 3 of the problem statement
    618618obviously hold, with 2 and 3 being a consequence of the definition of a correct
    619619labeling preserving compiler. It is also obvious that the value of the global
     
    641641compilation strategy and optimizations: the compiler may not duplicate any code
    642642that contains label emission statements, like loop bodies. Therefore several
    643 loop optimizations like peeling or unrolling are prevented. Moreover, precision
     643loop optimisations like peeling or unrolling are prevented. Moreover, precision
    644644of the object code labeling is not sufficient \emph{per se} to obtain global
    645645precision: we also implicitly assumed the static analysis to be able to
    646646associate a precise constant cost to every instruction. This is not possible in
    647 presence of stateful hardware whose state influences the cost of operations,
     647the presence of stateful hardware whose state influences the cost of operations,
    648648like pipelines and caches. In the next subsection we will see an extension of the
    649649basic labeling approach to cover this situation.
     
    652652with minor modifications to imperative and functional languages
    653653\cite{labeling2}. We have tested it on a simple imperative language without
    654 functions (a While language), on a subset of C and on two compilation chains for
    655 a purely functional higher order language. The two main changes required to deal
     654functions (a `while' language), on a subset of C and on two compilation chains for
     655a purely functional higher-order language. The two main changes required to deal
    656656with functional languages are: 1) because global variables and updates are not
    657 available, the instrumentation phase produces monadic code to “update” the
     657available, the instrumentation phase produces monadic code to `update' the
    658658global costs; 2) the requirements for a sound and precise labeling of the
    659659source code must be changed when the compilation is based on CPS translations.
    660 In particular, we need to introduce both labels emitted before a statement is
    661 executed and labels emitted after a statement is executed. The latter capture
     660In particular, we need to introduce labels emitted before a statement is
     661executed and also labels emitted after a statement is executed. The latter capture
    662662code that is inserted by the CPS translation and that would escape all label
    663663scopes.
     
    668668Therefore, the cost of executing computations that are later backtracked would
    669669not be correctly counted in. Any extension of logic languages with
    670 non-backtrackable state should support the labeling approach.
     670non-backtrackable state could support our labeling approach.
    671671
    672672\subsection{Dependent labeling}
     
    686686in correspondence with the source code state, but reconstructing the
    687687correspondence may be hard and lifting the cost model to work on the source code
    688 state is likely to produce cost expressions that are too hard to reason on.
     688state is likely to produce cost expressions that are too complex to understand and reason about.
    689689Luckily enough, in all modern architectures the cost of executing single
    690690instructions is either independent of the functional state or the jitter---the
    691691difference between the worst and best case execution times---is small enough
    692 to be bounded without loosing too much precision. Therefore we can concentrate
    693 on dependencies over the “non-functional” parts of the state only.
     692to be bounded without losing too much precision. Therefore we can concentrate
     693on dependencies over the `non-functional' parts of the state only.
    694694
    695695The non-functional state has no correspondence in the high level state and does
    696696not influence the functional properties. What can be done is to expose the
    697 non-functional state in the source code. We just present here the basic
    698 intuition in a simplified form: the technical details that allow to handle the
    699 general case are more complex and can be found in the CerCo deliverables. We add
     697non-functional state in the source code. We present here the basic
     698intuition in a simplified form: the technical details that allow us to handle the
     699general case are more complex and can be found in~\cite{paolo}. We add
    700700to the source code an additional global variable that represents the
    701701non-functional state and another one that remembers the last labels emitted. The
     
    721721
    722722Dependent labeling can also be applied to allow the compiler to duplicate
    723 blocks that contain labels (e.g. in loop optimizations) \cite{paolo}. The effect is to assign
     723blocks that contain labels (e.g. in loop optimisations)~\cite{paolo}. The effect is to assign
    724724a different cost to the different occurrences of a duplicated label. For
    725725example, loop peeling turns a loop into the concatenation of a copy of the loop
    726726body (that executes the first iteration) with the conditional execution of the
    727 loop (for the successive iterations). Because of further optimizations, the two
     727loop (for the successive iterations). Because of further optimisations, the two
    728728copies of the loop will be compiled differently, with the first body usually
    729729taking more time.
     
    733733same technique works for loop unrolling without modifications: the function will
    734734assign a cost to the even iterations and another cost to the odd ones. The
    735 actual work to be done consists in introducing in the source code and for each
    736 loop a variable that counts the number of iterations. The loop optimization code
     735actual work to be done consists of introducing within the source code, and for each
     736loop, a variable that counts the number of iterations. The loop optimisation code
    737737that duplicate the loop bodies must also modify the code to propagate correctly
    738738the update of the iteration numbers. The technical details are more complex and
    739739can be found in the CerCo reports and publications. The implementation, however,
    740 is quite simple and the changes to a loop optimizing compiler are minimal.
     740is quite simple and the changes to a loop optimising compiler are minimal.
    741741
    742742\subsection{Techniques to exploit the induced cost model}
     
    755755This principle entails that: 1)
    756756The inferred synthetic bounds are indeed correct as long as the general purpose
    757 tool is. 2) There is no limitation on the class of programs that can be handled
     757tool is; 2) there is no limitation on the class of programs that can be handled
    758758as long as the user is willing to carry on an interactive proof.
    759759
     
    765765a proof automatically, otherwise, user interaction is required.
    766766
    767 \paragraph{The Cost plugin and its application to the Lustre compiler.}
     767\paragraph{The Cost plugin and its application to the Lustre compiler}
    768768Frama-C \cite{framac} is a set of analysers for C programs with a
    769769specification language called ACSL. New analyses can be dynamically added
Note: See TracChangeset for help on using the changeset viewer.