Changeset 3432 for Papers/fopara2013


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

Consistently use ll spelling of labelled/labelling.

Location:
Papers/fopara2013
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.bib

    r3431 r3432  
    2525}
    2626
    27 @incollection{labeling,
     27@incollection{labelling,
    2828year={2012},
    2929isbn={978-3-642-32468-0},
     
    4040}
    4141
    42 @incollection{labeling2,
     42@incollection{labelling2,
    4343year={2012},
    4444isbn={978-3-642-32494-9},
  • Papers/fopara2013/fopara13.tex

    r3431 r3432  
    159159components.
    160160
    161 \paragraph{Contributions.} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a
     161\paragraph{Contributions.} We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a
    162162technique to implement compilers that induce cost models on source programs by
    163163very lightweight tracking of code changes through compilation. We have studied
     
    454454\lstinline'count' say that 4 bytes of stack are required, and that it
    455455takes 111 cycles to reach the next cost annotation (in the loop body).
    456 The compiler measures these on the labeled object code that it generates.
     456The compiler measures these on the labelled object code that it generates.
    457457
    458458 The annotated program can then be enriched with complexity
     
    550550\end{figure}
    551551\section{Main scientific and technical results}
    552 First we describe the basic labeling approach and our compiler
     552First we describe the basic labelling approach and our compiler
    553553implementations that use it.  This is suitable for basic architectures
    554 with simple cost models.  Then we will discuss the dependent labeling
     554with simple cost models.  Then we will discuss the dependent labelling
    555555extension which is suitable for more advanced processor architectures
    556556and compiler optimisations.  At the end of this section we will
     
    558558costs provided by the compilers.
    559559
    560 % \emph{Dependent labeling~\cite{?}.} The basic labeling approach assumes a
     560% \emph{Dependent labelling~\cite{?}.} The basic labelling approach assumes a
    561561% bijective mapping between object code and source code O(1) blocks (called basic
    562562% blocks). This assumption is violated by many program optimizations (e.g. loop
     
    564564% object code to be non parametric: every block must be assigned a cost that does
    565565% not depend on the state. This assumption is violated by stateful hardware like
    566 % pipelines, caches, branch prediction units. The dependent labeling approach is
    567 % an extension of the basic labeling approach that allows to handle parametric
     566% pipelines, caches, branch prediction units. The dependent labelling approach is
     567% an extension of the basic labelling approach that allows to handle parametric
    568568% cost models. We showed how the method allows to deal with loop optimizations and
    569569% pipelines, and we speculated about its applications to caches.
     
    572572% the analysis of functional properties of programs can be adapted to analyse the
    573573% non-functional properties of the source code instrumented by compilers that
    574 % implement the labeling approach. In order to gain confidence in this claim, we
     574% implement the labelling approach. In order to gain confidence in this claim, we
    575575% showed how to implement a cost invariant generator combining abstract
    576576% interpretation with separation logic ideas \cite{separation}. We integrated
     
    582582% automatically analyse the reaction time of Lustre nodes that are first compiled
    583583% to C using a standard Lustre compiler and then processed by a C compiler that
    584 % implements the labeling approach.
     584% implements the labelling approach.
    585585
    586586% \emph{The CerCo compiler.} This is a compiler from a large subset of the C
    587587% program to 8051/8052 object code,
    588 % integrating the labeling approach and a static analyser for 8051 executables.
     588% integrating the labelling approach and a static analyser for 8051 executables.
    589589% The latter can be implemented easily and does not require dependent costs
    590590% because the 8051 microprocessor is a very simple one, with constant-cost
     
    593593% that may require approximations or dependent costs. The compiler comes in
    594594% several versions: some are prototypes implemented directly in OCaml, and they
    595 % implement both the basic and dependent labeling approaches; the final version
     595% implement both the basic and dependent labelling approaches; the final version
    596596% is extracted from a Matita certification and at the moment implements only the
    597597% basic approach.
    598598
    599 \subsection{The (basic) labeling approach}
    600 The labeling approach is the foundational insight that underlies all the developments in CerCo.
     599\subsection{The (basic) labelling approach}
     600The labelling approach is the foundational insight that underlies all the developments in CerCo.
    601601It allows the tracking of the evolution of
    602602basic blocks during the compilation process in order to propagate the cost model from the
     
    615615bounded by a program-dependent constant (precision property).
    616616
    617 \paragraph{The labeling software components.} We solve the problem in four
    618 stages \cite{labeling}, implemented by four software components that are used
     617\paragraph{The labelling software components.} We solve the problem in four
     618stages \cite{labelling}, implemented by four software components that are used
    619619in sequence.
    620620
     
    622622statements in appropriate positions to mark the beginning of basic blocks.
    623623% The
    624 % set of labels with their positions is called labeling.
     624% set of labels with their positions is called labelling.
    625625The syntax and semantics
    626626of the source programming language is augmented with label emission statements.
     
    629629% Therefore the observables of a run of a program becomes a stream
    630630% of label emissions: $\ell_1,\ldots,\ell_n$, called the program trace. We clarify the conditions
    631 % that the labeling must respect later.
    632 
    633 The second component is a labeling preserving compiler. It can be obtained from
     631% that the labelling must respect later.
     632
     633The second component is a labelling preserving compiler. It can be obtained from
    634634an existing compiler by adding label emission statements to every intermediate
    635635language and by propagating label emission statements during compilation. The
     
    638638% We may also ask that the function that erases the cost
    639639% emission statements commute with compilation. This optional property grants that
    640 % the labeling does not interfere with the original compiler behaviour. A further
     640% the labelling does not interfere with the original compiler behaviour. A further
    641641% set of requirements will be added later.
    642642
    643 The third component is a static object code analyser. It takes as input a labeled
     643The third component is a static object code analyser. It takes as input a labelled
    644644object code and it computes the scope of each of its label emission statements,
    645645i.e.\ the tree of instructions that may be executed after the statement and before
     
    648648may contain a branching statement. In order to grant that such a finite tree
    649649exists, the object code must not contain any loop that is not broken by a label
    650 emission statement. This is the first requirement of a sound labeling. The
    651 analyser fails if the labeling is unsound. For each scope, the analyser
     650emission statement. This is the first requirement of a sound labelling. The
     651analyser fails if the labelling is unsound. For each scope, the analyser
    652652computes an upper bound of the execution time required by the scope, using the
    653653maximum of the costs of the two branches in case of a conditional statement.
     
    663663\paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement
    664664obviously hold, with 2 and 3 being a consequence of the definition of a correct
    665 labeling preserving compiler. It is also obvious that the value of the global
     665labelling preserving compiler. It is also obvious that the value of the global
    666666cost variable of an instrumented source code is at any time equal to the sum of
    667667the costs of the labels emitted by the corresponding labelled code. Moreover,
     
    671671the object code is equal to the sum of the costs of the labels emitted by the
    672672object code. We collect all the necessary conditions for this to happen in the
    673 definition of a sound labeling: a) all loops must be broken by a cost emission
     673definition of a sound labelling: a) all loops must be broken by a cost emission
    674674statement;  b) all program instructions must be in the scope of some cost
    675675emission statement. To satisfy also the fifth requirement, additional
    676 requirements must be imposed on the object code labeling to avoid all uses of
    677 the maximum in the cost computation: the labeling is precise if every label is
     676requirements must be imposed on the object code labelling to avoid all uses of
     677the maximum in the cost computation: the labelling is precise if every label is
    678678emitted at most once and both branches of a conditional jump start with a label
    679679emission statement.
    680680
    681 The correctness and precision of the labeling approach only rely on the
    682 correctness and precision of the object code labeling. The simplest
     681The correctness and precision of the labelling approach only rely on the
     682correctness and precision of the object code labelling. The simplest
    683683way to achieve them is to impose correctness and precision
    684 requirements also on the initial labeling produced by the first software
     684requirements also on the initial labelling produced by the first software
    685685component, and to ask the compiler to preserve these
    686686properties too. The latter requirement imposes serious limitations on the
     
    688688that contains label emission statements, like loop bodies. Therefore several
    689689loop optimisations like peeling or unrolling are prevented. Moreover, precision
    690 of the object code labeling is not sufficient \emph{per se} to obtain global
     690of the object code labelling is not sufficient \emph{per se} to obtain global
    691691precision: we implicitly assumed that a precise constant cost can be assigned
    692692to every instruction. This is not possible in
    693693the presence of stateful hardware whose state influences the cost of operations,
    694694like pipelines and caches. In Section~\ref{lab:deplabel} we will see an extension of the
    695 basic labeling approach to cover this situation.
     695basic labelling approach to cover this situation.
    696696
    697697In CerCo we have developed several cost preserving compilers based on
    698 the labeling approach. Excluding an initial certified compiler for a
     698the labelling approach. Excluding an initial certified compiler for a
    699699`while' language, all remaining compilers target realistic source
    700700languages---a pure higher order functional language and a large subset
     
    707707
    708708Two compilation chains were implemented for a purely functional
    709 higher-order language~\cite{labeling2}. The two main changes required
     709higher-order language~\cite{labelling2}. The two main changes required
    710710to deal with functional languages are: 1) because global variables and
    711711updates are not available, the instrumentation phase produces monadic
    712712code to `update' the global costs; 2) the requirements for a sound and
    713 precise labeling of the source code must be changed when the
     713precise labelling of the source code must be changed when the
    714714compilation is based on CPS translations.  In particular, we need to
    715715introduce labels emitted before a statement is executed and also
     
    728728% Therefore, the cost of executing computations that are later backtracked would
    729729% not be correctly counted in. Any extension of logic languages with
    730 % non-backtrackable state could support our labeling approach.
     730% non-backtrackable state could support our labelling approach.
    731731
    732732\subsection{The CerCo C compilers}
     
    735735Matita~\cite{matita}.  The first acted as a prototype for the second,
    736736but also supported MIPS and acted as a testbed for more advanced
    737 features such as the dependent labeling approach
     737features such as the dependent labelling approach
    738738in Section~\ref{lab:deplabel}.
    739739
     
    772772\begin{enumerate}
    773773\item All the intermediate languages include label emitting instructions to
    774 implement the labeling approach, and the compiler preserves execution traces.
     774implement the labelling approach, and the compiler preserves execution traces.
    775775\item Traditionally compilers target an assembly language with additional
    776776macro-instructions to be expanded before assembly; for CerCo we need to go all
     
    780780 and a loader, we do not support separate
    781781compilation and external calls. Adding them is orthogonal
    782 to the labeling approach and should not introduce extra problems.
     782to the labelling approach and should not introduce extra problems.
    783783\item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. This requires
    784784many changes and more compiler code, but it is not fundamentally more
     
    850850space is a clear requirement of meaningfulness of a run, because source programs
    851851do not crash for lack of space while object code ones do. The balancing of
    852 function calls and returns is a requirement for precision: the labeling approach
     852function calls and returns is a requirement for precision: the labelling approach
    853853allows the scope of label emission statements to extend after function calls to
    854854minimize the number of labels. Therefore a label pays for all the instructions
     
    868868not I/O times, as desired.
    869869
    870 \subsection{Dependent labeling}
     870\subsection{Dependent labelling}
    871871\label{lab:deplabel}
    872 The core idea of the basic labeling approach is to establish a tight connection
     872The core idea of the basic labelling approach is to establish a tight connection
    873873between basic blocks executed in the source and target languages. Once the
    874874connection is established, any cost model computed on the object code can be
     
    921921use more aggressive approximations for the ones that are executed least.
    922922
    923 Dependent labeling can also be applied to allow the compiler to duplicate
     923Dependent labelling can also be applied to allow the compiler to duplicate
    924924blocks that contain labels (e.g. in loop optimisations)~\cite{paolo}. The effect is to assign
    925925a different cost to the different occurrences of a duplicated label. For
     
    945945We now turn our attention to synthesising high-level costs, such as
    946946the execution time of a whole program.  We consider as our starting point source level costs
    947 provided by basic labeling, in other words annotations
     947provided by basic labelling, in other words annotations
    948948on the source code which are constants that provide a sound and sufficiently
    949949precise upper bound on the cost of executing the blocks after compilation to
     
    10781078characterized by history dependent stateful components, like caches and
    10791079pipelines. The main issue is to assign a parametric, dependent cost
    1080 to basic blocks that can be later transferred by the labeling approach to
     1080to basic blocks that can be later transferred by the labelling approach to
    10811081the source code and represented in a meaningful way to the user. The dependent
    1082 labeling approach that we have studied seems a promising tool to achieve
     1082labelling approach that we have studied seems a promising tool to achieve
    10831083this goal, but more work is required to provide good source level
    10841084approximations of the relevant processor state.
     
    10861086Other examples of future work are to improve the cost invariant
    10871087generator algorithms and the coverage of compiler optimizations, to combining
    1088 the labeling approach with the type and effect discipline of~\cite{typeffects}
     1088the labelling approach with the type and effect discipline of~\cite{typeffects}
    10891089to handle languages with implicit memory management, and to experiment with
    10901090our tools in the early phases of development. Larger case studies are also necessary
     
    11031103% European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177.
    11041104%
    1105 % \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C
     1105% \bibitem{labelling} \textbf{Certifying and Reasoning on Cost Annotations in C
    11061106% Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer
    11071107% LNCS
     
    11091109% %, DOI:10.1007/978-3-642-32469-7\_3.
    11101110%
    1111 % \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of
     1111% \bibitem{labelling2} \textbf{Certifying and reasoning on cost annotations of
    11121112% functional programs}.
    11131113% R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference
Note: See TracChangeset for help on using the changeset viewer.