Changeset 3142 for Deliverables/D3.4/Report/report.tex
- Timestamp:
- Apr 15, 2013, 10:51:14 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.4/Report/report.tex
r3140 r3142 133 133 \section{Introduction} 134 134 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 136 translation validation on sound, precise labelling properties.} 142 137 143 138 The \cerco{} compiler compiles C code targeting microcontrollers implementing … … 151 146 into the verification of the whole compiler. 152 147 153 % TODO: maybe mention stack space here? other additions? refer to "layering"? 148 \todo{maybe mention stack space here? other additions? refer to "layering"?} 154 149 A key part of this work was to separate the proofs about the compiled code's 155 150 extensional behaviour (that is, the functional correctness of the compiler) … … 172 167 statement more precise. Following that, in Section~\ref{sec:fegoals} we 173 168 describe the statements we need to prove about the intermediate \textsf{RTLabs} 174 programs sufficient for the back-end proofs. TODO: rest of document structure169 programs sufficient for the back-end proofs. \todo{rest of document structure} 175 170 176 171 \section{The compiler and main goals} … … 188 183 \> $\downarrow$ \> CIL parser (unformalized \ocaml)\\ 189 184 \textsf{Clight}\\ 185 %\> $\downarrow$ \> add runtime functions\\ 186 \> $\downarrow$ \> \lstinline[language=C]'switch' removal\\ 187 \> $\downarrow$ \> labelling\\ 190 188 \> $\downarrow$ \> cast removal\\ 191 \> $\downarrow$ \> add runtime functions\\192 \> $\downarrow$ \> labelling\\193 189 \> $\downarrow$ \> stack variable allocation and control structure 194 190 simplification\\ 195 191 \textsf{Cminor}\\ 196 \> $\downarrow$ \> generate global variable initialization code\\192 %\> $\downarrow$ \> generate global variable initialization code\\ 197 193 \> $\downarrow$ \> transform to RTL graph\\ 198 194 \textsf{RTLabs}\\ 195 \> $\downarrow$ \> check cost labelled properties of RTL graph\\ 199 196 \> $\downarrow$ \> start of target specific back-end\\ 200 197 \>\quad \vdots … … 202 199 \end{minipage} 203 200 \end{center} 204 \caption{Front-end languages and transformations}201 \caption{Front-end languages and compiler passes} 205 202 \label{fig:summary} 206 203 \end{figure} … … 233 230 \subsection{Revisions to the prototype compiler} 234 231 235 TODO: could be a good idea to have this again 232 TODO: could be a good idea to have this again; stack space, 233 initialisation, cost checks, had we dropped cminor loops in previous 234 writing?, check mailing list in case I've forgotten something 236 235 237 236 \subsection{Main goals} … … 442 441 \section{Finding corresponding measurable subtraces} 443 442 443 There 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 451 TODO: layered approach - main part is the common measurable 452 preservation proof; fine-grained version of normal simulation results 453 does rest. 454 455 \subsection{Generic measurable subtrace lifting proof} 456 457 Sketch properties required; need to preserve prefix as well as meas 458 subtrace; how to deal with untidy edges wrt to sim rel; anything to 459 say 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 467 TODO: ideal for this development would be to prove at labelling stage, 468 preserve throughout, fits with use of dep types to reduce partiality 469 of phases; time pressures suggest different approach: t.v. style, 470 runtime check only do proof in one place rather than three; can't push 471 further due to structured traces, possible future investigation if ... 472 444 473 \section{Existence of a structured trace} 445 474 \label{sec:structuretrace} 446 475 476 TODO: design, basic structure from termination proof, how cost 477 labelling props are baked in; unrepeating PCs, remainder of sound 478 labellings; coinductive version for whole programs, reason/relevance, 479 use of em (maybe a general comment about uses of classical reasoning 480 in development) 481 447 482 \section{Conclusion} 448 483 449 484 TODO 485 486 TODO: appendix on code layout? 450 487 451 488 \bibliographystyle{plain}
Note: See TracChangeset
for help on using the changeset viewer.