# Changeset 3336

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

80% done, synch. commit

File:
1 edited

### Legend:

Unmodified
 r3335 \subsection{The (basic) labeling approach} The labeling approach is the main technique that underlies all the developments in CerCo. It allows to track the evolution of basic blocks during compilation in order to propagate the cost model from the object code to the source code without loosing precision in the process. The labeling approach is the foundational insight that underlies all the developments in CerCo. It allows the tracking of the evolution of basic blocks during the compilation process in order to propagate the cost model from the object code to the source code without losing precision in the process. \paragraph{Problem statement.} Given a source program $P$, we want to obtain an instrumented source program $P'$,  written in the same programming language, and to perform the corresponding operations (soundness property); 5) the difference between the costs computed by $P'$ and the execution costs of $O$ must be bounded by a program dependent constant (precision property). \paragraph{The labeling software components.} We solve the problem in four bounded by a program-dependent constant (precision property). \paragraph{The labeling software components} We solve the problem in four stages \cite{labeling}, implemented by four software components that are used in sequence. The obtained source code is the instrumented source code. \paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement \paragraph{Correctness} Requirements 1, 2 and 3 of the problem statement obviously hold, with 2 and 3 being a consequence of the definition of a correct labeling preserving compiler. It is also obvious that the value of the global compilation strategy and optimizations: the compiler may not duplicate any code that contains label emission statements, like loop bodies. Therefore several loop optimizations like peeling or unrolling are prevented. Moreover, precision loop optimisations like peeling or unrolling are prevented. Moreover, precision of the object code labeling is not sufficient \emph{per se} to obtain global precision: we also implicitly assumed the static analysis to be able to associate a precise constant cost to every instruction. This is not possible in presence of stateful hardware whose state influences the cost of operations, the presence of stateful hardware whose state influences the cost of operations, like pipelines and caches. In the next subsection we will see an extension of the basic labeling approach to cover this situation. with minor modifications to imperative and functional languages \cite{labeling2}. We have tested it on a simple imperative language without functions (a While language), on a subset of C and on two compilation chains for a purely functional higher order language. The two main changes required to deal functions (a while' language), on a subset of C and on two compilation chains for a purely functional higher-order language. The two main changes required to deal with functional languages are: 1) because global variables and updates are not available, the instrumentation phase produces monadic code to “update” the available, the instrumentation phase produces monadic code to update' the global costs; 2) the requirements for a sound and precise labeling of the source code must be changed when the compilation is based on CPS translations. In particular, we need to introduce both labels emitted before a statement is executed and labels emitted after a statement is executed. The latter capture In particular, we need to introduce labels emitted before a statement is executed and also labels emitted after a statement is executed. The latter capture code that is inserted by the CPS translation and that would escape all label scopes. Therefore, the cost of executing computations that are later backtracked would not be correctly counted in. Any extension of logic languages with non-backtrackable state should support the labeling approach. non-backtrackable state could support our labeling approach. \subsection{Dependent labeling} in correspondence with the source code state, but reconstructing 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 hard to reason on. state is likely to produce cost expressions that are too complex to understand and reason about. Luckily enough, in all 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 to be bounded without loosing too much precision. Therefore we can concentrate on dependencies over the “non-functional” parts of the state only. to be bounded without losing too much precision. Therefore we can concentrate on dependencies over the `non-functional' parts of the state only. The non-functional state has no correspondence in the high level state and does not influence the functional properties. What can be done is to expose the non-functional state in the source code. We just present here the basic intuition in a simplified form: the technical details that allow to handle the general case are more complex and can be found in the CerCo deliverables. We add non-functional state in the source code. We present here the basic intuition in a simplified form: the technical details that allow us to handle the general case are more complex and can be found in~\cite{paolo}. We add to the source code an additional global variable that represents the non-functional state and another one that remembers the last labels emitted. The Dependent labeling can also be applied to allow the compiler to duplicate blocks that contain labels (e.g. in loop optimizations) \cite{paolo}. The effect is to assign blocks that contain labels (e.g. in loop optimisations)~\cite{paolo}. The effect is to assign a different cost to the different occurrences of a duplicated label. For example, loop peeling turns a loop into the concatenation of a copy of the loop body (that executes the first iteration) with the conditional execution of the loop (for the successive iterations). Because of further optimizations, the two loop (for the successive iterations). Because of further optimisations, the two copies of the loop will be compiled differently, with the first body usually taking more time. 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 in introducing in the source code and for each loop a variable that counts the number of iterations. The loop optimization code 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 that duplicate the loop bodies must also modify the code to propagate correctly the update of the iteration numbers. The technical details are more complex and can be found in the CerCo reports and publications. The implementation, however, is quite simple and the changes to a loop optimizing compiler are minimal. is quite simple and the changes to a loop optimising compiler are minimal. \subsection{Techniques to exploit the induced cost model} This principle entails that: 1) The inferred synthetic bounds are indeed correct as long as the general purpose tool is. 2) There is no limitation on the class of programs that can be handled tool is; 2) there is no limitation on the class of programs that can be handled as long as the user is willing to carry on an interactive proof. a proof automatically, otherwise, user interaction is required. \paragraph{The Cost plugin and its application to the Lustre compiler.} \paragraph{The Cost plugin and its application to the Lustre compiler} Frama-C \cite{framac} is a set of analysers for C programs with a specification language called ACSL. New analyses can be dynamically added