Changeset 3142 for Deliverables/D3.4/Report/report.tex

Timestamp:

Apr 15, 2013, 10:51:14 AM (7 years ago)

Author:

campbell

Message:

Sketch out a bit more of 3.4.

File:

• Deliverables/D3.4/Report/report.tex (modified) (7 diffs)

Deliverables/D3.4/Report/report.tex

@@ -133 +133 @@
 \section{Introduction}
 
-TODO: briefly, cerco compiler's purpose, prototype, formalisation, whole
-compiler.  Full functional correctness too ambitious; fortunately get nice
-layering of intensional correctness on top of mildly refined normal simulations.
-Hence, concentrate on new intensional correctness results; add stack space for
-more precise statement.  Also do some
-translation validation on sound, precise labelling properties.  Fluffly version
-of correctness statement.
+\todo{add stack space for more precise statement.  Also do some
+translation validation on sound, precise labelling properties.}
 
 The \cerco{} compiler compiles C code targeting microcontrollers implementing
@@ -151 +146 @@
 into the verification of the whole compiler.
 
-% TODO: maybe mention stack space here?  other additions?  refer to "layering"?
+\todo{maybe mention stack space here?  other additions?  refer to "layering"?}
 A key part of this work was to separate the proofs about the compiled code's
 extensional behaviour (that is, the functional correctness of the compiler)
@@ -172 +167 @@
 statement more precise.  Following that, in Section~\ref{sec:fegoals} we
 describe the statements we need to prove about the intermediate \textsf{RTLabs}
-programs sufficient for the back-end proofs.  TODO: rest of document structure
+programs sufficient for the back-end proofs.  \todo{rest of document structure}
 
 \section{The compiler and main goals}
@@ -188 +183 @@
 \> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
 \textsf{Clight}\\
+%\> $\downarrow$ \> add runtime functions\\
+\> $\downarrow$ \> \lstinline[language=C]'switch' removal\\
+\> $\downarrow$ \> labelling\\
 \> $\downarrow$ \> cast removal\\
-\> $\downarrow$ \> add runtime functions\\
-\> $\downarrow$ \> labelling\\
 \> $\downarrow$ \> stack variable allocation and control structure
  simplification\\
 \textsf{Cminor}\\
-\> $\downarrow$ \> generate global variable initialization code\\
+%\> $\downarrow$ \> generate global variable initialization code\\
 \> $\downarrow$ \> transform to RTL graph\\
 \textsf{RTLabs}\\
+\> $\downarrow$ \> check cost labelled properties of RTL graph\\
 \> $\downarrow$ \> start of target specific back-end\\
 \>\quad \vdots
@@ -202 +199 @@
 \end{minipage}
 \end{center}
-\caption{Front-end languages and transformations}
+\caption{Front-end languages and compiler passes}
 \label{fig:summary}
 \end{figure}
@@ -233 +230 @@
 \subsection{Revisions to the prototype compiler}
 
-TODO: could be a good idea to have this again
+TODO: could be a good idea to have this again; stack space,
+initialisation, cost checks, had we dropped cminor loops in previous
+writing?, check mailing list in case I've forgotten something
 
 \subsection{Main goals}
@@ -442 +441 @@
 \section{Finding corresponding measurable subtraces}
 
+There follow the three main passes of the front-end:
+\begin{enumerate}
+\item simplification of casts in \textsf{Clight} code
+\item \textsf{Clight} to \textsf{Cminor} translation, performing stack
+  variable allocation and simplifying control structures
+\item transformation to \textsf{RTLabs} control flow graph
+\end{enumerate}
+
+TODO: layered approach - main part is the common measurable
+preservation proof; fine-grained version of normal simulation results
+does rest.
+
+\subsection{Generic measurable subtrace lifting proof}
+
+Sketch properties required; need to preserve prefix as well as meas
+subtrace; how to deal with untidy edges wrt to sim rel; anything to
+say about obs, stack?
+
+\subsection{Simulation results for each pass}
+
+\todo{don't use loop structures from CompCert, go straight to jumps}
+
+\section{Checking cost labelling properties}
+
+TODO: ideal for this development would be to prove at labelling stage,
+preserve throughout, fits with use of dep types to reduce partiality
+of phases; time pressures suggest different approach: t.v. style,
+runtime check only do proof in one place rather than three; can't push
+further due to structured traces, possible future investigation if ...
+
 \section{Existence of a structured trace}
 \label{sec:structuretrace}
 
+TODO: design, basic structure from termination proof, how cost
+labelling props are baked in; unrepeating PCs, remainder of sound
+labellings; coinductive version for whole programs, reason/relevance,
+use of em (maybe a general comment about uses of classical reasoning
+in development)
+
 \section{Conclusion}
 
 TODO
+
+TODO: appendix on code layout?
 
 \bibliographystyle{plain}