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