Changeset 3315
- Timestamp:
- Jun 5, 2013, 6:17:31 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3314 r3315 213 213 The 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. 214 214 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: 215 The main peculiarities of the CerCo compiler are: 220 216 \begin{enumerate} 221 217 \item all of our intermediate languages include label emitting instructions to implement the labelling approach, and the compiler preserves execution traces. 222 \item t he target language of CompCert isan 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. 223 219 \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 224 220 \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. 225 221 \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.227 222 \end{enumerate} 228 223 229 224 \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} 225 The Trusted CerCo Compiler has been implemented and certified using the interactive theorem prover Matita. The details on the proof techniques employed and 226 the proof sketch can be collected from the CerCo deliverables and papers. 227 In this section we will only hint at the correctness statement, which turned 228 out to be more complex than what we expected at the beginning. 229 230 \paragraph{The statement} 233 231 The 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. 234 232 Real 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.