# Changeset 3432 for Papers

Ignore:
Timestamp:
Feb 14, 2014, 12:09:27 PM (6 years ago)
Message:

Consistently use ll spelling of labelled/labelling.

Location:
Papers/fopara2013
Files:
2 edited

### Legend:

Unmodified
 r3431 components. \paragraph{Contributions.} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a \paragraph{Contributions.} We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a technique to implement compilers that induce cost models on source programs by very lightweight tracking of code changes through compilation. We have studied \lstinline'count' say that 4 bytes of stack are required, and that it takes 111 cycles to reach the next cost annotation (in the loop body). The compiler measures these on the labeled object code that it generates. The compiler measures these on the labelled object code that it generates. The annotated program can then be enriched with complexity \end{figure} \section{Main scientific and technical results} First we describe the basic labeling approach and our compiler First we describe the basic labelling approach and our compiler implementations that use it.  This is suitable for basic architectures with simple cost models.  Then we will discuss the dependent labeling with simple cost models.  Then we will discuss the dependent labelling extension which is suitable for more advanced processor architectures and compiler optimisations.  At the end of this section we will costs provided by the compilers. % \emph{Dependent labeling~\cite{?}.} The basic labeling approach assumes a % \emph{Dependent labelling~\cite{?}.} The basic labelling approach assumes a % bijective mapping between object code and source code O(1) blocks (called basic % blocks). This assumption is violated by many program optimizations (e.g. loop % object code to be non parametric: every block must be assigned a cost that does % not depend on the state. This assumption is violated by stateful hardware like % pipelines, caches, branch prediction units. The dependent labeling approach is % an extension of the basic labeling approach that allows to handle parametric % pipelines, caches, branch prediction units. The dependent labelling approach is % an extension of the basic labelling approach that allows to handle parametric % cost models. We showed how the method allows to deal with loop optimizations and % pipelines, and we speculated about its applications to caches. % the analysis of functional properties of programs can be adapted to analyse the % non-functional properties of the source code instrumented by compilers that % implement the labeling approach. In order to gain confidence in this claim, we % implement the labelling approach. In order to gain confidence in this claim, we % showed how to implement a cost invariant generator combining abstract % interpretation with separation logic ideas \cite{separation}. We integrated % automatically analyse the reaction time of Lustre nodes that are first compiled % to C using a standard Lustre compiler and then processed by a C compiler that % implements the labeling approach. % implements the labelling approach. % \emph{The CerCo compiler.} This is a compiler from a large subset of the C % program to 8051/8052 object code, % integrating the labeling approach and a static analyser for 8051 executables. % integrating the labelling approach and a static analyser for 8051 executables. % The latter can be implemented easily and does not require dependent costs % because the 8051 microprocessor is a very simple one, with constant-cost % that may require approximations or dependent costs. The compiler comes in % several versions: some are prototypes implemented directly in OCaml, and they % implement both the basic and dependent labeling approaches; the final version % implement both the basic and dependent labelling approaches; the final version % is extracted from a Matita certification and at the moment implements only the % basic approach. \subsection{The (basic) labeling approach} The labeling approach is the foundational insight that underlies all the developments in CerCo. \subsection{The (basic) labelling approach} The labelling 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 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 \paragraph{The labelling software components.} We solve the problem in four stages \cite{labelling}, implemented by four software components that are used in sequence. statements in appropriate positions to mark the beginning of basic blocks. % The % set of labels with their positions is called labeling. % set of labels with their positions is called labelling. The syntax and semantics of the source programming language is augmented with label emission statements. % Therefore the observables of a run of a program becomes a stream % of label emissions: $\ell_1,\ldots,\ell_n$, called the program trace. We clarify the conditions % that the labeling must respect later. The second component is a labeling preserving compiler. It can be obtained from % that the labelling must respect later. The second component is a labelling preserving compiler. It can be obtained from an existing compiler by adding label emission statements to every intermediate language and by propagating label emission statements during compilation. The % We may also ask that the function that erases the cost % emission statements commute with compilation. This optional property grants that % the labeling does not interfere with the original compiler behaviour. A further % the labelling does not interfere with the original compiler behaviour. A further % set of requirements will be added later. The third component is a static object code analyser. It takes as input a labeled The third component is a static object code analyser. It takes as input a labelled object code and it computes the scope of each of its label emission statements, i.e.\ the tree of instructions that may be executed after the statement and before may contain a branching statement. In order to grant that such a finite tree exists, the object code must not contain any loop that is not broken by a label emission statement. This is the first requirement of a sound labeling. The analyser fails if the labeling is unsound. For each scope, the analyser emission statement. This is the first requirement of a sound labelling. The analyser fails if the labelling is unsound. For each scope, the analyser computes an upper bound of the execution time required by the scope, using the maximum of the costs of the two branches in case of a conditional 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 labelling preserving compiler. It is also obvious that the value of the global cost variable of an instrumented source code is at any time equal to the sum of the costs of the labels emitted by the corresponding labelled code. Moreover, the object code is equal to the sum of the costs of the labels emitted by the object code. We collect all the necessary conditions for this to happen in the definition of a sound labeling: a) all loops must be broken by a cost emission definition of a sound labelling: a) all loops must be broken by a cost emission statement;  b) all program instructions must be in the scope of some cost emission statement. To satisfy also the fifth requirement, additional requirements must be imposed on the object code labeling to avoid all uses of the maximum in the cost computation: the labeling is precise if every label is requirements must be imposed on the object code labelling to avoid all uses of the maximum in the cost computation: the labelling is precise if every label is emitted at most once and both branches of a conditional jump start with a label emission statement. The correctness and precision of the labeling approach only rely on the correctness and precision of the object code labeling. The simplest The correctness and precision of the labelling approach only rely on the correctness and precision of the object code labelling. The simplest way to achieve them is to impose correctness and precision requirements also on the initial labeling produced by the first software requirements also on the initial labelling produced by the first software component, and to ask the compiler to preserve these properties too. The latter requirement imposes serious limitations on the that contains label emission statements, like loop bodies. Therefore several loop optimisations like peeling or unrolling are prevented. Moreover, precision of the object code labeling is not sufficient \emph{per se} to obtain global of the object code labelling is not sufficient \emph{per se} to obtain global precision: we implicitly assumed that a precise constant cost can be assigned to every instruction. This is not possible in the presence of stateful hardware whose state influences the cost of operations, like pipelines and caches. In Section~\ref{lab:deplabel} we will see an extension of the basic labeling approach to cover this situation. basic labelling approach to cover this situation. In CerCo we have developed several cost preserving compilers based on the labeling approach. Excluding an initial certified compiler for a the labelling approach. Excluding an initial certified compiler for a while' language, all remaining compilers target realistic source languages---a pure higher order functional language and a large subset Two compilation chains were implemented for a purely functional higher-order language~\cite{labeling2}. The two main changes required higher-order language~\cite{labelling2}. 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 global costs; 2) the requirements for a sound and precise labeling of the source code must be changed when the precise labelling of the source code must be changed when the compilation is based on CPS translations.  In particular, we need to introduce labels emitted before a statement is executed and also % 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 could support our labeling approach. % non-backtrackable state could support our labelling approach. \subsection{The CerCo C compilers} Matita~\cite{matita}.  The first acted as a prototype for the second, but also supported MIPS and acted as a testbed for more advanced features such as the dependent labeling approach features such as the dependent labelling approach in Section~\ref{lab:deplabel}. \begin{enumerate} \item All the intermediate languages include label emitting instructions to implement the labeling approach, and the compiler preserves execution traces. implement the labelling approach, and the compiler preserves execution traces. \item Traditionally compilers target an assembly language with additional macro-instructions to be expanded before assembly; for CerCo we need to go all and a loader, we do not support separate compilation and external calls. Adding them is orthogonal to the labeling approach and should not introduce extra problems. to the labelling approach and should not introduce extra problems. \item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. This requires many changes and more compiler code, but it is not fundamentally more space is a clear requirement of meaningfulness of a run, because source programs do not crash for lack of space while object code ones do. The balancing of function calls and returns is a requirement for precision: the labeling approach function calls and returns is a requirement for precision: the labelling approach allows the scope of label emission statements to extend after function calls to minimize the number of labels. Therefore a label pays for all the instructions not I/O times, as desired. \subsection{Dependent labeling} \subsection{Dependent labelling} \label{lab:deplabel} The core idea of the basic labeling approach is to establish a tight connection The core idea of the basic labelling approach is to establish a tight connection between basic blocks executed in the source and target languages. Once the connection is established, any cost model computed on the object code can be use more aggressive approximations for the ones that are executed least. Dependent labeling can also be applied to allow the compiler to duplicate Dependent labelling can also be applied to allow the compiler to duplicate 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 We now turn our attention to synthesising high-level costs, such as the execution time of a whole program.  We consider as our starting point source level costs provided by basic labeling, in other words annotations provided by basic labelling, in other words annotations on the source code which are constants that provide a sound and sufficiently precise upper bound on the cost of executing the blocks after compilation to characterized by history dependent stateful components, like caches and pipelines. The main issue is to assign a parametric, dependent cost to basic blocks that can be later transferred by the labeling approach to to basic blocks that can be later transferred by the labelling approach to the source code and represented in a meaningful way to the user. The dependent labeling approach that we have studied seems a promising tool to achieve labelling approach that we have studied seems a promising tool to achieve this goal, but more work is required to provide good source level approximations of the relevant processor state. Other examples of future work are to improve the cost invariant generator algorithms and the coverage of compiler optimizations, to combining the labeling approach with the type and effect discipline of~\cite{typeffects} the labelling approach with the type and effect discipline of~\cite{typeffects} to handle languages with implicit memory management, and to experiment with our tools in the early phases of development. Larger case studies are also necessary % European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177. % % \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C % \bibitem{labelling} \textbf{Certifying and Reasoning on Cost Annotations in C % Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer % LNCS % %, DOI:10.1007/978-3-642-32469-7\_3. % % \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of % \bibitem{labelling2} \textbf{Certifying and reasoning on cost annotations of % functional programs}. % R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference