Changeset 3424


Ignore:
Timestamp:
Feb 11, 2014, 12:35:22 PM (5 years ago)
Author:
campbell
Message:

Minor edits to section 4.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3422 r3424  
    710710The hardware state comprises both the functional state that affects the
    711711computation (the value of the registers and memory) and the non-functional
    712 state that does not (the pipeline and cache contents for example). The former is
     712state that does not (the pipeline and cache contents, for example). The former is
    713713in correspondence with the source code state, but reconstructing the
    714714correspondence may be hard and lifting the cost model to work on the source code
    715715state is likely to produce cost expressions that are too complex to understand and reason about.
    716 Luckily enough, in all modern architectures the cost of executing single
     716Fortunately, in all modern architectures the cost of executing single
    717717instructions is either independent of the functional state or the jitter---the
    718718difference between the worst and best case execution times---is small enough
    719 to be bounded without losing too much precision. Therefore we can concentrate
    720 on dependencies over the `non-functional' parts of the state only.
     719to be bounded without losing too much precision. Therefore we only consider
     720dependencies on the `non-functional' parts of the state.
    721721
    722722The non-functional state has no correspondence in the high level state and does
     
    730730update function which is computed during static analysis too. The update
    731731function associates to each label a function from the recently emitted labels
    732 and old state to the new state. It is computed composing the semantics of every
     732and old state to the new state. It is computed by composing the semantics of every
    733733instruction in a basic block and restricting it to the non-functional part of
    734734the state.
     
    745745trade precision of the analysis for simplicity by approximating the parametric
    746746cost with safe non parametric bounds. Interestingly, the functional analysis of
    747 the code can determine which blocks are executed more frequently in order to
    748 approximate more aggressively the ones that are executed less.
     747the code could determine which blocks are executed more frequently in order to
     748use more aggressive approximations for the ones that are executed least.
    749749
    750750Dependent labeling can also be applied to allow the compiler to duplicate
     
    752752a different cost to the different occurrences of a duplicated label. For
    753753example, loop peeling turns a loop into the concatenation of a copy of the loop
    754 body (that executes the first iteration) with the conditional execution of the
    755 loop (for the successive iterations). Because of further optimisations, the two
    756 copies of the loop will be compiled differently, with the first body usually
     754body for the first iteration and the conditional execution of the
     755loop for successive iterations. Further optimisations will compile the two
     756copies of the loop differently, with the first body usually
    757757taking more time.
    758758
     
    763763actual work to be done consists of introducing within the source code, and for each
    764764loop, a variable that counts the number of iterations. The loop optimisation code
    765 that duplicate the loop bodies must also modify the code to propagate correctly
     765that duplicate the loop bodies must also modify the code to correctly propagate
    766766the update of the iteration numbers. The technical details are more complex and
    767767can be found in the CerCo reports and publications. The implementation, however,
     
    834834bound on the reaction time of the system. We tested the Cost plugin and the
    835835Lustre wrapper on the C programs generated by the Lustre compiler. For programs
    836 consisting of a few hundred lines of code, the cost plugin computes a WCET and Alt-
    837 Ergo is able to discharge all VCs automatically.
     836consisting of a few hundred lines of code, the cost plugin computes a
     837WCET and Alt-Ergo is able to discharge all VCs automatically.
    838838
    839839\paragraph{Handling C programs with simple loops.}
    840840The cost annotations added by the CerCo compiler take the form of C instructions
    841 that update by a constant a fresh global variable called the cost variable.
    842 Synthesizing a WCET of a C function thus consists in statically resolving an
     841that update a fresh global variable called the cost variable by a constant.
     842Synthesizing a WCET of a C function thus consists of statically resolving an
    843843upper bound of the difference between the value of the cost variable before and
    844 after the execution of the function, i.e. find in the function the instructions
     844after the execution of the function, i.e. finding the instructions
    845845that update the cost variable and establish the number of times they are passed
    846 through during the flow of execution. In order to do the analysis the plugin
     846through during the flow of execution. To perform the analysis the plugin
    847847makes the following assumptions on the programs:
    8488481) there are no recursive functions;
     
    886886
    887887\subsection{The CerCo compiler}
    888 In CerCo we have developed a certain number of cost preserving compilers based
     888In CerCo we have developed several cost preserving compilers based
    889889on the labeling approach. Excluding an initial certified compiler for a `while'
    890890language, all remaining compilers target realistic source languages---a pure
     
    901901advanced optimisations yet. Its user interface, however, is the same as the one
    902902of the other versions, in order to trade safety with additional performances. In
    903 particular, the Frama-C CerCo plugin can work without recompilation with all
    904 compilers.
     903particular, the Frama-C CerCo plugin can work without recompilation
     904with all of our C compilers.
    905905
    906906The 8051/8052 microprocessor is a very simple one, with constant-cost
     
    919919The CerCo compiler is loosely based on the CompCert compiler \cite{compcert}, a
    920920recently developed certified compiler from C to the PowerPC, ARM and x86
    921 microprocessors. Contrary to CompCert, both the CerCo code and its
    922 certification are open source. Some data structures and language definitions for
     921microprocessors. In contrast to CompCert, both the CerCo code and its
     922certification are fully open source. Some data structures and language definitions for
    923923the front-end are directly taken from CompCert, while the back-end is a redesign
    924924of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the
    925925Ecole Polytechnique.
    926926
    927 The main peculiarities of the CerCo compiler are the following.
     927The main differences in the CerCo compiler are:
    928928\begin{enumerate}
    929929\item All the intermediate languages include label emitting instructions to
     
    933933the way down to object code in order to perform the static analysis. Therefore
    934934we integrated also an optimising assembler and a static analyser.
    935 \item In order to avoid implementing a linker and a loader, we do not support separate
    936 compilation and external calls. Adding them is a transparent
    937 process to the labeling approach and should create no unknown problem.
    938 \item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. Targeting an 8-bit processor requires
    939 several changes and increased code size, but it is not fundamentally more
     935\item In order to avoid the additional work of implementing a linker
     936 and a loader, we do not support separate
     937compilation and external calls. Adding them is orthogonal
     938to the labeling approach and should not introduce extra problems.
     939\item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. This requires
     940many changes and more compiler code, but it is not fundamentally more
    940941complex. The proof of correctness, however, becomes much harder.
    941942\item We target a microprocessor that has a non uniform memory model, which is
     
    953954We implemented the
    954955CerCo compiler in the interactive theorem prover Matita and have formally
    955 certified that the cost model induced on the source code correctly and precisely
    956 predicts the object code behaviour. We actually induce two cost models, one for
     956certified that the cost models induced on the source code correctly and precisely
     957predicts the object code behaviour. There are two cost models, one for execution
    957958time and one for stack space consumption. We show the correctness of the prediction
    958959only for those programs that do not exhaust the available machine stack space, a
     
    964965proof for non-functional properties, we have introduced a new semantics for
    965966programming languages based on a new kind of structured observables with the
    966 relative notions of forward similarity and the study of the intentional
     967relative notions of forward similarity and the study of the intensional
    967968consequences of forward similarity. We have also introduced a unified
    968969representation for back-end intermediate languages that was exploited to provide
     
    10211022I/O operations can be performed in the prefix of the run, but not in the
    10221023measurable sub-run. Therefore we prove that we can predict reaction times, but
    1023 not I/O times, as it should be.
     1024not I/O times, as desired.
    10241025
    10251026\section{Conclusions and future work}
Note: See TracChangeset for help on using the changeset viewer.