Changeset 3313


Ignore:
Timestamp:
Jun 5, 2013, 5:40:37 PM (4 years ago)
Author:
tranquil
Message:

redrawn fork flow in tikz, adding the cost plugin

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3312 r3313  
    1818\usepackage{url}
    1919
     20\usepackage{tikz}
     21\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
     22
    2023%\renewcommand{\verb}{\lstinline}
    2124%\def\lstlanguagefiles{lst-grafite.tex}
     
    216219
    217220Other departures from CompCert are:
    218 1. all of our intermediate languages include label emitting instructions to implement the labelling approach, and the compiler preserves execution traces.
    219 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.
    220 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
    221 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.
    222 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.
    223 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.
     221\begin{enumerate}
     222\item all of our intermediate languages include label emitting instructions to implement the labelling approach, and the compiler preserves execution traces.
     223\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.
     224\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
     225\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.
     226\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.
     227\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.
     228\end{enumerate}
    224229
    225230\section{A formal certification of the CerCo compiler}
     
    237242
    238243\begin{figure}[t]
    239 \begin{tabular}{l@{\hspace{0.2cm}}|l}
     244\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
    240245\begin{lstlisting}
    241246char a[] = {3, 2, 7, -4};
     
    255260\end{lstlisting}
    256261&
    257  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
     262%  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
     263\begin{tikzpicture}[
     264    baseline={([yshift=-.5ex]current bounding box)},
     265    element/.style={draw, text width=1.6cm, on chain, text badly centered},
     266    >=stealth
     267    ]
     268{[start chain=going below, node distance=.5cm]
     269\node [element] (cerco) {CerCo\\compiler};
     270\node [element] (cost)  {CerCo\\cost plugin};
     271{[densely dashed]
     272\node [element] (ded)   {Deductive\\platform};
     273\node [element] (check) {Proof\\checker};
     274}
     275}
     276\coordinate [left=3.5cm of cerco] (left);
     277{[every node/.style={above, text width=3.5cm, text badly centered,
     278                     font=\scriptsize}]
     279\draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) --
     280    node {C source}
     281    (t-|left);
     282\draw [->] (cerco) -- (cost);
     283\draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
     284    node {C source+cost annotations}
     285    (t-|left) coordinate (cerco out);
     286\draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
     287    node {C source+cost annotations\\+synthesized assertions}
     288    (t-|left) coordinate (out);
     289{[densely dashed]
     290\draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
     291    node {C source+cost annotations\\+complexity assertions}
     292    (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
     293\draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
     294    node {complexity obligations}
     295    (t-|left) coordinate (out);
     296\draw [<-] ([yshift=-1ex]check.north west) coordinate (t) --
     297    node {complexity proof}
     298    (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
     299\draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) .. (ded in);
     300}}
     301%% user:
     302% head
     303\draw (current bounding box.west) ++(-.2,.5)
     304    circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t);
     305% arms
     306\draw (t) -- +(-.3,-.2);
     307\draw (t) -- +(.3,-.2);
     308% body
     309\draw (t) -- ++(0,-.4) coordinate (t);
     310% legs
     311\draw (t) -- +(-.2,-.6);
     312\draw (t) -- +(.2,-.6);
     313\end{tikzpicture}
    258314\end{tabular}
    259315\caption{On the left: a C program that counts the array's elements
    260316 greater or equal to the treshold. On the right: CerCo's interaction
    261  diagram.}
     317 diagram. CerCo's components are drawn solid.}
    262318\label{test1}
    263319\end{figure}
Note: See TracChangeset for help on using the changeset viewer.