[3128] | 1 | \documentclass[11pt,epsf,a4wide]{article} |
---|
| 2 | \usepackage[mathletters]{ucs} |
---|
| 3 | \usepackage[utf8x]{inputenc} |
---|
[3168] | 4 | \usepackage{stmaryrd} |
---|
[3128] | 5 | \usepackage{listings} |
---|
| 6 | \usepackage{../../style/cerco} |
---|
| 7 | \newcommand{\ocaml}{OCaml} |
---|
| 8 | \newcommand{\clight}{Clight} |
---|
| 9 | \newcommand{\matita}{Matita} |
---|
| 10 | \newcommand{\sdcc}{\texttt{sdcc}} |
---|
| 11 | |
---|
| 12 | \newcommand{\textSigma}{\ensuremath{\Sigma}} |
---|
| 13 | |
---|
| 14 | % LaTeX Companion, p 74 |
---|
| 15 | \newcommand{\todo}[1]{\marginpar{\raggedright - #1}} |
---|
| 16 | |
---|
| 17 | \lstdefinelanguage{coq} |
---|
| 18 | {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record}, |
---|
| 19 | morekeywords={[2]if,then,else}, |
---|
| 20 | } |
---|
| 21 | |
---|
| 22 | \lstdefinelanguage{matita} |
---|
| 23 | {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on}, |
---|
| 24 | morekeywords={[2]whd,normalize,elim,cases,destruct}, |
---|
| 25 | mathescape=true, |
---|
| 26 | morecomment=[n]{(*}{*)}, |
---|
| 27 | } |
---|
| 28 | |
---|
| 29 | \lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false, |
---|
| 30 | keywordstyle=\color{red}\bfseries, |
---|
| 31 | keywordstyle=[2]\color{blue}, |
---|
| 32 | commentstyle=\color{green}, |
---|
| 33 | stringstyle=\color{blue}, |
---|
| 34 | showspaces=false,showstringspaces=false} |
---|
| 35 | |
---|
| 36 | \lstset{extendedchars=false} |
---|
| 37 | \lstset{inputencoding=utf8x} |
---|
| 38 | \DeclareUnicodeCharacter{8797}{:=} |
---|
| 39 | \DeclareUnicodeCharacter{10746}{++} |
---|
| 40 | \DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} |
---|
| 41 | \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} |
---|
| 42 | |
---|
| 43 | |
---|
| 44 | \title{ |
---|
| 45 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
| 46 | (ICT)\\ |
---|
| 47 | PROGRAMME\\ |
---|
| 48 | \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}} |
---|
| 49 | |
---|
| 50 | \date{ } |
---|
| 51 | \author{} |
---|
| 52 | |
---|
| 53 | \begin{document} |
---|
| 54 | \thispagestyle{empty} |
---|
| 55 | |
---|
| 56 | \vspace*{-1cm} |
---|
| 57 | \begin{center} |
---|
| 58 | \includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png} |
---|
| 59 | \end{center} |
---|
| 60 | |
---|
| 61 | \begin{minipage}{\textwidth} |
---|
| 62 | \maketitle |
---|
| 63 | \end{minipage} |
---|
| 64 | |
---|
| 65 | |
---|
| 66 | \vspace*{0.5cm} |
---|
| 67 | \begin{center} |
---|
| 68 | \begin{LARGE} |
---|
| 69 | \bf |
---|
| 70 | Report n. D3.4\\ |
---|
| 71 | Front-end Correctness Proofs\\ |
---|
| 72 | \end{LARGE} |
---|
| 73 | \end{center} |
---|
| 74 | |
---|
| 75 | \vspace*{2cm} |
---|
| 76 | \begin{center} |
---|
| 77 | \begin{large} |
---|
| 78 | Version 1.0 |
---|
| 79 | \end{large} |
---|
| 80 | \end{center} |
---|
| 81 | |
---|
| 82 | \vspace*{0.5cm} |
---|
| 83 | \begin{center} |
---|
| 84 | \begin{large} |
---|
| 85 | Authors:\\ |
---|
| 86 | Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark |
---|
| 87 | \end{large} |
---|
| 88 | \end{center} |
---|
| 89 | |
---|
| 90 | \vspace*{\fill} |
---|
| 91 | \noindent |
---|
| 92 | Project Acronym: \cerco{}\\ |
---|
| 93 | Project full title: Certified Complexity\\ |
---|
| 94 | Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ |
---|
| 95 | |
---|
| 96 | \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881} |
---|
| 97 | |
---|
| 98 | \newpage |
---|
| 99 | |
---|
[3228] | 100 | \section*{Executive Summary} |
---|
| 101 | \addcontentsline{toc}{section}{Executive Summary} |
---|
| 102 | |
---|
| 103 | |
---|
| 104 | \cerco{} Work Package 3, \emph{Verified Compiler - front end} aims |
---|
| 105 | for formalise and verify the front-end of the \cerco{} cost lifting |
---|
| 106 | compiler. This document accompanies the final deliverable, |
---|
| 107 | \textbf{D3.4: Front-end Correctness Proofs}. The deliverable consists |
---|
| 108 | of the formal correctness proofs for the front-end, written in the |
---|
| 109 | \matita{} proof assistant and this document provides report on the |
---|
| 110 | work carried out for it. |
---|
| 111 | |
---|
| 112 | \vspace*{1cm} |
---|
| 113 | |
---|
[3128] | 114 | \paragraph{Abstract} |
---|
[3228] | 115 | |
---|
[3173] | 116 | We report on the correctness proofs for the front-end of the \cerco{} |
---|
| 117 | cost lifting compiler. First, we identify the core result we wish to |
---|
| 118 | prove, which says that the we correctly predict the precise execution |
---|
| 119 | time for particular parts of the execution called \emph{measurable} |
---|
| 120 | subtraces. Then we consider the three distinct parts of the task: |
---|
| 121 | showing that the \emph{annotated source code} output by the compiler |
---|
| 122 | has equivalent behaviour to the original input (up to the |
---|
| 123 | annotations); showing that a measurable subtrace of the |
---|
| 124 | annotated source code corresponds to an equivalent measurable subtrace |
---|
| 125 | in the code produced by the front-end, including costs; and finally |
---|
| 126 | showing that the enriched \emph{structured} execution traces required |
---|
| 127 | for cost correctness in the back-end can be constructed from the |
---|
[3128] | 128 | properties of the code produced by the front-end. |
---|
| 129 | |
---|
[3214] | 130 | A key part of our work is that the intensional correctness results which show |
---|
[3128] | 131 | that we get consistent cost measurements throughout the intermediate languages |
---|
| 132 | of the compiler can be layered on top of normal forward simulation results, |
---|
[3173] | 133 | if we split those results into local call-structure preserving simulations. |
---|
[3231] | 134 | This split allowed us to concentrate on the \textbf{intensional} proofs by |
---|
| 135 | axiomatising some of the extensional simulation results that are very similar to |
---|
| 136 | existing compiler correctness results, such as CompCert. |
---|
[3128] | 137 | |
---|
[3226] | 138 | This report is about the correctness results that are deliverable |
---|
| 139 | D3.4, which are about the formalised compiler described in D3.2, using |
---|
| 140 | the source language semantics from D3.1 and intermediate language |
---|
| 141 | semantics from D3.3. It builds on earlier work on the correctness of |
---|
| 142 | a toy compiler built to test the labelling approach in D2.1. Together |
---|
| 143 | with the companion deliverable about the correctness of the back-end, |
---|
| 144 | D4.4, we obtain results about the whole formalised compiler. |
---|
[3128] | 145 | |
---|
| 146 | \newpage |
---|
| 147 | |
---|
| 148 | \tableofcontents |
---|
| 149 | |
---|
| 150 | % CHECK: clear up any -ize vs -ise |
---|
| 151 | % CHECK: clear up any "front end" vs "front-end" |
---|
| 152 | % CHECK: clear up any mentions of languages that aren't textsf'd. |
---|
| 153 | % CHECK: fix unicode in listings |
---|
| 154 | |
---|
| 155 | \section{Introduction} |
---|
| 156 | |
---|
[3214] | 157 | The \cerco{} compiler produces a version of the source code containing |
---|
[3226] | 158 | annotations describing the timing behaviour of the object code, as |
---|
| 159 | well as the object code itself. It compiles C code, targeting |
---|
[3214] | 160 | microcontrollers implementing the Intel 8051 architecture. There are |
---|
| 161 | two versions: first, an initial prototype was implemented in |
---|
[3226] | 162 | \ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{} |
---|
| 163 | proof assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to |
---|
[3214] | 164 | produce an executable compiler. In this document we present results |
---|
[3226] | 165 | from Deliverable 3.4, the formalised proofs in \matita{} about the |
---|
| 166 | front-end of the latter version of the compiler (culminating in the |
---|
| 167 | \lstinline'front_end_correct' lemma), and describe how that fits |
---|
| 168 | into the verification of the whole compiler. |
---|
[3128] | 169 | |
---|
[3231] | 170 | A key part of this work was to layer the \emph{intensional} correctness |
---|
[3214] | 171 | results that show that the costs produced are correct on top of the |
---|
[3231] | 172 | proofs about the compiled code's \emph{extensional} behaviour (that is, the |
---|
[3212] | 173 | functional correctness of the compiler). Unfortunately, the ambitious |
---|
| 174 | goal of completely verifying the entire compiler was not feasible |
---|
| 175 | within the time available, but thanks to this separation of |
---|
[3231] | 176 | extensional and intensional proofs we are able to axiomatise some extensional |
---|
[3214] | 177 | simulation results which are similar to those in other compiler verification |
---|
[3212] | 178 | projects and concentrate on the novel intensional proofs. We were |
---|
| 179 | also able to add stack space costs to obtain a stronger result. The |
---|
| 180 | proofs were made more tractable by introducing compile-time checks for |
---|
[3173] | 181 | the `sound and precise' cost labelling properties rather than proving |
---|
| 182 | that they are preserved throughout. |
---|
[3128] | 183 | |
---|
| 184 | The overall statement of correctness says that the annotated program has the |
---|
| 185 | same behaviour as the input, and that for any suitably well-structured part of |
---|
| 186 | the execution (which we call \emph{measurable}), the object code will execute |
---|
| 187 | the same behaviour taking precisely the time given by the cost annotations in |
---|
| 188 | the annotated source program. |
---|
| 189 | |
---|
| 190 | In the next section we recall the structure of the compiler and make the overall |
---|
| 191 | statement more precise. Following that, in Section~\ref{sec:fegoals} we |
---|
| 192 | describe the statements we need to prove about the intermediate \textsf{RTLabs} |
---|
[3214] | 193 | programs for the back-end proofs. |
---|
[3231] | 194 | Section~\ref{sec:inputtolabelling} covers the compiler passes which produce the |
---|
[3212] | 195 | annotated source program and Section~\ref{sec:measurablelifting} the rest |
---|
[3231] | 196 | of the transformations in the front-end. Then the compile-time checks |
---|
[3212] | 197 | for good cost labelling are detailed in Section~\ref{sec:costchecks} |
---|
| 198 | and the proofs that the structured traces required by the back-end |
---|
| 199 | exist are discussed in Section~\ref{sec:structuredtrace}. |
---|
[3128] | 200 | |
---|
[3231] | 201 | \section{The compiler and its correctness statement} |
---|
[3128] | 202 | |
---|
[3231] | 203 | The uncertified prototype \ocaml{} \cerco{} compiler was originally described |
---|
[3181] | 204 | in Deliverables 2.1 and 2.2. Its design was replicated in the formal |
---|
| 205 | \matita{} code, which was presented in Deliverables 3.2 and 4.2, for |
---|
| 206 | the front-end and back-end respectively. |
---|
[3128] | 207 | |
---|
| 208 | \begin{figure} |
---|
| 209 | \begin{center} |
---|
[3214] | 210 | \includegraphics[width=0.5\linewidth]{compiler-plain.pdf} |
---|
[3181] | 211 | \end{center} |
---|
| 212 | \caption{Languages in the \cerco{} compiler} |
---|
| 213 | \label{fig:compilerlangs} |
---|
| 214 | \end{figure} |
---|
| 215 | |
---|
| 216 | The compiler uses a number of intermediate languages, as outlined the |
---|
| 217 | middle two lines of Figure~\ref{fig:compilerlangs}. The upper line |
---|
| 218 | represents the front-end of the compiler, and the lower the back-end, |
---|
[3231] | 219 | finishing with Intel 8051 binary code. Not all of the front-end compiler passes |
---|
| 220 | introduce a new language, and Figure~\ref{fig:summary} presents a |
---|
[3181] | 221 | list of every pass involved. |
---|
| 222 | |
---|
| 223 | \begin{figure} |
---|
| 224 | \begin{center} |
---|
[3128] | 225 | \begin{minipage}{.8\linewidth} |
---|
| 226 | \begin{tabbing} |
---|
| 227 | \quad \= $\downarrow$ \quad \= \kill |
---|
[3231] | 228 | \textsf{C} (unformalised)\\ |
---|
| 229 | \> $\downarrow$ \> CIL parser (unformalised \ocaml)\\ |
---|
[3128] | 230 | \textsf{Clight}\\ |
---|
[3142] | 231 | %\> $\downarrow$ \> add runtime functions\\ |
---|
| 232 | \> $\downarrow$ \> \lstinline[language=C]'switch' removal\\ |
---|
| 233 | \> $\downarrow$ \> labelling\\ |
---|
[3128] | 234 | \> $\downarrow$ \> cast removal\\ |
---|
| 235 | \> $\downarrow$ \> stack variable allocation and control structure |
---|
| 236 | simplification\\ |
---|
| 237 | \textsf{Cminor}\\ |
---|
[3142] | 238 | %\> $\downarrow$ \> generate global variable initialization code\\ |
---|
[3128] | 239 | \> $\downarrow$ \> transform to RTL graph\\ |
---|
| 240 | \textsf{RTLabs}\\ |
---|
[3142] | 241 | \> $\downarrow$ \> check cost labelled properties of RTL graph\\ |
---|
[3128] | 242 | \> $\downarrow$ \> start of target specific back-end\\ |
---|
| 243 | \>\quad \vdots |
---|
| 244 | \end{tabbing} |
---|
| 245 | \end{minipage} |
---|
| 246 | \end{center} |
---|
[3142] | 247 | \caption{Front-end languages and compiler passes} |
---|
[3128] | 248 | \label{fig:summary} |
---|
| 249 | \end{figure} |
---|
| 250 | |
---|
[3181] | 251 | \label{page:switchintro} |
---|
[3231] | 252 | The annotated source code is produced by the cost labelling phase. |
---|
[3181] | 253 | Note that there is a pass to replace C \lstinline[language=C]'switch' |
---|
| 254 | statements before labelling --- we need to remove them because the |
---|
| 255 | simple form of labelling used in the formalised compiler is not quite |
---|
[3214] | 256 | capable of capturing their execution time costs, largely due to C's |
---|
| 257 | `fall-through' behaviour where execution from one branch continues in |
---|
| 258 | the next unless there is an explicit \lstinline[language=C]'break'. |
---|
[3181] | 259 | |
---|
| 260 | The cast removal phase which follows cost labelling simplifies |
---|
[3214] | 261 | expressions to prevent unnecessary arithmetic promotion, which is |
---|
[3181] | 262 | specified by the C standard but costly for an 8-bit target. The |
---|
| 263 | transformation to \textsf{Cminor} and subsequently \textsf{RTLabs} |
---|
| 264 | bear considerable resemblance to some passes of the CompCert |
---|
[3212] | 265 | compiler~\cite{Blazy-Leroy-Clight-09,Leroy-backend}, although we use a simpler \textsf{Cminor} where |
---|
[3181] | 266 | all loops use \lstinline[language=C]'goto' statements, and the |
---|
| 267 | \textsf{RTLabs} language retains a target-independent flavour. The |
---|
| 268 | back-end takes \textsf{RTLabs} code as input. |
---|
| 269 | |
---|
| 270 | The whole compilation function returns the following information on success: |
---|
[3128] | 271 | \begin{lstlisting}[language=matita] |
---|
[3214] | 272 | record compiler_output : Type[0] := |
---|
| 273 | { c_labelled_object_code: labelled_object_code |
---|
| 274 | ; c_stack_cost: stack_cost_model |
---|
| 275 | ; c_max_stack: nat |
---|
| 276 | ; c_init_costlabel: costlabel |
---|
| 277 | ; c_labelled_clight: clight_program |
---|
| 278 | ; c_clight_cost_map: clight_cost_map |
---|
| 279 | }. |
---|
[3128] | 280 | \end{lstlisting} |
---|
| 281 | It consists of annotated 8051 object code, a mapping from function |
---|
[3214] | 282 | identifiers to the function's stack space usage, the space available for the |
---|
[3173] | 283 | stack after global variable allocation, a cost label covering the |
---|
| 284 | execution time for the initialisation of global variables and the call |
---|
| 285 | to the \lstinline[language=C]'main' function, the annotated source |
---|
| 286 | code, and finally a mapping from cost labels to actual execution time |
---|
| 287 | costs. |
---|
[3128] | 288 | |
---|
[3214] | 289 | An \ocaml{} pretty printer is used to provide a concrete version of |
---|
| 290 | the output code and annotated source code. In the case of the |
---|
| 291 | annotated source code, it also inserts the actual costs alongside the |
---|
| 292 | cost labels, and optionally adds a global cost variable and |
---|
[3231] | 293 | instrumentation to support further reasoning in external tools such as |
---|
| 294 | Frama-C. |
---|
[3128] | 295 | |
---|
| 296 | \subsection{Revisions to the prototype compiler} |
---|
| 297 | |
---|
[3181] | 298 | Our focus on intensional properties prompted us to consider whether we |
---|
| 299 | could incorporate stack space into the costs presented to the user. |
---|
| 300 | We only allocate one fixed-size frame per function, so modelling this |
---|
| 301 | was relatively simple. It is the only form of dynamic memory |
---|
| 302 | allocation provided by the compiler, so we were able to strengthen the |
---|
| 303 | statement of the goal to guarantee successful execution whenever the |
---|
[3214] | 304 | stack space obeys the \lstinline'c_max_stack' bound calculated by |
---|
| 305 | subtracting the global variable requirements from the total memory |
---|
| 306 | available. |
---|
[3128] | 307 | |
---|
[3214] | 308 | The cost labelling checks at the end of Figure~\ref{fig:summary} have been |
---|
[3181] | 309 | introduced to reduce the proof burden, and are described in |
---|
| 310 | Section~\ref{sec:costchecks}. |
---|
[3159] | 311 | |
---|
[3181] | 312 | The use of dependent types to capture simple intermediate language |
---|
[3231] | 313 | invariants makes every front-end pass a total function, except |
---|
| 314 | \textsf{Clight} to \textsf{Cminor} and the cost checks. Hence various |
---|
| 315 | well-formedness and type safety checks are performed only once between |
---|
[3214] | 316 | \textsf{Clight} and \textsf{Cminor}, and the invariants rule out any |
---|
[3231] | 317 | difficulties in the later stages. With the benefit of hindsight we |
---|
| 318 | would have included an initial checking phase to produce a |
---|
| 319 | `well-formed' variant of \textsf{Clight}, conjecturing that this would |
---|
| 320 | simplify various parts of the proofs for the \textsf{Clight} stages |
---|
| 321 | which deal with potentially ill-formed code. |
---|
[3181] | 322 | |
---|
[3231] | 323 | Following D2.2, we previously generated code for global variable |
---|
[3223] | 324 | initialisation in \textsf{Cminor}, for which we reserved a cost label |
---|
| 325 | to represent the execution time for initialisation. However, the |
---|
| 326 | back-end must also add an initial call to the main function, whose |
---|
| 327 | cost must also be accounted for, so we decided to move the |
---|
| 328 | initialisation code to the back-end and merge the costs. |
---|
[3181] | 329 | |
---|
[3231] | 330 | \subsection{Main correctness statement} |
---|
[3128] | 331 | |
---|
| 332 | Informally, our main intensional result links the time difference in a source |
---|
| 333 | code execution to the time difference in the object code, expressing the time |
---|
| 334 | for the source by summing the values for the cost labels in the trace, and the |
---|
| 335 | time for the target by a clock built in to the 8051 executable semantics. |
---|
| 336 | |
---|
| 337 | The availability of precise timing information for 8501 |
---|
| 338 | implementations and the design of the compiler allow it to give exact |
---|
[3173] | 339 | time costs in terms of processor cycles, not just upper bounds. |
---|
| 340 | However, these exact results are only available if the subtrace we |
---|
| 341 | measure starts and ends at suitable points. In particular, pure |
---|
| 342 | computation with no observable effects may be reordered and moved past |
---|
| 343 | cost labels, so we cannot measure time between arbitrary statements in |
---|
| 344 | the program. |
---|
[3128] | 345 | |
---|
| 346 | There is also a constraint on the subtraces that we |
---|
| 347 | measure due to the requirements of the correctness proof for the |
---|
| 348 | object code timing analysis. To be sure that the timings are assigned |
---|
| 349 | to the correct cost label, we need to know that each return from a |
---|
| 350 | function call must go to the correct return address. It is difficult |
---|
| 351 | to observe this property locally in the object code because it relies |
---|
| 352 | on much earlier stages in the compiler. To convey this information to |
---|
| 353 | the timing analysis extra structure is imposed on the subtraces, which |
---|
[3173] | 354 | is described in Section~\ref{sec:fegoals}. |
---|
[3128] | 355 | |
---|
| 356 | % Regarding the footnote, would there even be much point? |
---|
[3173] | 357 | % TODO: this might be quite easy to add ('just' subtract the |
---|
| 358 | % measurable subtrace from the second label to the end). Could also |
---|
| 359 | % measure other traces in this manner. |
---|
[3128] | 360 | These restrictions are reflected in the subtraces that we give timing |
---|
| 361 | guarantees on; they must start at a cost label and end at the return |
---|
| 362 | of the enclosing function of the cost label\footnote{We expect that |
---|
[3216] | 363 | this would generalise to more general subtraces by subtracting costs |
---|
| 364 | for unwanted measurable suffixes of a measurable subtrace.}. A |
---|
| 365 | typical example of such a subtrace is the execution of an entire |
---|
| 366 | function from the cost label at the start of the function until it |
---|
| 367 | returns. We call such any such subtrace \emph{measurable} if it (and |
---|
| 368 | the prefix of the trace from the start to the subtrace) can also be |
---|
| 369 | executed within the available stack space. |
---|
[3128] | 370 | |
---|
| 371 | Now we can give the main intensional statement for the compiler. |
---|
| 372 | Given a \emph{measurable} subtrace for a labelled \textsf{Clight} |
---|
| 373 | program, there is a subtrace of the 8051 object code program where the |
---|
| 374 | time differences match. Moreover, \emph{observable} parts of the |
---|
| 375 | trace also match --- these are the appearance of cost labels and |
---|
| 376 | function calls and returns. |
---|
| 377 | |
---|
[3216] | 378 | |
---|
| 379 | |
---|
[3128] | 380 | More formally, the definition of this statement in \matita{} is |
---|
| 381 | \begin{lstlisting}[language=matita] |
---|
| 382 | definition simulates := |
---|
| 383 | $\lambda$p: compiler_output. |
---|
[3216] | 384 | let initial_status := initialise_status $...$ (cm (c_labelled_object_code $...$ p)) in |
---|
[3128] | 385 | $\forall$m1,m2. |
---|
[3216] | 386 | measurable Clight_pcs (c_labelled_clight $...$ p) m1 m2 |
---|
| 387 | (stack_sizes (c_stack_cost $...$ p)) (c_max_stack $...$ p) $\rightarrow$ |
---|
[3128] | 388 | $\forall$c1,c2. |
---|
[3216] | 389 | clock_after Clight_pcs (c_labelled_clight $...$ p) m1 (c_clight_cost_map $...$ p) = OK $...$ c1 $\rightarrow$ |
---|
| 390 | clock_after Clight_pcs (c_labelled_clight $...$ p) (m1+m2) (c_clight_cost_map $...$ p) = OK $...$ c2 $\rightarrow$ |
---|
[3128] | 391 | $\exists$n1,n2. |
---|
[3216] | 392 | observables Clight_pcs (c_labelled_clight $...$ p) m1 m2 = |
---|
| 393 | observables (OC_preclassified_system (c_labelled_object_code $...$ p)) |
---|
| 394 | (c_labelled_object_code $...$ p) n1 n2 |
---|
[3128] | 395 | $\wedge$ |
---|
[3216] | 396 | clock ?? (execute (n1+n2) ? initial_status) = |
---|
| 397 | clock ?? (execute n1 ? initial_status) + (c2-c1). |
---|
[3128] | 398 | \end{lstlisting} |
---|
| 399 | where the \lstinline'measurable', \lstinline'clock_after' and |
---|
[3216] | 400 | \lstinline'observables' definitions are generic definitions for multiple |
---|
[3128] | 401 | languages; in this case the \lstinline'Clight_pcs' record applies them |
---|
| 402 | to \textsf{Clight} programs. |
---|
| 403 | |
---|
[3131] | 404 | There is a second part to the statement, which says that the initial |
---|
| 405 | processing of the input program to produce the cost labelled version |
---|
| 406 | does not affect the semantics of the program: |
---|
| 407 | % Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function |
---|
| 408 | \begin{lstlisting}[language=matita] |
---|
| 409 | $\forall$input_program,output. |
---|
| 410 | compile input_program = return output $\rightarrow$ |
---|
[3216] | 411 | not_wrong $...$ (exec_inf $...$ clight_fullexec input_program) $\rightarrow$ |
---|
[3131] | 412 | sim_with_labels |
---|
[3216] | 413 | (exec_inf $...$ clight_fullexec input_program) |
---|
| 414 | (exec_inf $...$ clight_fullexec (c_labelled_clight $...$ output)) |
---|
[3131] | 415 | \end{lstlisting} |
---|
| 416 | That is, any successful compilation produces a labelled program that |
---|
| 417 | has identical behaviour to the original, so long as there is no |
---|
| 418 | `undefined behaviour'. |
---|
[3128] | 419 | |
---|
[3216] | 420 | Note that this statement provides full functional correctness, including |
---|
[3131] | 421 | preservation of (non-)termination. The intensional result above does |
---|
| 422 | not do this directly --- it does not guarantee the same result or same |
---|
| 423 | termination. There are two mitigating factors, however: first, to |
---|
[3216] | 424 | prove the intensional property you need local simulation results --- these |
---|
[3131] | 425 | can be pieced together to form full behavioural equivalence, only time |
---|
| 426 | constraints have prevented us from doing so. Second, if we wish to |
---|
| 427 | confirm a result, termination, or non-termination we could add an |
---|
| 428 | observable witness, such as a function that is only called if the |
---|
| 429 | correct result is given. The intensional result guarantees that the |
---|
| 430 | observable witness is preserved, so the program must behave correctly. |
---|
| 431 | |
---|
[3226] | 432 | These two results are combined in the the \lstinline'correct' |
---|
| 433 | theorem in the file \lstinline'correctness.ma'. |
---|
| 434 | |
---|
[3231] | 435 | \section{Correctness statement for the front-end} |
---|
[3128] | 436 | \label{sec:fegoals} |
---|
| 437 | |
---|
| 438 | The essential parts of the intensional proof were outlined during work |
---|
[3216] | 439 | on a toy compiler in Task |
---|
| 440 | 2.1~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}. These are |
---|
[3128] | 441 | \begin{enumerate} |
---|
| 442 | \item functional correctness, in particular preserving the trace of |
---|
| 443 | cost labels, |
---|
| 444 | \item the \emph{soundness} and \emph{precision} of the cost labelling |
---|
| 445 | on the object code, and |
---|
| 446 | \item the timing analysis on the object code produces a correct |
---|
| 447 | mapping from cost labels to time. |
---|
| 448 | \end{enumerate} |
---|
| 449 | |
---|
| 450 | However, that toy development did not include function calls. For the |
---|
| 451 | full \cerco{} compiler we also need to maintain the invariant that |
---|
| 452 | functions return to the correct program location in the caller, as we |
---|
| 453 | mentioned in the previous section. During work on the back-end timing |
---|
| 454 | analysis (describe in more detail in the companion deliverable, D4.4) |
---|
| 455 | the notion of a \emph{structured trace} was developed to enforce this |
---|
| 456 | return property, and also most of the cost labelling properties too. |
---|
| 457 | |
---|
| 458 | \begin{figure} |
---|
| 459 | \begin{center} |
---|
| 460 | \includegraphics[width=0.5\linewidth]{compiler.pdf} |
---|
| 461 | \end{center} |
---|
| 462 | \caption{The compiler and proof outline} |
---|
| 463 | \label{fig:compiler} |
---|
| 464 | \end{figure} |
---|
| 465 | |
---|
| 466 | Jointly, we generalised the structured traces to apply to any of the |
---|
[3216] | 467 | intermediate languages which have some idea of program counter. This means |
---|
[3128] | 468 | that they are introduced part way through the compiler, see |
---|
| 469 | Figure~\ref{fig:compiler}. Proving that a structured trace can be |
---|
| 470 | constructed at \textsf{RTLabs} has several virtues: |
---|
| 471 | \begin{itemize} |
---|
| 472 | \item This is the first language where every operation has its own |
---|
| 473 | unique, easily addressable, statement. |
---|
[3173] | 474 | \item Function calls and returns are still handled implicitly in the |
---|
| 475 | language and so the structural properties are ensured by the |
---|
| 476 | semantics. |
---|
[3216] | 477 | \item Many of the back-end languages from \textsf{RTL} onwards share a common |
---|
[3128] | 478 | core set of definitions, and using structured traces throughout |
---|
| 479 | increases this uniformity. |
---|
| 480 | \end{itemize} |
---|
| 481 | |
---|
[3140] | 482 | \begin{figure} |
---|
| 483 | \begin{center} |
---|
| 484 | \includegraphics[width=0.6\linewidth]{strtraces.pdf} |
---|
| 485 | \end{center} |
---|
| 486 | \caption{Nesting of functions in structured traces} |
---|
| 487 | \label{fig:strtrace} |
---|
| 488 | \end{figure} |
---|
[3173] | 489 | A structured trace is a mutually inductive data type which |
---|
[3128] | 490 | contains the steps from a normal program trace, but arranged into a |
---|
| 491 | nested structure which groups entire function calls together and |
---|
| 492 | aggregates individual steps between cost labels (or between the final |
---|
[3140] | 493 | cost label and the return from the function), see |
---|
[3173] | 494 | Figure~\ref{fig:strtrace}. This captures the idea that the cost labels |
---|
[3140] | 495 | only represent costs \emph{within} a function --- calls to other |
---|
[3173] | 496 | functions are accounted for in the nested trace for their execution, and we |
---|
[3140] | 497 | can locally regard function calls as a single step. |
---|
[3128] | 498 | |
---|
| 499 | These structured traces form the core part of the intermediate results |
---|
| 500 | that we must prove so that the back-end can complete the main |
---|
| 501 | intensional result stated above. In full, we provide the back-end |
---|
| 502 | with |
---|
| 503 | \begin{enumerate} |
---|
| 504 | \item A normal trace of the \textbf{prefix} of the program's execution |
---|
| 505 | before reaching the measurable subtrace. (This needs to be |
---|
[3173] | 506 | preserved so that we know that the stack space consumed is correct, |
---|
| 507 | and to set up the simulation results.) |
---|
[3128] | 508 | \item The \textbf{structured trace} corresponding to the measurable |
---|
| 509 | subtrace. |
---|
| 510 | \item An additional property about the structured trace that no |
---|
[3131] | 511 | `program counter' is \textbf{repeated} between cost labels. Together with |
---|
[3128] | 512 | the structure in the trace, this takes over from showing that |
---|
| 513 | cost labelling is sound and precise. |
---|
[3131] | 514 | \item A proof that the \textbf{observables} have been preserved. |
---|
| 515 | \item A proof that the \textbf{stack limit} is still observed by the prefix and |
---|
[3128] | 516 | the structure trace. (This is largely a consequence of the |
---|
| 517 | preservation of observables.) |
---|
| 518 | \end{enumerate} |
---|
[3226] | 519 | The \lstinline'front_end_correct' lemma in the |
---|
| 520 | \lstinline'correctness.ma' file provides a record containing these. |
---|
[3128] | 521 | |
---|
| 522 | Following the outline in Figure~\ref{fig:compiler}, we will first deal |
---|
| 523 | with the transformations in \textsf{Clight} that produce the source |
---|
| 524 | program with cost labels, then show that measurable traces can be |
---|
[3216] | 525 | lifted to \textsf{RTLabs}, and finally show that we can construct the |
---|
[3128] | 526 | properties listed above ready for the back-end proofs. |
---|
| 527 | |
---|
| 528 | \section{Input code to cost labelled program} |
---|
[3212] | 529 | \label{sec:inputtolabelling} |
---|
[3128] | 530 | |
---|
[3181] | 531 | As explained on page~\pageref{page:switchintro}, the costs of complex |
---|
| 532 | C \lstinline[language=C]'switch' statements cannot be represented with |
---|
[3216] | 533 | the simple labelling used in the formalised compiler. Our first pass |
---|
| 534 | replaces these statements with simpler C code, allowing our second |
---|
| 535 | pass to perform the cost labelling. We show that the behaviour of |
---|
| 536 | programs is unchanged by these passes using forward |
---|
| 537 | simulations\footnote{All of our languages are deterministic, which can |
---|
| 538 | be seen directly from their executable definitions. Thus we know that |
---|
| 539 | forward simulations are sufficient because the target cannot have any |
---|
| 540 | other behaviour.}. |
---|
[3138] | 541 | |
---|
[3211] | 542 | \subsection{Switch removal} |
---|
[3138] | 543 | |
---|
[3216] | 544 | We compile away \lstinline[language=C]'switch' statements into more |
---|
| 545 | basic \textsf{Clight} code. |
---|
[3211] | 546 | Note that this transformation does not necessarily deteriorate the |
---|
| 547 | efficiency of the generated code. For instance, compilers such as GCC |
---|
| 548 | introduce balanced trees of ``if-then-else'' constructs for small |
---|
| 549 | switches. However, our implementation strategy is much simpler. Let |
---|
| 550 | us consider the following input statement. |
---|
| 551 | |
---|
| 552 | \begin{lstlisting}[language=C] |
---|
| 553 | switch(e) { |
---|
| 554 | case v1: |
---|
| 555 | stmt1; |
---|
| 556 | case v2: |
---|
| 557 | stmt2; |
---|
| 558 | default: |
---|
| 559 | stmt_default; |
---|
| 560 | } |
---|
| 561 | \end{lstlisting} |
---|
| 562 | |
---|
| 563 | Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default} |
---|
| 564 | may contain \lstinline[language=C]'break' statements, which have the |
---|
| 565 | effect of exiting the switch statement. In the absence of break, the |
---|
[3216] | 566 | execution falls through each case sequentially. In our implementation, |
---|
[3211] | 567 | we produce an equivalent sequence of ``if-then'' chained by gotos: |
---|
| 568 | \begin{lstlisting}[language=C] |
---|
| 569 | fresh = e; |
---|
| 570 | if(fresh == v1) { |
---|
| 571 | $\llbracket$stmt1$\rrbracket$; |
---|
| 572 | goto lbl_case2; |
---|
| 573 | }; |
---|
| 574 | if(fresh == v2) { |
---|
| 575 | lbl_case2: |
---|
[3216] | 576 | $\llbracket$stmt2$\rrbracket$; |
---|
[3211] | 577 | goto lbl_case2; |
---|
| 578 | }; |
---|
| 579 | $\llbracket$stmt_default$\rrbracket$; |
---|
| 580 | exit_label: |
---|
| 581 | \end{lstlisting} |
---|
| 582 | |
---|
| 583 | The proof had to tackle the following points: |
---|
| 584 | \begin{itemize} |
---|
[3216] | 585 | \item the source and target memories are not the same (due to the fresh variable), |
---|
[3211] | 586 | \item the flow of control is changed in a non-local way (e.g. \textbf{goto} |
---|
| 587 | instead of \textbf{break}). |
---|
| 588 | \end{itemize} |
---|
| 589 | In order to tackle the first point, we implemented a version of memory |
---|
[3231] | 590 | extensions similar to those of CompCert. |
---|
[3211] | 591 | |
---|
[3223] | 592 | For the simulation we decided to prove a sufficient amount to give us |
---|
| 593 | confidence in the definitions and approach, but curtail the proof |
---|
| 594 | because this pass does not contribute to the intensional correctness |
---|
| 595 | result. We tackled several simple cases, that do not interact with |
---|
| 596 | the switch removal per se, to show that the definitions were usable, |
---|
| 597 | and part of the switch case to check that the approach is |
---|
| 598 | reasonable. This comprises propagating the memory extension through |
---|
| 599 | each statement (except switch), as well as various invariants that are |
---|
| 600 | needed for the switch case (in particular, freshness hypotheses). The |
---|
| 601 | details of the evaluation process for the source switch statement and |
---|
| 602 | its target counterpart can be found in the file |
---|
[3226] | 603 | \lstinline'switchRemoval.ma', along more details on the transformation |
---|
[3223] | 604 | itself. |
---|
| 605 | |
---|
[3211] | 606 | Proving the correctness of the second point would require reasoning on the |
---|
| 607 | semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} |
---|
| 608 | semantics, this is implemented as a function-wide lookup of the target label. |
---|
| 609 | The invariant we would need is the fact that a global label lookup on a freshly |
---|
| 610 | created goto is equivalent to a local lookup. This would in turn require the |
---|
[3231] | 611 | propagation of some freshness hypotheses on labels. As discussed, |
---|
[3211] | 612 | we decided to omit this part of the correctness proof. |
---|
| 613 | |
---|
| 614 | \subsection{Cost labelling} |
---|
| 615 | |
---|
| 616 | The simulation for the cost labelling pass is the simplest in the |
---|
| 617 | front-end. The main argument is that any step of the source program |
---|
| 618 | is simulated by the same step of the labelled one, plus any extra |
---|
| 619 | steps for the added cost labels. The extra instructions do not change |
---|
| 620 | the memory or local environments, although we have to keep track of |
---|
[3216] | 621 | the extra instructions that appear in continuations, for example |
---|
| 622 | during the execution of a \lstinline[language=C]'while' loop. |
---|
[3211] | 623 | |
---|
[3231] | 624 | We do not attempt to capture any cost properties of the labelling\footnote{We describe how the cost properties are |
---|
| 625 | established in Section~\ref{sec:costchecks}.} in |
---|
| 626 | the simulation proof, which allows the proof to be oblivious to the choice |
---|
[3211] | 627 | of cost labels. Hence we do not have to reason about the threading of |
---|
| 628 | name generation through the labelling function, greatly reducing the |
---|
[3216] | 629 | amount of effort required. |
---|
[3211] | 630 | |
---|
| 631 | %TODO: both give one-step-sim-by-many forward sim results; switch |
---|
| 632 | %removal tricky, uses aux var to keep result of expr, not central to |
---|
| 633 | %intensional correctness so curtailed proof effort once reasonable |
---|
| 634 | %level of confidence in code gained; labelling much simpler; don't care |
---|
| 635 | %what the labels are at this stage, just need to know when to go |
---|
| 636 | %through extra steps. Rolled up into a single result with a cofixpoint |
---|
| 637 | %to obtain coinductive statement of equivalence (show). |
---|
| 638 | |
---|
[3128] | 639 | \section{Finding corresponding measurable subtraces} |
---|
[3212] | 640 | \label{sec:measurablelifting} |
---|
[3128] | 641 | |
---|
[3142] | 642 | There follow the three main passes of the front-end: |
---|
| 643 | \begin{enumerate} |
---|
| 644 | \item simplification of casts in \textsf{Clight} code |
---|
| 645 | \item \textsf{Clight} to \textsf{Cminor} translation, performing stack |
---|
| 646 | variable allocation and simplifying control structures |
---|
| 647 | \item transformation to \textsf{RTLabs} control flow graph |
---|
| 648 | \end{enumerate} |
---|
[3216] | 649 | We have taken a common approach to |
---|
[3158] | 650 | each pass: first we build (or axiomatise) forward simulation results |
---|
[3216] | 651 | that are similar to normal compiler proofs, but which are slightly more |
---|
[3158] | 652 | fine-grained so that we can see that the call structure and relative |
---|
| 653 | placement of cost labels is preserved. |
---|
[3142] | 654 | |
---|
[3158] | 655 | Then we instantiate a general result which shows that we can find a |
---|
| 656 | \emph{measurable} subtrace in the target of the pass that corresponds |
---|
[3173] | 657 | to the measurable subtrace in the source. By repeated application of |
---|
[3158] | 658 | this result we can find a measurable subtrace of the execution of the |
---|
| 659 | \textsf{RTLabs} code, suitable for the construction of a structured |
---|
[3216] | 660 | trace (see Section~\ref{sec:structuredtrace}). This is essentially an |
---|
[3158] | 661 | extra layer on top of the simulation proofs that provides us with the |
---|
[3216] | 662 | additional information required for our intensional correctness proof. |
---|
[3142] | 663 | |
---|
| 664 | \subsection{Generic measurable subtrace lifting proof} |
---|
| 665 | |
---|
[3158] | 666 | Our generic proof is parametrised on a record containing small-step |
---|
| 667 | semantics for the source and target language, a classification of |
---|
| 668 | states (the same form of classification is used when defining |
---|
[3216] | 669 | structured traces), a simulation relation which respects the |
---|
| 670 | classification and cost labelling and |
---|
| 671 | four simulation results. The simulations are split by the starting state's |
---|
| 672 | classification and whether it is a cost label, which will allow us to |
---|
| 673 | observe that the call structure is preserved. They are: |
---|
[3158] | 674 | \begin{enumerate} |
---|
| 675 | \item a step from a `normal' state (which is not classified as a call |
---|
| 676 | or return) which is not a cost label is simulated by zero or more |
---|
| 677 | `normal' steps; |
---|
| 678 | \item a step from a `call' state followed by a cost label step is |
---|
| 679 | simulated by a step from a `call' state, a corresponding label step, |
---|
| 680 | then zero or more `normal' steps; |
---|
| 681 | \item a step from a `call' state not followed by a cost label |
---|
| 682 | similarly (note that this case cannot occur in a well-labelled |
---|
| 683 | program, but we do not have enough information locally to exploit |
---|
| 684 | this); and |
---|
| 685 | \item a cost label step is simulated by a cost label step. |
---|
| 686 | \end{enumerate} |
---|
| 687 | Finally, we need to know that a successfully translated program will |
---|
| 688 | have an initial state in the simulation relation with the original |
---|
| 689 | program's initial state. |
---|
[3142] | 690 | |
---|
[3227] | 691 | The back-end has similar requirements for lifting simulations to |
---|
| 692 | structured traces. Fortunately, our treatment of calls and returns |
---|
| 693 | can be slightly simpler because we have special call and return states |
---|
| 694 | that correspond to function entry and return that are separate from |
---|
| 695 | the actual instructions. This was originally inherited from our port |
---|
| 696 | of CompCert's \textsf{Clight} semantics, but proves useful here |
---|
| 697 | because we only need to consider adding extra steps \emph{after} a |
---|
| 698 | call or return state, because the instruction step deals with extra |
---|
| 699 | steps that occur before. The back-end makes all of the call and |
---|
| 700 | return machinery explicit, and thus needs more complex statements |
---|
| 701 | about extra steps before and after each call and return. |
---|
| 702 | |
---|
[3158] | 703 | \begin{figure} |
---|
| 704 | \begin{center} |
---|
| 705 | \includegraphics[width=0.5\linewidth]{meassim.pdf} |
---|
| 706 | \end{center} |
---|
| 707 | \caption{Tiling of simulation for a measurable subtrace} |
---|
| 708 | \label{fig:tiling} |
---|
| 709 | \end{figure} |
---|
| 710 | |
---|
| 711 | To find the measurable subtrace in the target program's execution we |
---|
| 712 | walk along the original program's execution trace applying the |
---|
| 713 | appropriate simulation result by induction on the number of steps. |
---|
| 714 | While the number of steps taken varies, the overall structure is |
---|
| 715 | preserved, as illustrated in Figure~\ref{fig:tiling}. By preserving |
---|
| 716 | the structure we also maintain the same intensional observables. One |
---|
| 717 | delicate point is that the cost label following a call must remain |
---|
| 718 | directly afterwards\footnote{The prototype compiler allowed some |
---|
| 719 | straight-line code to appear before the cost label until a later |
---|
| 720 | stage of the compiler, but we must move the requirement forward to |
---|
| 721 | fit with the structured traces.} |
---|
| 722 | % Damn it, I should have just moved the cost label forwards in RTLabs, |
---|
| 723 | % like the prototype does in RTL to ERTL; the result would have been |
---|
| 724 | % simpler. Or was there some reason not to do that? |
---|
| 725 | (both in the program code and in the execution trace), even if we |
---|
| 726 | introduce extra steps, for example to store parameters in memory in |
---|
| 727 | \textsf{Cminor}. Thus we have a version of the call simulation |
---|
[3231] | 728 | that deals with both the call and the cost label in one result. |
---|
[3158] | 729 | |
---|
[3231] | 730 | In addition to the subtrace we are interested in measuring, we must |
---|
| 731 | prove that the earlier part of the trace is also preserved in |
---|
| 732 | order to use the simulation from the initial state. This proof also |
---|
[3158] | 733 | guarantees that we do not run out of stack space before the subtrace |
---|
| 734 | we are interested in. The lemmas for this prefix and the measurable |
---|
| 735 | subtrace are similar, following the pattern above. However, the |
---|
| 736 | measurable subtrace also requires us to rebuild the termination |
---|
[3173] | 737 | proof. This is defined recursively: |
---|
| 738 | \label{prog:terminationproof} |
---|
[3158] | 739 | \begin{lstlisting}[language=matita] |
---|
[3216] | 740 | let rec will_return_aux C (depth:nat) |
---|
[3231] | 741 | (trace:list (cs_state $...$ C $\times$ trace)) on trace : bool := |
---|
[3216] | 742 | match trace with |
---|
| 743 | [ nil $\Rightarrow$ false |
---|
| 744 | | cons h tl $\Rightarrow$ |
---|
| 745 | let $\langle$s,tr$\rangle$ := h in |
---|
| 746 | match cs_classify C s with |
---|
| 747 | [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl |
---|
| 748 | | cl_return $\Rightarrow$ |
---|
| 749 | match depth with |
---|
| 750 | [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ] |
---|
| 751 | | S d $\Rightarrow$ will_return_aux C d tl |
---|
| 752 | ] |
---|
| 753 | | _ $\Rightarrow$ will_return_aux C depth tl |
---|
| 754 | ] |
---|
| 755 | ]. |
---|
[3158] | 756 | \end{lstlisting} |
---|
| 757 | The \lstinline'depth' is the number of return states we need to see |
---|
| 758 | before we have returned to the original function (initially zero) and |
---|
| 759 | \lstinline'trace' the measurable subtrace obtained from the running |
---|
| 760 | the semantics for the correct number of steps. This definition |
---|
| 761 | unfolds tail recursively for each step, and once the corresponding |
---|
| 762 | simulation result has been applied a new one for the target can be |
---|
| 763 | asserted by unfolding and applying the induction hypothesis on the |
---|
| 764 | shorter trace. |
---|
| 765 | |
---|
[3227] | 766 | Combining the lemmas about the prefix and the measurable subtrace |
---|
| 767 | requires a little care because the states joining the two might not be |
---|
[3231] | 768 | related in the simulation. In particular, if the measurable subtrace |
---|
[3227] | 769 | starts from the cost label at the beginning of the function there may |
---|
| 770 | be some extra instructions in the target code to execute to complete |
---|
| 771 | function entry before the states are back in the relation. Hence we |
---|
[3231] | 772 | carefully phrased the lemmas to allow for such extra steps. |
---|
[3227] | 773 | |
---|
| 774 | Together, these then gives us an overall result for any simulation fitting the |
---|
[3158] | 775 | requirements above (contained in the \lstinline'meas_sim' record): |
---|
| 776 | \begin{lstlisting}[language=matita] |
---|
| 777 | theorem measured_subtrace_preserved : |
---|
| 778 | $\forall$MS:meas_sim. |
---|
| 779 | $\forall$p1,p2,m,n,stack_cost,max. |
---|
| 780 | ms_compiled MS p1 p2 $\rightarrow$ |
---|
| 781 | measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$ |
---|
| 782 | $\exists$m',n'. |
---|
| 783 | measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$ |
---|
| 784 | observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. |
---|
| 785 | \end{lstlisting} |
---|
| 786 | The stack space requirement that is embedded in \lstinline'measurable' |
---|
[3216] | 787 | is a consequence of the preservation of observables, because it is |
---|
| 788 | determined by the functions called and returned from, which are observable. |
---|
[3158] | 789 | |
---|
[3142] | 790 | \subsection{Simulation results for each pass} |
---|
| 791 | |
---|
[3216] | 792 | We now consider the simulation results for the passes, each of which |
---|
| 793 | is used to instantiate the |
---|
| 794 | \lstinline[language=matita]'measured_subtrace_preserved' theorem to |
---|
| 795 | construct the measurable subtrace for the next language. |
---|
[3168] | 796 | |
---|
[3216] | 797 | \subsubsection{Cast simplification} |
---|
| 798 | |
---|
| 799 | The parser used in \cerco{} introduces a lot of explicit type casts. |
---|
[3191] | 800 | If left as they are, these constructs can greatly hamper the |
---|
| 801 | quality of the generated code -- especially as the architecture |
---|
[3216] | 802 | we consider is an $8$-bit one. In \textsf{Clight}, casts are |
---|
[3191] | 803 | expressions. Hence, most of the work of this transformation |
---|
| 804 | proceeds on expressions. The tranformation proceeds by recursively |
---|
| 805 | trying to coerce an expression to a particular integer type, which |
---|
| 806 | is in practice smaller than the original one. This functionality |
---|
| 807 | is implemented by two mutually recursive functions whose signature |
---|
| 808 | is the following. |
---|
[3168] | 809 | |
---|
[3191] | 810 | \begin{lstlisting}[language=matita] |
---|
| 811 | let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) |
---|
[3216] | 812 | : $\Sigma$result:bool$\times$expr. |
---|
| 813 | $\forall$ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) := $\ldots$ |
---|
[3168] | 814 | |
---|
[3216] | 815 | and simplify_inside (e:expr) : $\Sigma$result:expr. conservation e result := $\ldots$ |
---|
[3191] | 816 | \end{lstlisting} |
---|
[3168] | 817 | |
---|
[3191] | 818 | The \textsf{simplify\_inside} acts as a wrapper for |
---|
| 819 | \textsf{simplify\_expr}. Whenever \textsf{simplify\_inside} encounters |
---|
| 820 | a \textsf{Ecast} expression, it tries to coerce the sub-expression |
---|
| 821 | to the desired type using \textsf{simplify\_expr}, which tries to |
---|
| 822 | perform the actual coercion. In return, \textsf{simplify\_expr} calls |
---|
| 823 | back \textsf{simplify\_inside} in some particular positions, where we |
---|
| 824 | decided to be conservative in order to simplify the proofs. However, |
---|
| 825 | the current design allows to incrementally revert to a more aggressive |
---|
| 826 | version, by replacing recursive calls to \textsf{simplify\_inside} by |
---|
| 827 | calls to \textsf{simplify\_expr} \emph{and} proving the corresponding |
---|
| 828 | invariants -- where possible. |
---|
[3168] | 829 | |
---|
[3191] | 830 | The \textsf{simplify\_inv} invariant encodes either the conservation |
---|
| 831 | of the semantics during the transformation corresponding to the failure |
---|
[3231] | 832 | of the coercion (\textsf{Inv\_eq} constructor), or the successful |
---|
[3191] | 833 | downcast of the considered expression to the target type |
---|
| 834 | (\textsf{Inv\_coerce\_ok}). |
---|
[3168] | 835 | |
---|
[3191] | 836 | \begin{lstlisting}[language=matita] |
---|
| 837 | inductive simplify_inv |
---|
| 838 | (ge : genv) (en : env) (m : mem) |
---|
[3216] | 839 | (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool $\rightarrow$ Prop := |
---|
| 840 | | Inv_eq : $\forall$result_flag. $\ldots$ |
---|
[3191] | 841 | simplify_inv ge en m e1 e2 target_sz target_sg result_flag |
---|
[3216] | 842 | | Inv_coerce_ok : $\forall$src_sz,src_sg. |
---|
| 843 | typeof e1 = Tint src_sz src_sg $\rightarrow$ |
---|
| 844 | typeof e2 = Tint target_sz target_sg $\rightarrow$ |
---|
| 845 | smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2) $\rightarrow$ |
---|
[3191] | 846 | simplify_inv ge en m e1 e2 target_sz target_sg true. |
---|
| 847 | \end{lstlisting} |
---|
[3168] | 848 | |
---|
[3216] | 849 | The \textsf{conservation} invariant for \textsf{simplify\_inside} simply states the conservation |
---|
[3191] | 850 | of the semantics, as in the \textsf{Inv\_eq} constructor of the previous |
---|
| 851 | invariant. |
---|
| 852 | |
---|
| 853 | \begin{lstlisting}[language=matita] |
---|
[3216] | 854 | definition conservation := $\lambda$e,result. $\forall$ge,en,m. |
---|
[3191] | 855 | res_sim ? (exec_expr ge en m e) (exec_expr ge en m result) |
---|
[3216] | 856 | $\wedge$ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) |
---|
| 857 | $\wedge$ typeof e = typeof result. |
---|
[3191] | 858 | \end{lstlisting} |
---|
| 859 | |
---|
| 860 | This invariant is then easily lifted to statement evaluations. |
---|
| 861 | The main problem encountered with this particular pass was dealing with |
---|
| 862 | inconsistently typed programs, a canonical case being a particular |
---|
| 863 | integer constant of a certain size typed with another size. This |
---|
[3216] | 864 | prompted the need to introduce numerous type checks, making |
---|
| 865 | both the implementation and the proof more complex, even though more |
---|
| 866 | comprehensive checks are made in the next stage. |
---|
[3223] | 867 | %\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} |
---|
[3191] | 868 | |
---|
[3218] | 869 | \subsubsection{Clight to Cminor} |
---|
[3168] | 870 | |
---|
[3216] | 871 | This pass is the last one operating on the \textsf{Clight} language. |
---|
| 872 | Its input is a full \textsf{Clight} program, and its output is a |
---|
| 873 | \textsf{Cminor} program. Note that we do not use an equivalent of |
---|
[3223] | 874 | CompCert's \textsf{C\#minor} language: we translate directly to a |
---|
[3216] | 875 | variant of \textsf{Cminor}. This presents the advantage of not |
---|
| 876 | requiring the special loop constructs, nor the explicit block |
---|
| 877 | structure. Another salient point of our approach is that a significant |
---|
| 878 | number of the properties needed for the simulation proof were directly |
---|
| 879 | encoded in dependently typed translation functions. In particular, |
---|
| 880 | freshness conditions and well-typedness conditions are included. The |
---|
| 881 | main effects of the transformation from \textsf{Clight} to |
---|
[3168] | 882 | \textsf{Cminor} are listed below. |
---|
| 883 | |
---|
| 884 | \begin{itemize} |
---|
| 885 | \item Variables are classified as being either globals, stack-allocated |
---|
| 886 | locals or potentially register-allocated locals. The value of register-allocated |
---|
| 887 | local variables is moved out of the modelled memory and stored in a |
---|
| 888 | dedicated environment. |
---|
[3216] | 889 | \item In \textsf{Clight}, each local variable has a dedicated memory block, whereas |
---|
[3168] | 890 | stack-allocated locals are bundled together on a function-by-function basis. |
---|
| 891 | \item Loops are converted to jumps. |
---|
| 892 | \end{itemize} |
---|
| 893 | |
---|
| 894 | The first two points require memory injections which are more flexible that those |
---|
| 895 | needed in the switch removal case. In the remainder of this section, we briefly |
---|
| 896 | discuss our implementation of memory injections, and then the simulation proof. |
---|
| 897 | |
---|
[3218] | 898 | \paragraph{Memory injections.} |
---|
[3168] | 899 | |
---|
| 900 | Our memory injections are modelled after the work of Blazy \& Leroy. |
---|
| 901 | However, the corresponding paper is based on the first version of the |
---|
[3231] | 902 | CompCert memory model~\cite{2008-Leroy-Blazy-memory-model}, whereas we use a much more concrete model, allowing byte-level |
---|
[3223] | 903 | manipulations (as in the later version of CompCert's memory model). We proved |
---|
[3231] | 904 | roughly 80 \% of the required lemmas. Notably, some of the difficulties encountered were |
---|
| 905 | due to overly relaxed conditions on pointer validity (fixed during development). |
---|
[3216] | 906 | Some more side conditions had to be added to take care of possible overflows when converting |
---|
[3231] | 907 | from \textbf{Z} block bounds to $16$ bit pointer offsets (in practice, such overflows |
---|
[3168] | 908 | only occur in edge cases that are easily ruled out -- but this fact is not visible |
---|
| 909 | in memory injections). Concretely, some of the lemmas on the preservation of simulation of |
---|
[3216] | 910 | loads after writes were axiomatised, due to a lack of time. |
---|
[3168] | 911 | |
---|
[3218] | 912 | \paragraph{Simulation proof.} |
---|
[3168] | 913 | |
---|
[3223] | 914 | We proved the simulation result for expressions and a representative |
---|
| 915 | selection of statements. In particular we tackled |
---|
| 916 | \lstinline[language=C]'while' statements to ensure that we correctly |
---|
| 917 | translate loops because our approach differs from CompCert by |
---|
| 918 | converting directly to \textsf{Cminor} \lstinline[language=C]'goto's |
---|
[3231] | 919 | rather than maintaining a notion of loop in \textsf{Cminor}. We also have a partial |
---|
[3223] | 920 | proof for function entry, covering the setup of the memory injection, |
---|
| 921 | but not function exit. Exits, and the remaining statements, have been |
---|
| 922 | axiomatised. |
---|
[3168] | 923 | |
---|
[3231] | 924 | Careful management of the proof state was required because proof terms |
---|
| 925 | are embedded in \textsf{Cminor} code to show that invariants are |
---|
| 926 | respected. These proof terms appear in the proof state when inverting |
---|
| 927 | the translation functions, and they can be large and awkward. While |
---|
| 928 | generalising them away is usually sufficient, it can be difficult when |
---|
| 929 | they appear under a binder. |
---|
[3168] | 930 | |
---|
[3223] | 931 | %The correctness proof for this transformation was not completed. We proved the |
---|
| 932 | %simulation result for expressions and for some subset of the critical statement cases. |
---|
| 933 | %Notably lacking are the function entry and exit, where the memory injection is |
---|
| 934 | %properly set up. As would be expected, a significant amount of work has to be performed |
---|
| 935 | %to show the conservation of all invariants at each simulation step. |
---|
| 936 | |
---|
| 937 | %\todo{list cases, explain while loop, explain labeling problem} |
---|
| 938 | |
---|
[3218] | 939 | \subsubsection{Cminor to RTLabs} |
---|
| 940 | |
---|
| 941 | The translation from \textsf{Cminor} to \textsf{RTLabs} is a fairly |
---|
| 942 | routine control flow graph (CFG) construction. As such, we chose to |
---|
[3231] | 943 | axiomatise the associated extensional simulation results. However, we did prove several |
---|
[3218] | 944 | properties of the generated programs: |
---|
| 945 | \begin{itemize} |
---|
| 946 | \item All statements are type correct with respect to the declared |
---|
| 947 | pseudo-register type environment. |
---|
| 948 | \item The CFG is closed, and has a distinguished entry node and a |
---|
| 949 | unique exit node. |
---|
| 950 | \end{itemize} |
---|
| 951 | |
---|
| 952 | These properties rely on similar properties about type safety and the |
---|
[3231] | 953 | presence of \lstinline[language=C]'goto'-labels for \textsf{Cminor} programs |
---|
[3218] | 954 | which are checked at the preceding stage. As a result, this |
---|
| 955 | transformation is total and any compilation failures must occur when |
---|
| 956 | the corresponding \textsf{Clight} source is available and a better |
---|
| 957 | error message can be generated. |
---|
| 958 | |
---|
| 959 | The proof obligations for these properties include many instances of |
---|
| 960 | graph inclusion. We automated these proofs using a small amount of |
---|
| 961 | reflection, making the obligations much easier to handle. One |
---|
[3231] | 962 | drawback to enforcing invariants throughout is that temporarily |
---|
[3218] | 963 | breaking them can be awkward. For example, \lstinline'return' |
---|
| 964 | statements were originally used as placeholders for |
---|
| 965 | \lstinline[language=C]'goto' destinations that had not yet been |
---|
| 966 | translated. However, this made establishing the single exit node |
---|
| 967 | property rather difficult, and a different placeholder was chosen |
---|
| 968 | instead. In other circumstances it is possible to prove a more |
---|
| 969 | complex invariant then simplify it at the end of the transformation. |
---|
| 970 | |
---|
[3142] | 971 | \section{Checking cost labelling properties} |
---|
[3181] | 972 | \label{sec:costchecks} |
---|
[3142] | 973 | |
---|
[3159] | 974 | Ideally, we would provide proofs that the cost labelling pass always |
---|
[3216] | 975 | produces programs that are soundly and precisely labelled and that |
---|
[3159] | 976 | each subsequent pass preserves these properties. This would match our |
---|
| 977 | use of dependent types to eliminate impossible sources of errors |
---|
| 978 | during compilation, in particular retaining intermediate language type |
---|
| 979 | information. |
---|
[3142] | 980 | |
---|
[3159] | 981 | However, given the limited amount of time available we realised that |
---|
| 982 | implementing a compile-time check for a sound and precise labelling of |
---|
| 983 | the \textsf{RTLabs} intermediate code would reduce the proof burden |
---|
| 984 | considerably. This is similar in spirit to the use of translation |
---|
[3212] | 985 | validation in certified compilation, which makes a similar trade-off |
---|
| 986 | between the potential for compile-time failure and the volume of proof |
---|
| 987 | required. |
---|
[3159] | 988 | |
---|
| 989 | The check cannot be pushed into a later stage of the compiler because |
---|
| 990 | much of the information is embedded into the structured traces. |
---|
| 991 | However, if an alternative method was used to show that function |
---|
| 992 | returns in the compiled code are sufficiently well-behaved, then we |
---|
| 993 | could consider pushing the cost property checks into the timing |
---|
| 994 | analysis itself. We leave this as a possible area for future work. |
---|
| 995 | |
---|
| 996 | \subsection{Implementation and correctness} |
---|
[3231] | 997 | \label{sec:costchecksimpl} |
---|
[3159] | 998 | |
---|
| 999 | For a cost labelling to be sound and precise we need a cost label at |
---|
[3173] | 1000 | the start of each function, after each branch and at least one in |
---|
[3159] | 1001 | every loop. The first two parts are trivial to check by examining the |
---|
| 1002 | code. In \textsf{RTLabs} the last part is specified by saying |
---|
| 1003 | that there is a bound on the number of successive instruction nodes in |
---|
| 1004 | the CFG that you can follow before you encounter a cost label, and |
---|
| 1005 | checking this is more difficult. |
---|
| 1006 | |
---|
[3216] | 1007 | The implementation progresses through the set of nodes in the graph, |
---|
[3159] | 1008 | following successors until a cost label is found or a label-free cycle |
---|
[3231] | 1009 | is discovered (in which case the property does not hold and we return |
---|
| 1010 | an error). This is made easier by the prior knowledge that every |
---|
| 1011 | successor of a branch instruction is a cost label, so we do not need |
---|
| 1012 | to search each branch. When a label is found, we remove the chain of |
---|
| 1013 | program counters from the set and continue from another node in the |
---|
| 1014 | set until it is empty, at which point we know that there is a bound |
---|
| 1015 | for every node in the graph. |
---|
[3159] | 1016 | |
---|
[3231] | 1017 | Directly reasoning about the function that implements this procedure would be |
---|
[3159] | 1018 | rather awkward, so an inductive specification of a single step of its |
---|
| 1019 | behaviour was written and proved to match the implementation. This |
---|
| 1020 | was then used to prove the implementation sound and complete. |
---|
| 1021 | |
---|
[3216] | 1022 | While we have not attempted to prove that the cost labelled properties |
---|
[3159] | 1023 | are established and preserved earlier in the compiler, we expect that |
---|
[3216] | 1024 | the effort for the \textsf{Cminor} to \textsf{RTLabs} stage alone |
---|
| 1025 | would be similar to the work outlined above, because it involves the |
---|
| 1026 | change from requiring a cost label at particular positions to |
---|
| 1027 | requiring cost labels to break loops in the CFG. As there are another |
---|
| 1028 | three passes to consider (including the labelling itself), we believe |
---|
| 1029 | that using the check above is much simpler overall. |
---|
[3159] | 1030 | |
---|
[3167] | 1031 | % TODO? Found some Clight to Cminor bugs quite quickly |
---|
| 1032 | |
---|
[3128] | 1033 | \section{Existence of a structured trace} |
---|
[3158] | 1034 | \label{sec:structuredtrace} |
---|
[3128] | 1035 | |
---|
[3231] | 1036 | The \emph{structured trace} idea introduced in |
---|
| 1037 | Section~\ref{sec:fegoals} enriches the execution trace of a program by |
---|
| 1038 | nesting function calls in a mixed-step style and embedding the cost |
---|
| 1039 | labelling properties of the program. See Figure~\ref{fig:strtrace} on |
---|
| 1040 | page~\pageref{fig:strtrace} for an illustration of a structured trace. |
---|
| 1041 | It was originally designed to support the proof of correctness for the |
---|
| 1042 | timing analysis of the object code in the back-end, then generalised |
---|
| 1043 | to provide a common structure to use from the end of the front-end to |
---|
| 1044 | the object code. |
---|
[3159] | 1045 | |
---|
[3167] | 1046 | To make the definition generic we abstract over the semantics of the |
---|
| 1047 | language, |
---|
| 1048 | \begin{lstlisting}[language=matita] |
---|
| 1049 | record abstract_status : Type[1] := |
---|
| 1050 | { as_status :> Type[0] |
---|
| 1051 | ; as_execute : relation as_status |
---|
| 1052 | ; as_pc : DeqSet |
---|
| 1053 | ; as_pc_of : as_status $\rightarrow$ as_pc |
---|
| 1054 | ; as_classify : as_status $\rightarrow$ status_class |
---|
| 1055 | ; as_label_of_pc : as_pc $\rightarrow$ option costlabel |
---|
| 1056 | ; as_after_return : ($\Sigma$s:as_status. as_classify s = cl_call) $\rightarrow$ as_status $\rightarrow$ Prop |
---|
| 1057 | ; as_result: as_status $\rightarrow$ option int |
---|
| 1058 | ; as_call_ident : ($\Sigma$s:as_status.as_classify s = cl_call) $\rightarrow$ ident |
---|
| 1059 | ; as_tailcall_ident : ($\Sigma$s:as_status.as_classify s = cl_tailcall) $\rightarrow$ ident |
---|
| 1060 | }. |
---|
| 1061 | \end{lstlisting} |
---|
[3231] | 1062 | which requires a type of states, an execution relation\footnote{All of |
---|
[3216] | 1063 | our semantics are executable, but using a relation was simpler in |
---|
[3231] | 1064 | the abstraction.}, some notion of abstract |
---|
| 1065 | program counter with decidable equality, the classification of states, |
---|
[3167] | 1066 | and functions to extract the observable intensional information (cost |
---|
[3173] | 1067 | labels and the identity of functions that are called). The |
---|
| 1068 | \lstinline'as_after_return' property links the state before a function |
---|
| 1069 | call with the state after return, providing the evidence that |
---|
| 1070 | execution returns to the correct place. The precise form varies |
---|
| 1071 | between stages; in \textsf{RTLabs} it insists the CFG, the pointer to |
---|
| 1072 | the CFG node to execute next, and some call stack information is |
---|
| 1073 | preserved. |
---|
[3159] | 1074 | |
---|
[3167] | 1075 | The structured traces are defined using three mutually inductive |
---|
| 1076 | types. The core data structure is \lstinline'trace_any_label', which |
---|
[3216] | 1077 | captures some straight-line execution until the next cost label or the |
---|
| 1078 | return from the enclosing function. Any function calls are embedded as |
---|
| 1079 | a single step, with its own trace nested inside and the before and |
---|
| 1080 | after states linked by \lstinline'as_after_return'; and states |
---|
| 1081 | classified as a `jump' (in particular branches) must be followed by a |
---|
| 1082 | cost label. |
---|
[3159] | 1083 | |
---|
[3167] | 1084 | The second type, \lstinline'trace_label_label', is a |
---|
| 1085 | \lstinline'trace_any_label' where the initial state is cost labelled. |
---|
| 1086 | Thus a trace in this type identifies a series of steps whose cost is |
---|
| 1087 | entirely accounted for by the label at the start. |
---|
| 1088 | |
---|
| 1089 | Finally, \lstinline'trace_label_return' is a sequence of |
---|
| 1090 | \lstinline'trace_label_label' values which end in the return from the |
---|
| 1091 | function. These correspond to a measurable subtrace, and in |
---|
[3173] | 1092 | particular include executions of an entire function call (and so are |
---|
| 1093 | used for the nested calls in \lstinline'trace_any_label'). |
---|
[3167] | 1094 | |
---|
[3173] | 1095 | \subsection{Construction} |
---|
| 1096 | |
---|
[3203] | 1097 | The construction of the structured trace replaces syntactic cost |
---|
[3216] | 1098 | labelling properties, which place requirements on where labels appear |
---|
[3231] | 1099 | in the program, with semantic properties that constrain the execution |
---|
[3203] | 1100 | traces of the program. The construction begins by defining versions |
---|
[3216] | 1101 | of the sound and precise labelling properties on states and global |
---|
| 1102 | environments (for the code that appears in each of them) rather than |
---|
| 1103 | whole programs, and showing that these are preserved by steps of the |
---|
| 1104 | \textsf{RTLabs} semantics. |
---|
[3203] | 1105 | |
---|
[3231] | 1106 | Then we show that each cost labelling property required by the |
---|
| 1107 | definition of structured traces is locally satisfied. These proofs are |
---|
| 1108 | broken up by the classification of states. Similarly, we prove a |
---|
| 1109 | step-by-step stack preservation result, which states that the |
---|
| 1110 | \textsf{RTLabs} semantics never changes the lower parts of the stack. |
---|
[3203] | 1111 | |
---|
| 1112 | The core part of the construction of a structured trace is to use the |
---|
| 1113 | proof of termination from the measurable trace (defined on |
---|
[3173] | 1114 | page~\pageref{prog:terminationproof}) to `fold up' the execution into |
---|
[3203] | 1115 | the nested form. The results outlined above fill in the proof |
---|
| 1116 | obligations for the cost labelling properties and the stack |
---|
| 1117 | preservation result shows that calls return to the correct location. |
---|
[3173] | 1118 | |
---|
[3203] | 1119 | The structured trace alone is not sufficient to capture the property |
---|
| 1120 | that the program is soundly labelled. While the structured trace |
---|
| 1121 | guarantees termination, it still permits a loop to be executed a |
---|
| 1122 | finite number of times without encountering a cost label. We |
---|
| 1123 | eliminate this by proving that no `program counter' repeats within any |
---|
| 1124 | \lstinline'trace_any_label' section by showing that it is incompatible |
---|
| 1125 | with the property that there is a bound on the number of successor |
---|
| 1126 | instructions you can follow in the CFG before you encounter a cost |
---|
[3231] | 1127 | label (from Section~\ref{sec:costchecksimpl}). |
---|
[3142] | 1128 | |
---|
[3216] | 1129 | \subsubsection{Complete execution structured traces} |
---|
[3203] | 1130 | |
---|
| 1131 | The development of the construction above started relatively early, |
---|
[3216] | 1132 | before the measurable subtrace preservation proofs. To be confident |
---|
| 1133 | that the traces were well-formed at that time, we also developed a |
---|
| 1134 | complete execution form that embeds the traces above. This includes |
---|
| 1135 | non-terminating program executions, where an infinite number of the terminating |
---|
| 1136 | structured traces are embedded. This construction confirmed that our |
---|
| 1137 | definition of structured traces was consistent, although we later |
---|
| 1138 | found that we did not require the whole execution version for the |
---|
| 1139 | compiler correctness results. |
---|
[3203] | 1140 | |
---|
| 1141 | To construct these we need to know whether each function call will |
---|
| 1142 | eventually terminate, requiring the use of the excluded middle. This |
---|
| 1143 | classical reasoning is local to the construction of whole program |
---|
| 1144 | traces and is not necessary for our main results. |
---|
| 1145 | |
---|
[3128] | 1146 | \section{Conclusion} |
---|
| 1147 | |
---|
[3212] | 1148 | In combination with the work on the CerCo back-end and by |
---|
| 1149 | concentrating on the novel intensional parts of the proof, we have |
---|
| 1150 | shown that it is possible to construct certifying compilers that |
---|
[3216] | 1151 | correctly report execution time and stack space costs. The layering |
---|
| 1152 | of intensional correctness proofs on top of normal simulation results |
---|
| 1153 | provides a useful separation of concerns, and could permit the reuse |
---|
| 1154 | of existing results. |
---|
[3128] | 1155 | |
---|
[3226] | 1156 | \appendix |
---|
[3216] | 1157 | |
---|
[3226] | 1158 | \section{Files} |
---|
[3216] | 1159 | |
---|
[3226] | 1160 | The following table gives a high-level overview of the \matita{} |
---|
| 1161 | source files in Deliverable 3.4: |
---|
[3142] | 1162 | |
---|
[3226] | 1163 | \bigskip |
---|
| 1164 | |
---|
| 1165 | \begin{tabular}{rp{.7\linewidth}} |
---|
| 1166 | \lstinline'compiler.ma' & Top-level compiler definitions, in particular |
---|
| 1167 | \lstinline'front_end', and the whole compiler definition |
---|
| 1168 | \lstinline'compile'. \\ |
---|
| 1169 | \lstinline'correctness.ma' & Correctness results: \lstinline'front_end_correct' |
---|
| 1170 | and \lstinline'correct', respectively. \\ |
---|
| 1171 | \lstinline'Clight/*' & \textsf{Clight}: proofs for switch |
---|
| 1172 | removal, cost labelling, cast simplification and conversion to |
---|
| 1173 | \textsf{Cminor}. \\ |
---|
| 1174 | \lstinline'Cminor/*' & \textsf{Cminor}: axioms of conversion to |
---|
| 1175 | \textsf{RTLabs}. \\ |
---|
| 1176 | \lstinline'RTLabs/*' & \textsf{RTLabs}: definitions and proofs for |
---|
| 1177 | compile-time cost labelling checks, construction of structured traces. |
---|
| 1178 | \\ |
---|
| 1179 | \lstinline'common/Measurable.ma' & Definitions for measurable |
---|
| 1180 | subtraces. \\ |
---|
| 1181 | \lstinline'common/FEMeasurable.ma' & Generic measurable subtrace |
---|
| 1182 | lifting proof. \\ |
---|
| 1183 | \lstinline'common/*' & Other common definitions relevant to many parts |
---|
| 1184 | of the compiler and proof. \\ |
---|
| 1185 | \lstinline'utilities/*' & General purpose definitions used throughout, |
---|
| 1186 | including extensions to the standard \matita{} library. |
---|
| 1187 | \end{tabular} |
---|
| 1188 | |
---|
[3128] | 1189 | \bibliographystyle{plain} |
---|
| 1190 | \bibliography{report} |
---|
| 1191 | |
---|
| 1192 | \end{document} |
---|