Changeset 3142


Ignore:
Timestamp:
Apr 15, 2013, 10:51:14 AM (4 years ago)
Author:
campbell
Message:

Sketch out a bit more of 3.4.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3140 r3142  
    133133\section{Introduction}
    134134
    135 TODO: briefly, cerco compiler's purpose, prototype, formalisation, whole
    136 compiler.  Full functional correctness too ambitious; fortunately get nice
    137 layering of intensional correctness on top of mildly refined normal simulations.
    138 Hence, concentrate on new intensional correctness results; add stack space for
    139 more precise statement.  Also do some
    140 translation validation on sound, precise labelling properties.  Fluffly version
    141 of correctness statement.
     135\todo{add stack space for more precise statement.  Also do some
     136translation validation on sound, precise labelling properties.}
    142137
    143138The \cerco{} compiler compiles C code targeting microcontrollers implementing
     
    151146into the verification of the whole compiler.
    152147
    153 % TODO: maybe mention stack space here?  other additions?  refer to "layering"?
     148\todo{maybe mention stack space here?  other additions?  refer to "layering"?}
    154149A key part of this work was to separate the proofs about the compiled code's
    155150extensional behaviour (that is, the functional correctness of the compiler)
     
    172167statement more precise.  Following that, in Section~\ref{sec:fegoals} we
    173168describe the statements we need to prove about the intermediate \textsf{RTLabs}
    174 programs sufficient for the back-end proofs.  TODO: rest of document structure
     169programs sufficient for the back-end proofs.  \todo{rest of document structure}
    175170
    176171\section{The compiler and main goals}
     
    188183\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
    189184\textsf{Clight}\\
     185%\> $\downarrow$ \> add runtime functions\\
     186\> $\downarrow$ \> \lstinline[language=C]'switch' removal\\
     187\> $\downarrow$ \> labelling\\
    190188\> $\downarrow$ \> cast removal\\
    191 \> $\downarrow$ \> add runtime functions\\
    192 \> $\downarrow$ \> labelling\\
    193189\> $\downarrow$ \> stack variable allocation and control structure
    194190 simplification\\
    195191\textsf{Cminor}\\
    196 \> $\downarrow$ \> generate global variable initialization code\\
     192%\> $\downarrow$ \> generate global variable initialization code\\
    197193\> $\downarrow$ \> transform to RTL graph\\
    198194\textsf{RTLabs}\\
     195\> $\downarrow$ \> check cost labelled properties of RTL graph\\
    199196\> $\downarrow$ \> start of target specific back-end\\
    200197\>\quad \vdots
     
    202199\end{minipage}
    203200\end{center}
    204 \caption{Front-end languages and transformations}
     201\caption{Front-end languages and compiler passes}
    205202\label{fig:summary}
    206203\end{figure}
     
    233230\subsection{Revisions to the prototype compiler}
    234231
    235 TODO: could be a good idea to have this again
     232TODO: could be a good idea to have this again; stack space,
     233initialisation, cost checks, had we dropped cminor loops in previous
     234writing?, check mailing list in case I've forgotten something
    236235
    237236\subsection{Main goals}
     
    442441\section{Finding corresponding measurable subtraces}
    443442
     443There follow the three main passes of the front-end:
     444\begin{enumerate}
     445\item simplification of casts in \textsf{Clight} code
     446\item \textsf{Clight} to \textsf{Cminor} translation, performing stack
     447  variable allocation and simplifying control structures
     448\item transformation to \textsf{RTLabs} control flow graph
     449\end{enumerate}
     450
     451TODO: layered approach - main part is the common measurable
     452preservation proof; fine-grained version of normal simulation results
     453does rest.
     454
     455\subsection{Generic measurable subtrace lifting proof}
     456
     457Sketch properties required; need to preserve prefix as well as meas
     458subtrace; how to deal with untidy edges wrt to sim rel; anything to
     459say about obs, stack?
     460
     461\subsection{Simulation results for each pass}
     462
     463\todo{don't use loop structures from CompCert, go straight to jumps}
     464
     465\section{Checking cost labelling properties}
     466
     467TODO: ideal for this development would be to prove at labelling stage,
     468preserve throughout, fits with use of dep types to reduce partiality
     469of phases; time pressures suggest different approach: t.v. style,
     470runtime check only do proof in one place rather than three; can't push
     471further due to structured traces, possible future investigation if ...
     472
    444473\section{Existence of a structured trace}
    445474\label{sec:structuretrace}
    446475
     476TODO: design, basic structure from termination proof, how cost
     477labelling props are baked in; unrepeating PCs, remainder of sound
     478labellings; coinductive version for whole programs, reason/relevance,
     479use of em (maybe a general comment about uses of classical reasoning
     480in development)
     481
    447482\section{Conclusion}
    448483
    449484TODO
     485
     486TODO: appendix on code layout?
    450487
    451488\bibliographystyle{plain}
Note: See TracChangeset for help on using the changeset viewer.