Ignore:
Timestamp:
Feb 14, 2014, 2:43:25 PM (6 years ago)
Author:
campbell
Message:

Revise sections 4.1, 4.2.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3432 r3433  
    362362
    363363\section{The typical CerCo workflow}
     364\label{sec:workflow}
    364365\begin{figure}[!t]
    365366\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
     
    611612behaviour; 4) after execution and in interesting points during execution, the
    612613cost information computed by $P'$ must be an upper bound of the one spent by $O$
    613 to perform the corresponding operations (soundness property); 5) the difference
     614to perform the corresponding operations (\emph{soundness} property); 5) the difference
    614615between the costs computed by $P'$ and the execution costs of $O$ must be
    615 bounded by a program-dependent constant (precision property).
     616bounded by a program-dependent constant (\emph{precision} property).
    616617
    617618\paragraph{The labelling software components.} We solve the problem in four
     
    621622The first component labels the source program $P$ by injecting label emission
    622623statements in appropriate positions to mark the beginning of basic blocks.
     624These are the positions where the cost instrumentation will appear in the final output.
    623625% The
    624626% set of labels with their positions is called labelling.
     
    630632% of label emissions: $\ell_1,\ldots,\ell_n$, called the program trace. We clarify the conditions
    631633% that the labelling must respect later.
     634For the example in Section~\ref{sec:workflow} this is just the original C code
     635with ``EMIT'' instructions added at every point a \lstinline'__cost_incr' call
     636appears in the final code.
    632637
    633638The second component is a labelling preserving compiler. It can be obtained from
     
    635640language and by propagating label emission statements during compilation. The
    636641compiler is correct if it preserves both the functional behaviour of the program
    637 and the traces of observables.
     642and the traces of observables, including the labels `emitted'.
    638643% We may also ask that the function that erases the cost
    639644% emission statements commute with compilation. This optional property grants that
     
    641646% set of requirements will be added later.
    642647
    643 The third component is a static object code analyser. It takes as input a labelled
    644 object code and it computes the scope of each of its label emission statements,
    645 i.e.\ the tree of instructions that may be executed after the statement and before
    646 a new label emission is encountered.
    647 It is a tree and not a sequence because the scope
    648 may contain a branching statement. In order to grant that such a finite tree
    649 exists, 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 labelling. The
    651 analyser fails if the labelling is unsound. For each scope, the analyser
    652 computes an upper bound of the execution time required by the scope, using the
    653 maximum of the costs of the two branches in case of a conditional statement.
    654 Finally, the analyser computes the cost of a label by taking the maximum of the
    655 costs of the scopes of every statement that emits that label.
    656 
    657 The fourth and last component takes in input the cost model computed at step 3
    658 and the labelled code computed at step 1. It outputs a source program obtained
    659 by replacing each label emission statement with a statement that increments the
    660 global cost variable with the cost associated to the label by the cost model. 
    661 The obtained source code is the instrumented source code.
    662 
    663 \paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement
    664 obviously hold, with 2 and 3 being a consequence of the definition of a correct
    665 labelling preserving compiler. It is also obvious that the value of the global
    666 cost variable of an instrumented source code is at any time equal to the sum of
    667 the costs of the labels emitted by the corresponding labelled code. Moreover,
    668 because the compiler preserves all traces, the sum of the costs of the labels
    669 emitted in the source and target labelled code are the same. Therefore, to
    670 satisfy the fourth requirement, we need to grant that the time taken to execute
    671 the object code is equal to the sum of the costs of the labels emitted by the
    672 object code. We collect all the necessary conditions for this to happen in the
    673 definition of a sound labelling: a) all loops must be broken by a cost emission
    674 statement;  b) all program instructions must be in the scope of some cost
    675 emission statement. To satisfy also the fifth requirement, additional
    676 requirements must be imposed on the object code labelling to avoid all uses of
    677 the maximum in the cost computation: the labelling is precise if every label is
    678 emitted at most once and both branches of a conditional jump start with a label
     648The third component analyses the labelled
     649object code to compute the scope of each of its label emission statements,
     650i.e.\ the instructions that may be executed after the statement and before
     651a new label emission is encountered, and then computes the maximum cost of
     652each.  Note that we only have enough information at this point to compute
     653the cost of loop-free portions of code.  We will consider how to ensure that
     654every loop is broken by a cost label shortly.
     655%It is a tree and not a sequence because the scope
     656%may contain a branching statement. In order to grant that such a finite tree
     657%exists, the object code must not contain any loop that is not broken by a label
     658%emission statement. This is the first requirement of a sound labelling. The
     659%analyser fails if the labelling is unsound. For each scope, the analyser
     660%computes an upper bound of the execution time required by the scope, using the
     661%maximum of the costs of the two branches in case of a conditional statement.
     662%Finally, the analyser computes the cost of a label by taking the maximum of the
     663%costs of the scopes of every statement that emits that label.
     664
     665The fourth and final component replaces the labels in the labelled
     666version of the source code produced at the start with the costs
     667computed for each label's scope.  This yields the instrumented source
     668code.  For the example, this is the code in \autoref{itest1}, except
     669for the specifications in comments, which we consider in
     670Section~\ref{sec:exploit}.
     671
     672\paragraph{Correctness.} Requirements 1 and 2 hold because of the
     673non-invasive labelling procedure.  Requirement 3 can be satisfied by
     674implementing compilation correctly.  It is obvious that the value of
     675the global cost variable of the instrumented source code is always
     676equal to the sum of the costs of the labels emitted by the
     677corresponding labelled code. Moreover, because the compiler preserves
     678all traces, the sum of the costs of the labels emitted in the source
     679and target labelled code are the same. Therefore, to satisfy the
     680soundness requirement, we need to ensure that the time taken to
     681execute the object code is equal to the sum of the costs of the labels
     682emitted by the object code. We collect all the necessary conditions
     683for this to happen in the definition of a \emph{sound} labelling: a)
     684all loops must be broken by a cost emission statement; b) all program
     685instructions must be in the scope of some cost emission statement.
     686This ensures that every label's scope is a tree of instructions, with
     687the cost being the most expensive path. To satisfy also the precision
     688requirement, we must make the scopes flat sequences of instructions.
     689We require a \emph{precise} labelling where every label is emitted at
     690most once and both branches of each conditional jump start with a label
    679691emission statement.
    680692
    681693The correctness and precision of the labelling approach only rely on the
    682694correctness and precision of the object code labelling. The simplest
    683 way to achieve them is to impose correctness and precision
    684 requirements also on the initial labelling produced by the first software
    685 component, and to ask the compiler to preserve these
     695way to achieve that is to impose correctness and precision
     696requirements on the source code labelling produced at the start, and
     697to demand that the compiler to preserve these
    686698properties too. The latter requirement imposes serious limitations on the
    687699compilation strategy and optimizations: the compiler may not duplicate any code
     
    693705the presence of stateful hardware whose state influences the cost of operations,
    694706like pipelines and caches. In Section~\ref{lab:deplabel} we will see an extension of the
    695 basic labelling approach to cover this situation.
     707basic labelling approach which tackles these problems.
    696708
    697709In CerCo we have developed several cost preserving compilers based on
     
    739751
    740752The second C compiler is the \emph{Trusted CerCo Compiler}, whose cost
    741 predictions are formally verified. The code distributed
    742 is extracted OCaml code from the Matita implementation. In the rest of
    743 this section we will only focus on the Trusted CerCo Compiler, that only targets
    744 the C language and the 8051/8052 family, and that does not implement any
    745 advanced optimisations yet. Its user interface, however, is the same as the one
    746 of the other version, in order to trade safety with additional performances. In
    747 particular, the Frama-C CerCo plugin can work without recompilation
     753predictions are formally verified. The executable code
     754is OCaml code extracted from the Matita implementation. The Trusted
     755CerCo Compiler only targets
     756the C language and the 8051/8052 family, and does not yet implement any
     757advanced optimisations. Its user interface, however, is the same as the
     758other version for interoperability. In
     759particular, the Frama-C CerCo plugin descibed in
     760Section~\ref{sec:exploit} can work without recompilation
    748761with both of our C compilers.
    749762
    750763The 8051/8052 microprocessor is a very simple one, with constant-cost
    751764instructions. It was chosen to separate the issue of exact propagation of the
    752 cost model from the orthogonal problem of the static analysis of object code
    753 that may require approximations or dependent costs.
     765cost model from the orthogonal problem of low-level timing analysis of object code
     766that may require approximation or dependent costs.
    754767
    755768The (trusted) CerCo compiler implements the following optimisations: cast
     
    773786\item All the intermediate languages include label emitting instructions to
    774787implement the labelling approach, and the compiler preserves execution traces.
    775 \item Traditionally compilers target an assembly language with additional
    776 macro-instructions to be expanded before assembly; for CerCo we need to go all
    777 the way down to object code in order to perform the static analysis. Therefore
    778 we integrated also an optimising assembler and a static analyser.
     788\item Instead of targeting an assembly language with additional
     789macro-instructions which are expanded before assembly, we directly
     790produce object code in order to perform the timing analysis, using
     791an integrated optimising assembler.
    779792\item In order to avoid the additional work of implementing a linker
    780793 and a loader, we do not support separate
     
    788801becoming common again in multi-core processors. Therefore the compiler has to
    789802keep track of data and it must move data between memory regions in the proper
    790 way. Moreover the size of pointers to different regions is not uniform. An
    791 additional difficulty was that the space available for the stack in internal
    792 memory in the 8051 is tiny, allowing only a minor number of nested calls. To
    793 support full recursion in order to test the CerCo tools also on recursive
    794 programs, the compiler implements a stack in external memory.
     803way. Moreover the size of pointers to different regions is not uniform. %An
     804%additional difficulty was that the space available for the stack in internal
     805%memory in the 8051 is tiny, allowing only a minor number of nested calls. To
     806%support full recursion in order to test the CerCo tools also on recursive
     807%programs, the compiler implements a stack in external memory.
    795808\end{enumerate}
    796809
     
    943956
    944957\subsection{Techniques to exploit the induced cost model}
     958\label{sec:exploit}
    945959We now turn our attention to synthesising high-level costs, such as
    946960the execution time of a whole program.  We consider as our starting point source level costs
Note: See TracChangeset for help on using the changeset viewer.