source: Deliverables/D3.4/Report/report.tex @ 3167

Last change on this file since 3167 was 3167, checked in by campbell, 6 years ago

A little bit about structured traces.

File size: 30.5 KB
RevLine 
[3128]1\documentclass[11pt,epsf,a4wide]{article}
2\usepackage[mathletters]{ucs}
3\usepackage[utf8x]{inputenc}
4\usepackage{listings}
5\usepackage{../../style/cerco}
6\newcommand{\ocaml}{OCaml}
7\newcommand{\clight}{Clight}
8\newcommand{\matita}{Matita}
9\newcommand{\sdcc}{\texttt{sdcc}}
10
11\newcommand{\textSigma}{\ensuremath{\Sigma}}
12
13% LaTeX Companion, p 74
14\newcommand{\todo}[1]{\marginpar{\raggedright - #1}}
15
16\lstdefinelanguage{coq}
17  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
18   morekeywords={[2]if,then,else},
19  }
20
21\lstdefinelanguage{matita}
22  {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on},
23   morekeywords={[2]whd,normalize,elim,cases,destruct},
24   mathescape=true,
25   morecomment=[n]{(*}{*)},
26  }
27
28\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
31        commentstyle=\color{green},
32        stringstyle=\color{blue},
33        showspaces=false,showstringspaces=false}
34
35\lstset{extendedchars=false}
36\lstset{inputencoding=utf8x}
37\DeclareUnicodeCharacter{8797}{:=}
38\DeclareUnicodeCharacter{10746}{++}
39\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
40\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
41
42
43\title{
44INFORMATION AND COMMUNICATION TECHNOLOGIES\\
45(ICT)\\
46PROGRAMME\\
47\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
48
49\date{ }
50\author{}
51
52\begin{document}
53\thispagestyle{empty}
54
55\vspace*{-1cm}
56\begin{center}
57\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
58\end{center}
59
60\begin{minipage}{\textwidth}
61\maketitle
62\end{minipage}
63
64
65\vspace*{0.5cm}
66\begin{center}
67\begin{LARGE}
68\bf
69Report n. D3.4\\
70Front-end Correctness Proofs\\
71\end{LARGE} 
72\end{center}
73
74\vspace*{2cm}
75\begin{center}
76\begin{large}
77Version 1.0
78\end{large}
79\end{center}
80
81\vspace*{0.5cm}
82\begin{center}
83\begin{large}
84Authors:\\
85Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark
86\end{large}
87\end{center}
88
89\vspace*{\fill}
90\noindent
91Project Acronym: \cerco{}\\
92Project full title: Certified Complexity\\
93Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
94
95\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
96
97\newpage
98
99\vspace*{7cm}
100\paragraph{Abstract}
101We report on the correctness proofs for the front-end of the \cerco{} cost
102lifting compiler, considering three distinct parts of the task: showing that
103the \emph{annotated source code} output by the compiler has equivalent
104behaviour to the original input (up to the annotations); showing that a
105\emph{measurable} subtrace of the annotated source code corresponds to an
106equivalent measurable subtrace in the code produced by the front-end, including
107costs; and finally showing that the enriched \emph{structured} execution traces
108required for cost correctness in the back-end can be constructed from the
109properties of the code produced by the front-end.
110
111A key part of our work is that the intensional correctness results that show
112that we get consistent cost measurements throughout the intermediate languages
113of the compiler can be layered on top of normal forward simulation results,
114if we split them into local call-structure preserving results.
115
116This deliverable shows correctness results about the formalised compiler
117described in D3.2, using the source language semantics from D3.1 and
118intermediate language semantics from D3.3.  Together with the companion
119deliverable about the correctness of the back-end, D4.4, we obtain results
120about the whole formalised compiler.
121
122% TODO: mention the deliverable about the extracted compiler et al?
123
124\newpage 
125
126\tableofcontents
127
128% CHECK: clear up any -ize vs -ise
129% CHECK: clear up any "front end" vs "front-end"
130% CHECK: clear up any mentions of languages that aren't textsf'd.
131% CHECK: fix unicode in listings
132
133\section{Introduction}
134
[3142]135\todo{add stack space for more precise statement.  Also do some
136translation validation on sound, precise labelling properties.}
[3128]137
138The \cerco{} compiler compiles C code targeting microcontrollers implementing
139the Intel 8051 architecture, which produces both the object code and source
140code containing annotations describing the timing behavior of the object code.
141There are two versions: first, an initial prototype implemented in
142\ocaml{}~\cite{d2.2}, and a version formalised in the \matita{} proof
143assistant~\cite{d3.2,d4.2} and then extracted to \ocaml{} code to produce an
144executable compiler.  In this document we present results formalised in
145\matita{} about the front-end of that version of the compiler, and how that fits
146into the verification of the whole compiler.
147
[3142]148\todo{maybe mention stack space here?  other additions?  refer to "layering"?}
[3128]149A key part of this work was to separate the proofs about the compiled code's
150extensional behaviour (that is, the functional correctness of the compiler)
151from the intensional correctness that the costs given are correct.
152Unfortunately, the ambitious goal of completely verifying the compiler was not
153feasible within the time available, but thanks to this separation of extensional
154and intensional proofs we are able to axiomatize simulation results similar to
155those in other compiler verification projects and concentrate on the novel
156intensional proofs.  The proofs were also made more tractable by introducing
157compile-time checks for the `sound and precise' cost labelling properties
158rather than proving that they are preserved throughout.
159
160The overall statement of correctness says that the annotated program has the
161same behaviour as the input, and that for any suitably well-structured part of
162the execution (which we call \emph{measurable}), the object code will execute
163the same behaviour taking precisely the time given by the cost annotations in
164the annotated source program.
165
166In the next section we recall the structure of the compiler and make the overall
167statement more precise.  Following that, in Section~\ref{sec:fegoals} we
168describe the statements we need to prove about the intermediate \textsf{RTLabs}
[3142]169programs sufficient for the back-end proofs.  \todo{rest of document structure}
[3128]170
171\section{The compiler and main goals}
172
173TODO: outline compiler, maybe figure from talk, maybe something like the figure
174below.
175
176TODO: might want a version of this figure
177\begin{figure}
178\begin{center}
179\begin{minipage}{.8\linewidth}
180\begin{tabbing}
181\quad \= $\downarrow$ \quad \= \kill
182\textsf{C} (unformalized)\\
183\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
184\textsf{Clight}\\
[3142]185%\> $\downarrow$ \> add runtime functions\\
186\> $\downarrow$ \> \lstinline[language=C]'switch' removal\\
187\> $\downarrow$ \> labelling\\
[3128]188\> $\downarrow$ \> cast removal\\
189\> $\downarrow$ \> stack variable allocation and control structure
190 simplification\\
191\textsf{Cminor}\\
[3142]192%\> $\downarrow$ \> generate global variable initialization code\\
[3128]193\> $\downarrow$ \> transform to RTL graph\\
194\textsf{RTLabs}\\
[3142]195\> $\downarrow$ \> check cost labelled properties of RTL graph\\
[3128]196\> $\downarrow$ \> start of target specific back-end\\
197\>\quad \vdots
198\end{tabbing}
199\end{minipage}
200\end{center}
[3142]201\caption{Front-end languages and compiler passes}
[3128]202\label{fig:summary}
203\end{figure}
204
205The compiler function returns the following record on success:
206\begin{lstlisting}[language=matita]
207record compiler_output : Type[0] :=
208 { c_labelled_object_code: labelled_object_code
209 ; c_stack_cost: stack_cost_model
210 ; c_max_stack: nat
211 ; c_init_costlabel: costlabel
212 ; c_labelled_clight: clight_program
213 ; c_clight_cost_map: clight_cost_map
214 }.
215\end{lstlisting}
216It consists of annotated 8051 object code, a mapping from function
217identifiers to the function's stack space usage\footnote{The compiled
218  code's only stack usage is to allocate a fixed-size frame on each
219  function entry and discard it on exit.}, a cost label covering the
220initialisation of global variables and calling the
221\lstinline[language=C]'main' function, the annotated source code, and
222finally a mapping from cost labels to actual execution time costs.
223
224An \ocaml{} pretty printer is used to provide a concrete version of the output
225code.  In the case of the annotated source code, it also inserts the actual
226costs alongside the cost labels, and optionally adds a global cost variable
227and instrumentation to support further reasoning.  \todo{Cross-ref case study
228deliverables}
229
230\subsection{Revisions to the prototype compiler}
231
[3142]232TODO: could be a good idea to have this again; stack space,
233initialisation, cost checks, had we dropped cminor loops in previous
234writing?, check mailing list in case I've forgotten something
[3128]235
[3159]236TODO: continued use of dep types to reduce partiality
237
[3128]238\subsection{Main goals}
239
240TODO: need an example for this
241
242Informally, our main intensional result links the time difference in a source
243code execution to the time difference in the object code, expressing the time
244for the source by summing the values for the cost labels in the trace, and the
245time for the target by a clock built in to the 8051 executable semantics.
246
247The availability of precise timing information for 8501
248implementations and the design of the compiler allow it to give exact
249time costs in terms of processor cycles.  However, these exact results
250are only available if the subtrace we measure starts and ends at
251suitable points.  In particular, pure computation with no observable
252effects may be reordered and moved past cost labels, so we cannot
253measure time between arbitrary statements in the program.
254
255There is also a constraint on the subtraces that we
256measure due to the requirements of the correctness proof for the
257object code timing analysis.  To be sure that the timings are assigned
258to the correct cost label, we need to know that each return from a
259function call must go to the correct return address.  It is difficult
260to observe this property locally in the object code because it relies
261on much earlier stages in the compiler.  To convey this information to
262the timing analysis extra structure is imposed on the subtraces, which
263we will give more details on in Section~\ref{sec:fegoals}.
264
265% Regarding the footnote, would there even be much point?
266These restrictions are reflected in the subtraces that we give timing
267guarantees on; they must start at a cost label and end at the return
268of the enclosing function of the cost label\footnote{We expect that
269  this would generalise to subtraces between cost labels in the same
270  function, but could not justify the extra complexity that would be
271  required to show this.}.  A typical example of such a subtrace is
272the execution of an entire function from the cost label at the start
273of the function until it returns.  We call such any such subtrace
274\emph{measurable} if it (and the prefix of the trace before it) can
275also be executed within the available stack space.
276
277Now we can give the main intensional statement for the compiler.
278Given a \emph{measurable} subtrace for a labelled \textsf{Clight}
279program, there is a subtrace of the 8051 object code program where the
280time differences match.  Moreover, \emph{observable} parts of the
281trace also match --- these are the appearance of cost labels and
282function calls and returns.
283
284More formally, the definition of this statement in \matita{} is
285\begin{lstlisting}[language=matita]
286definition simulates :=
287  $\lambda$p: compiler_output.
288  let initial_status := initialise_status $\dots$ (cm (c_labelled_object_code $\dots$ p)) in
289  $\forall$m1,m2.
290   measurable Clight_pcs (c_labelled_clight $\dots$ p) m1 m2
291    (lookup_stack_cost (c_stack_cost $\dots$ p)) (c_max_stack $\dots$ p) $\rightarrow$
292  $\forall$c1,c2.
293   clock_after Clight_pcs (c_labelled_clight $\dots$ p) m1 (c_clight_cost_map $\dots$ p) = OK $\dots$ c1 $\rightarrow$
294   clock_after Clight_pcs (c_labelled_clight $\dots$ p) (m1+m2) (c_clight_cost_map $\dots$ p) = OK $\dots$ c2 $\rightarrow$
295  $\exists$n1,n2.
296   observables Clight_pcs (c_labelled_clight $\dots$ p) m1 m2 =
297   observables (OC_preclassified_system (c_labelled_object_code $\dots$ p))
298    (c_labelled_object_code $\dots$ p) n1 n2
299  $\wedge$
300   c2 - c1 = clock $\dots$ (execute n2 ? initial_status) - clock $\dots$ (execute n1 ? initial_status).
301\end{lstlisting}
302where the \lstinline'measurable', \lstinline'clock_after' and
303\lstinline'observables' definitions can be applied to multiple
304languages; in this case the \lstinline'Clight_pcs' record applies them
305to \textsf{Clight} programs.
306
[3131]307There is a second part to the statement, which says that the initial
308processing of the input program to produce the cost labelled version
309does not affect the semantics of the program:
310% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
311\begin{lstlisting}[language=matita]
312  $\forall$input_program,output.
313  compile input_program = return output $\rightarrow$
314  not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
315  sim_with_labels
316   (exec_inf … clight_fullexec input_program)
317   (exec_inf … clight_fullexec (c_labelled_clight … output))
318\end{lstlisting}
319That is, any successful compilation produces a labelled program that
320has identical behaviour to the original, so long as there is no
321`undefined behaviour'.
[3128]322
[3131]323Note that this provides full functional correctness, including
324preservation of (non-)termination.  The intensional result above does
325not do this directly --- it does not guarantee the same result or same
326termination.  There are two mitigating factors, however: first, to
327prove the intensional property you need local simulation results that
328can be pieced together to form full behavioural equivalence, only time
329constraints have prevented us from doing so.  Second, if we wish to
330confirm a result, termination, or non-termination we could add an
331observable witness, such as a function that is only called if the
332correct result is given.  The intensional result guarantees that the
333observable witness is preserved, so the program must behave correctly.
334
[3128]335\section{Intermediate goals for the front-end}
336\label{sec:fegoals}
337
338The essential parts of the intensional proof were outlined during work
339on a toy
340compiler~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}.  These
341are
342\begin{enumerate}
343\item functional correctness, in particular preserving the trace of
344  cost labels,
345\item the \emph{soundness} and \emph{precision} of the cost labelling
346  on the object code, and
347\item the timing analysis on the object code produces a correct
348  mapping from cost labels to time.
349\end{enumerate}
350
351However, that toy development did not include function calls.  For the
352full \cerco{} compiler we also need to maintain the invariant that
353functions return to the correct program location in the caller, as we
354mentioned in the previous section.  During work on the back-end timing
355analysis (describe in more detail in the companion deliverable, D4.4)
356the notion of a \emph{structured trace} was developed to enforce this
357return property, and also most of the cost labelling properties too.
358
359\begin{figure}
360\begin{center}
361\includegraphics[width=0.5\linewidth]{compiler.pdf}
362\end{center}
363\caption{The compiler and proof outline}
364\label{fig:compiler}
365\end{figure}
366
367Jointly, we generalised the structured traces to apply to any of the
368intermediate languages with some idea of program counter.  This means
369that they are introduced part way through the compiler, see
370Figure~\ref{fig:compiler}.  Proving that a structured trace can be
371constructed at \textsf{RTLabs} has several virtues:
372\begin{itemize}
373\item This is the first language where every operation has its own
374  unique, easily addressable, statement.
375\item Function calls and returns are still handled in the language and
376  so the structural properties are ensured by the semantics.
377\item Many of the back-end languages from \textsf{RTL} share a common
378  core set of definitions, and using structured traces throughout
379  increases this uniformity.
380\end{itemize}
381
[3140]382\begin{figure}
383\begin{center}
384\includegraphics[width=0.6\linewidth]{strtraces.pdf}
385\end{center}
386\caption{Nesting of functions in structured traces}
387\label{fig:strtrace}
388\end{figure}
[3128]389A structured trace is a mutually inductive data type which principally
390contains the steps from a normal program trace, but arranged into a
391nested structure which groups entire function calls together and
392aggregates individual steps between cost labels (or between the final
[3140]393cost label and the return from the function), see
394Figure~\ref{fig:strtrace}.  This capture the idea that the cost labels
395only represent costs \emph{within} a function --- calls to other
396functions are accounted for in the trace for their execution, and we
397can locally regard function calls as a single step.
[3128]398
399These structured traces form the core part of the intermediate results
400that we must prove so that the back-end can complete the main
401intensional result stated above.  In full, we provide the back-end
402with
403\begin{enumerate}
404\item A normal trace of the \textbf{prefix} of the program's execution
405  before reaching the measurable subtrace.  (This needs to be
406  preserved so that we know that the stack space consumed is correct.)
407\item The \textbf{structured trace} corresponding to the measurable
408  subtrace.
409\item An additional property about the structured trace that no
[3131]410  `program counter' is \textbf{repeated} between cost labels.  Together with
[3128]411  the structure in the trace, this takes over from showing that
412  cost labelling is sound and precise.
[3131]413\item A proof that the \textbf{observables} have been preserved.
414\item A proof that the \textbf{stack limit} is still observed by the prefix and
[3128]415  the structure trace.  (This is largely a consequence of the
416  preservation of observables.)
417\end{enumerate}
418
419Following the outline in Figure~\ref{fig:compiler}, we will first deal
420with the transformations in \textsf{Clight} that produce the source
421program with cost labels, then show that measurable traces can be
422lifted to \textsf{RTLabs}, and finally that we can construct the
423properties listed above ready for the back-end proofs.
424
425\section{Input code to cost labelled program}
426
[3138]427The simple form of labelling used in the formalised compiler is not
428quite capable of capturing costs arising from complex C
429\lstinline[language=C]'switch' statements, largely due to the
430fall-through behaviour.  Our first pass replaces these statements with
431simpler C code, allowing our second pass to perform the cost
432labelling.  We show that the behaviour of programs is unchanged by
433these passes.
434
435TODO: both give one-step-sim-by-many forward sim results; switch
436removal tricky, uses aux var to keep result of expr, not central to
437intensional correctness so curtailed proof effort once reasonable
438level of confidence in code gained; labelling much simpler; don't care
439what the labels are at this stage, just need to know when to go
440through extra steps.  Rolled up into a single result with a cofixpoint
441to obtain coinductive statement of equivalence (show).
442
[3128]443\section{Finding corresponding measurable subtraces}
444
[3142]445There follow the three main passes of the front-end:
446\begin{enumerate}
447\item simplification of casts in \textsf{Clight} code
448\item \textsf{Clight} to \textsf{Cminor} translation, performing stack
449  variable allocation and simplifying control structures
450\item transformation to \textsf{RTLabs} control flow graph
451\end{enumerate}
[3158]452\todo{I keep mentioning forward sim results - I probably ought to say
453  something about determinancy} We have taken a common approach to
454each pass: first we build (or axiomatise) forward simulation results
455that are similar to normal compiler proofs, but slightly more
456fine-grained so that we can see that the call structure and relative
457placement of cost labels is preserved.
[3142]458
[3158]459Then we instantiate a general result which shows that we can find a
460\emph{measurable} subtrace in the target of the pass that corresponds
461to the measurable subtract in the source.  By repeated application of
462this result we can find a measurable subtrace of the execution of the
463\textsf{RTLabs} code, suitable for the construction of a structured
464trace (see Section~\ref{sec:structuredtrace}.  This is essentially an
465extra layer on top of the simulation proofs that provides us with the
466extra information required for our intensional correctness proof.
[3142]467
468\subsection{Generic measurable subtrace lifting proof}
469
[3158]470Our generic proof is parametrised on a record containing small-step
471semantics for the source and target language, a classification of
472states (the same form of classification is used when defining
473structured traces), a simulation relation which loosely respects the
474classification and cost labelling \todo{this isn't very helpful} and
475four simulation results:
476\begin{enumerate}
477\item a step from a `normal' state (which is not classified as a call
478  or return) which is not a cost label is simulated by zero or more
479  `normal' steps;
480\item a step from a `call' state followed by a cost label step is
481  simulated by a step from a `call' state, a corresponding label step,
482  then zero or more `normal' steps;
483\item a step from a `call' state not followed by a cost label
484  similarly (note that this case cannot occur in a well-labelled
485  program, but we do not have enough information locally to exploit
486  this); and
487\item a cost label step is simulated by a cost label step.
488\end{enumerate}
489Finally, we need to know that a successfully translated program will
490have an initial state in the simulation relation with the original
491program's initial state.
[3142]492
[3158]493\begin{figure}
494\begin{center}
495\includegraphics[width=0.5\linewidth]{meassim.pdf}
496\end{center}
497\caption{Tiling of simulation for a measurable subtrace}
498\label{fig:tiling}
499\end{figure}
500
501To find the measurable subtrace in the target program's execution we
502walk along the original program's execution trace applying the
503appropriate simulation result by induction on the number of steps.
504While the number of steps taken varies, the overall structure is
505preserved, as illustrated in Figure~\ref{fig:tiling}.  By preserving
506the structure we also maintain the same intensional observables.  One
507delicate point is that the cost label following a call must remain
508directly afterwards\footnote{The prototype compiler allowed some
509  straight-line code to appear before the cost label until a later
510  stage of the compiler, but we must move the requirement forward to
511  fit with the structured traces.}
512% Damn it, I should have just moved the cost label forwards in RTLabs,
513% like the prototype does in RTL to ERTL; the result would have been
514% simpler.  Or was there some reason not to do that?
515(both in the program code and in the execution trace), even if we
516introduce extra steps, for example to store parameters in memory in
517\textsf{Cminor}.  Thus we have a version of the call simulation
518that deals with both in one result.
519
520In addition to the subtrace we are interested in measuring we must
521also prove that the earlier part of the trace is also preserved in
522order to use the simulation from the initial state.  It also
523guarantees that we do not run out of stack space before the subtrace
524we are interested in.  The lemmas for this prefix and the measurable
525subtrace are similar, following the pattern above.  However, the
526measurable subtrace also requires us to rebuild the termination
527proof.  This has a recursive form:
528\begin{lstlisting}[language=matita]
529let rec will_return_aux C (depth:nat)
530                             (trace:list (cs_state … C × trace)) on trace : bool :=
531match trace with
532[ nil $\Rightarrow$ false
533| cons h tl $\Rightarrow$
534  let $\langle$s,tr$\rangle$ := h in
535  match cs_classify C s with
536  [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
537  | cl_return $\Rightarrow$
538      match depth with
539      [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
540      | S d $\Rightarrow$ will_return_aux C d tl
541      ]
542  | _ $\Rightarrow$ will_return_aux C depth tl
543  ]
544].
545\end{lstlisting}
546The \lstinline'depth' is the number of return states we need to see
547before we have returned to the original function (initially zero) and
548\lstinline'trace' the measurable subtrace obtained from the running
549the semantics for the correct number of steps.  This definition
550unfolds tail recursively for each step, and once the corresponding
551simulation result has been applied a new one for the target can be
552asserted by unfolding and applying the induction hypothesis on the
553shorter trace.
554
555This then gives us an overall result for any simulation fitting the
556requirements above (contained in the \lstinline'meas_sim' record):
557\begin{lstlisting}[language=matita]
558theorem measured_subtrace_preserved :
559  $\forall$MS:meas_sim.
560  $\forall$p1,p2,m,n,stack_cost,max.
561  ms_compiled MS p1 p2 $\rightarrow$
562  measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$
563  $\exists$m',n'.
564    measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$
565    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
566\end{lstlisting}
567The stack space requirement that is embedded in \lstinline'measurable'
568is a consequence of the preservation of observables.
569
570TODO: how to deal with untidy edges wrt to sim rel; anything to
571say about obs?
572
573TODO: say something about termination measures; cost labels are
574statements/exprs in these languages; split call/return gives simpler
575simulations
576
[3142]577\subsection{Simulation results for each pass}
578
579\todo{don't use loop structures from CompCert, go straight to jumps}
580
581\section{Checking cost labelling properties}
582
[3159]583Ideally, we would provide proofs that the cost labelling pass always
584produced programs that are soundly and precisely labelled and that
585each subsequent pass preserves these properties.  This would match our
586use of dependent types to eliminate impossible sources of errors
587during compilation, in particular retaining intermediate language type
588information.
[3142]589
[3159]590However, given the limited amount of time available we realised that
591implementing a compile-time check for a sound and precise labelling of
592the \textsf{RTLabs} intermediate code would reduce the proof burden
593considerably.  This is similar in spirit to the use of translation
594validation in certified compilation\todo{Cite some suitable work
595  here}, which makes a similar trade-off between the potential for
596compile-time failure and the volume of proof required.
597
598The check cannot be pushed into a later stage of the compiler because
599much of the information is embedded into the structured traces.
600However, if an alternative method was used to show that function
601returns in the compiled code are sufficiently well-behaved, then we
602could consider pushing the cost property checks into the timing
603analysis itself.  We leave this as a possible area for future work.
604
605\subsection{Implementation and correctness}
606
607For a cost labelling to be sound and precise we need a cost label at
608the start of each function, after each branch and at least once in
609every loop.  The first two parts are trivial to check by examining the
610code.  In \textsf{RTLabs} the last part is specified by saying
611that there is a bound on the number of successive instruction nodes in
612the CFG that you can follow before you encounter a cost label, and
613checking this is more difficult.
614
615The implementation works through the set of nodes in the graph,
616following successors until a cost label is found or a label-free cycle
617is discovered (in which case the property does not hold and we stop).
618This is made easier by the prior knowledge that any branch is followed
619by cost labels, so we do not need to search each branch.  When a label
620is found, we remove the chain from the set and continue until it is
621empty, at which point we know that there is a bound for every node in
622the graph.
623
624Directly reasoning about the function that implements this would be
625rather awkward, so an inductive specification of a single step of its
626behaviour was written and proved to match the implementation.  This
627was then used to prove the implementation sound and complete.
628
629While we have not attempted to proof that the cost labelled properties
630are established and preserved earlier in the compiler, we expect that
631the effort for the \textsf{Cminor} to \textsf{RTLabs} would be similar
632to the work outlined above, because it involves the change from
633requiring a cost label at particular positions to requiring cost
634labels to break loops in the CFG.  As there are another three passes
635to consider (including the labelling itself), we believe that using
636the check above is much simpler overall.
637
[3167]638% TODO? Found some Clight to Cminor bugs quite quickly
639
[3128]640\section{Existence of a structured trace}
[3158]641\label{sec:structuredtrace}
[3128]642
[3159]643\emph{Structured traces} enrich the execution trace of a program by
644nesting function calls in a mixed-step style\todo{Can I find a
645  justification for mixed-step} and embedding the cost properties of
646the program.  It was originally designed to support the proof of
647correctness for the timing analysis of the object code in the
648back-end, then generalised to provide a common structure to use from
649the end of the front-end to the object code.  See
650Figure~\ref{fig:strtrace} on page~\pageref{fig:strtrace}
651for an illustration of a structured trace.
652
[3167]653To make the definition generic we abstract over the semantics of the
654language,
655\begin{lstlisting}[language=matita]
656record abstract_status : Type[1] :=
657  { as_status :> Type[0]
658  ; as_execute : relation as_status
659  ; as_pc : DeqSet
660  ; as_pc_of : as_status $\rightarrow$ as_pc
661  ; as_classify : as_status $\rightarrow$ status_class
662  ; as_label_of_pc : as_pc $\rightarrow$ option costlabel
663  ; as_after_return : ($\Sigma$s:as_status. as_classify s =  cl_call) $\rightarrow$ as_status $\rightarrow$ Prop
664  ; as_result: as_status $\rightarrow$ option int
665  ; as_call_ident : ($\Sigma$s:as_status.as_classify s = cl_call) $\rightarrow$ ident
666  ; as_tailcall_ident : ($\Sigma$s:as_status.as_classify s = cl_tailcall) $\rightarrow$ ident
667  }.
668\end{lstlisting}
669which gives a type of states, an execution relation, some notion of
670program counters with decidable equality, the classification of states
671and functions to extract the observable intensional information (cost
672labels and the identity of functions that are called).
[3159]673
[3167]674The structured traces are defined using three mutually inductive
675types.  The core data structure is \lstinline'trace_any_label', which
676captures some straight-line execution until the next cost label or
677function return.  Each function call is embedded as a single step,
678with its own trace nested inside, and states classified as a `jump'
679(in particular branches) must be followed by a cost label.
[3159]680
[3167]681The second type, \lstinline'trace_label_label', is a
682\lstinline'trace_any_label' where the initial state is cost labelled.
683Thus a trace in this type identifies a series of steps whose cost is
684entirely accounted for by the label at the start.
685
686Finally, \lstinline'trace_label_return' is a sequence of
687\lstinline'trace_label_label' values which end in the return from the
688function.  These correspond to a measurable subtrace, and in
689particular include executions of an entire function call.
690
[3142]691TODO: design, basic structure from termination proof, how cost
692labelling props are baked in; unrepeating PCs, remainder of sound
693labellings; coinductive version for whole programs, reason/relevance,
694use of em (maybe a general comment about uses of classical reasoning
695in development)
696
[3128]697\section{Conclusion}
698
699TODO
700
[3142]701TODO: appendix on code layout?
702
[3128]703\bibliographystyle{plain}
704\bibliography{report}
705
706\end{document}
Note: See TracBrowser for help on using the repository browser.