# Changeset 3313 for Papers

Ignore:
Timestamp:
Jun 5, 2013, 5:40:37 PM (6 years ago)
Message:

redrawn fork flow in tikz, adding the cost plugin

File:
1 edited

### Legend:

Unmodified
 r3312 \usepackage{url} \usepackage{tikz} \usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes} %\renewcommand{\verb}{\lstinline} %\def\lstlanguagefiles{lst-grafite.tex} Other departures from CompCert are: 1. all of our intermediate languages include label emitting instructions to implement the labelling approach, and the compiler preserves execution traces. 2. 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. 3. 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 4. 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. 5. 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. 6. 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. \begin{enumerate} \item all of our intermediate languages include label emitting instructions to implement the labelling approach, and the compiler preserves execution traces. \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. \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 \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. \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. \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. \end{enumerate} \section{A formal certification of the CerCo compiler} \begin{figure}[t] \begin{tabular}{l@{\hspace{0.2cm}}|l} \begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l} \begin{lstlisting} char a[] = {3, 2, 7, -4}; \end{lstlisting} & $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$ %  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$ \begin{tikzpicture}[ baseline={([yshift=-.5ex]current bounding box)}, element/.style={draw, text width=1.6cm, on chain, text badly centered}, >=stealth ] {[start chain=going below, node distance=.5cm] \node [element] (cerco) {CerCo\\compiler}; \node [element] (cost)  {CerCo\\cost plugin}; {[densely dashed] \node [element] (ded)   {Deductive\\platform}; \node [element] (check) {Proof\\checker}; } } \coordinate [left=3.5cm of cerco] (left); {[every node/.style={above, text width=3.5cm, text badly centered, font=\scriptsize}] \draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) -- node {C source} (t-|left); \draw [->] (cerco) -- (cost); \draw [->] ([yshift=1ex]cerco.south west) coordinate (t) -- node {C source+cost annotations} (t-|left) coordinate (cerco out); \draw [->] ([yshift=1ex]cost.south west) coordinate (t) -- node {C source+cost annotations\\+synthesized assertions} (t-|left) coordinate (out); {[densely dashed] \draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) -- node {C source+cost annotations\\+complexity assertions} (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out); \draw [->] ([yshift=1ex]ded.south west) coordinate (t) -- node {complexity obligations} (t-|left) coordinate (out); \draw [<-] ([yshift=-1ex]check.north west) coordinate (t) -- node {complexity proof} (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out); \draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) .. (ded in); }} %% user: % head \draw (current bounding box.west) ++(-.2,.5) circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t); % arms \draw (t) -- +(-.3,-.2); \draw (t) -- +(.3,-.2); % body \draw (t) -- ++(0,-.4) coordinate (t); % legs \draw (t) -- +(-.2,-.6); \draw (t) -- +(.2,-.6); \end{tikzpicture} \end{tabular} \caption{On the left: a C program that counts the array's elements greater or equal to the treshold. On the right: CerCo's interaction diagram.} diagram. CerCo's components are drawn solid.} \label{test1} \end{figure}