Changeset 3315


Ignore:
Timestamp:
Jun 5, 2013, 6:17:31 PM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3314 r3315  
    213213The CerCo compiler is loosely based on the CompCert compiler, a recently developed certified compiler from C to the PowerPC, ARM and x86 microprocessors. Contrarily to CompCert, both the CerCo code and its certification are open source. Some data structures and language definitions for the front-end are directly taken from CompCert, while the back-end is a redesign and reimplementation of a didactic compiler from Pascal to MIPS used by Francois Pottier for a course at the Ecole Polytechnique.
    214214
    215 Following CompCert tradition, the compiler is organised in an unusually large number of intermediate passes, all responsible for just one change in the semantics of the source and target languages. Introducing multiple passes has minor performance implications on modern hardware and it allows to simplify the simulation proofs. The first three intermediate languages for the front-end. They are syntactically and semantically quite different between each other. For example, in the first language we find the traditional looping structures of C, in the second all loops are infinite loops (built with GOTOs) interrupted using BREAKs and in the third one the code is organised as a graph of statements where loops become loops in the graph. The four back-end languages, instead, have a more similar syntax.
    216 
    217 Departing from CompCert, we do not provide a stand alone syntax and semantics for every back-end language. Instead, we developed a generic representation of back-end languages as a parametric data type that can be instantiated to the wanted language. The generic representation allows to multiply the number of passes without increasing too much the code size. For example, we also provide a single generic semantics for the generic representation, parameterized over pass specific details.
    218 
    219 Other departures from CompCert are:
     215The main peculiarities of the CerCo compiler are:
    220216\begin{enumerate}
    221217\item all of our intermediate languages include label emitting instructions to implement the labelling approach, and the compiler preserves execution traces.
    222 \item the target language of CompCert is an assembly language with additional macro-instructions to be expanded before assembly; for CerCo we need to go all the way down to object code in order to perform the static analysis. Therefore we developed also an optimizing assembler and a static analyser, all integrated in the compiler.
     218\item tradiniotally compilers target an assembly language with additional macro-instructions to be expanded before assembly; for CerCo we need to go all the way down to object code in order to perform the static analysis. Therefore we developed also an optimizing assembler and a static analyser, all integrated in the compiler.
    223219\item to avoid implementing a linker and a loader, we do not support separate compilation and external calls. Adding a linker and a loader is a transparent process to the labelling approach and should create no unknown problem
    224220\item we target an 8-bit processor. Targeting an 8 bit processor requires several changes and increased code size, but it is not fundamentally more complex. The proof of correctness, however, becomes much harder.
    225221\item we target a microprocessor that has a non uniform memory model, which is still often the case for microprocessors used in embedded systems and that is becoming common again in multi-core processors. Therefore the compiler has to keep track of the position of data and it must move data between memory regions in the proper way. Also the size of pointers to different regions is not uniform. In our case, an additional difficulty was that the space available for the stack in internal memory in the 8051 is tiny, allowing only a minor number of nested calls. To support full recursion in order to test the CerCo tools also on recursive programs, the compiler manually manages a stack in external memory.
    226 \item while there is a rough correspondence between CompCert and CerCo back-end passes,  the order of the passes is permuted. In the future we want to explore how to exploit our generic back-end language representation to try to freely compose and permute passes.
    227222\end{enumerate}
    228223
    229224\section{A formal certification of the CerCo compiler}
    230 The Trusted CerCo Compiler has been implemented and certified using the interactive theorem prover Matita. In this section we briefly hint at the exact correctness statement and at the main ingredients of the proof. Details on the proof techniques employed and further information can be collected from the CerCo deliverables and papers.
    231 
    232 \subsection{The statement}
     225The Trusted CerCo Compiler has been implemented and certified using the interactive theorem prover Matita. The details on the proof techniques employed and
     226the proof sketch can be collected from the CerCo deliverables and papers.
     227In this section we will only hint at the correctness statement, which turned
     228out to be more complex than what we expected at the beginning.
     229
     230\paragraph{The statement}
    233231The most natural statement of correctness for our complexity preserving compiler is that the time spent for execution by a terminating object code program should be the time predicted on the source code by adding up the cost of every label emission statement. This statement, however, is too naïve to be useful for real world real time programs like those used in embedded systems.
    234232Real time programs are often reactive programs that loop forever responding to events (inputs) by performing some computation followed by some action (output) and the return to the initial state. For looping programs the overall execution time does not make sense. The same happens for reactive programs that spend an unpredictable amount of time in I/O. What is interesting is the reaction time that measure the time spent between I/O events. Moreover, we are interested in predicting and ruling out programs that crash running out of space on a certain input.
Note: See TracChangeset for help on using the changeset viewer.