Changeset 3214
- Timestamp:
- Apr 29, 2013, 7:17:03 PM (5 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.4/Report/report.tex
r3212 r3214 114 114 properties of the code produced by the front-end. 115 115 116 A key part of our work is that the intensional correctness results thatshow116 A key part of our work is that the intensional correctness results which show 117 117 that we get consistent cost measurements throughout the intermediate languages 118 118 of the compiler can be layered on top of normal forward simulation results, … … 122 122 compiler described in D3.2, using the source language semantics from 123 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 in125 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.124 earlier work on the correctness of a toy compiler built to test the 125 labelling approach in D2.1. Together with the companion deliverable 126 about the correctness of the back-end, D4.4, we obtain results about 127 the whole formalised compiler. 128 128 129 129 % TODO: mention the deliverable about the extracted compiler et al? … … 140 140 \section{Introduction} 141 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. 142 The \cerco{} compiler produces a version of the source code containing 143 annotations describing the timing behaviour of the object code, as well 144 as the object code itself. It compiles C code, targeting 145 microcontrollers implementing the Intel 8051 architecture. There are 146 two versions: first, an initial prototype was implemented in 147 \ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{} proof 148 assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to 149 produce an executable compiler. In this document we present results 150 formalised in \matita{} about the front-end of the latter version of 151 the compiler, and how that fits into the verification of the whole 152 compiler. 152 153 153 154 A key part of this work was to layer the intensional correctness 154 results that show that the costs givenare correct on top of the155 results that show that the costs produced are correct on top of the 155 156 proofs about the compiled code's extensional behaviour (that is, the 156 157 functional correctness of the compiler). Unfortunately, the ambitious 157 158 goal of completely verifying the entire compiler was not feasible 158 159 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 verification160 extensional and intensional proofs we are able to axiomatize some 161 simulation results which are similar to those in other compiler verification 161 162 projects and concentrate on the novel intensional proofs. We were 162 163 also able to add stack space costs to obtain a stronger result. The … … 174 175 statement more precise. Following that, in Section~\ref{sec:fegoals} we 175 176 describe the statements we need to prove about the intermediate \textsf{RTLabs} 176 programs sufficientfor the back-end proofs.177 programs for the back-end proofs. 177 178 Section~\ref{sec:inputtolabelling} covers the passes which produce the 178 179 annotated source program and Section~\ref{sec:measurablelifting} the rest … … 191 192 \begin{figure} 192 193 \begin{center} 193 \includegraphics {compiler-plain.pdf}194 \includegraphics[width=0.5\linewidth]{compiler-plain.pdf} 194 195 \end{center} 195 196 \caption{Languages in the \cerco{} compiler} … … 237 238 statements before labelling --- we need to remove them because the 238 239 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. 240 capable of capturing their execution time costs, largely due to C's 241 `fall-through' behaviour where execution from one branch continues in 242 the next unless there is an explicit \lstinline[language=C]'break'. 241 243 242 244 The cast removal phase which follows cost labelling simplifies 243 expressions to prevent unnecessary arithmetic promotion which is245 expressions to prevent unnecessary arithmetic promotion, which is 244 246 specified by the C standard but costly for an 8-bit target. The 245 247 transformation to \textsf{Cminor} and subsequently \textsf{RTLabs} … … 252 254 The whole compilation function returns the following information on success: 253 255 \begin{lstlisting}[language=matita] 254 record compiler_output : Type[0] :=255 { c_labelled_object_code: labelled_object_code256 ; c_stack_cost: stack_cost_model257 ; c_max_stack: nat258 ; c_init_costlabel: costlabel259 ; c_labelled_clight: clight_program260 ; c_clight_cost_map: clight_cost_map261 }.256 record compiler_output : Type[0] := 257 { c_labelled_object_code: labelled_object_code 258 ; c_stack_cost: stack_cost_model 259 ; c_max_stack: nat 260 ; c_init_costlabel: costlabel 261 ; c_labelled_clight: clight_program 262 ; c_clight_cost_map: clight_cost_map 263 }. 262 264 \end{lstlisting} 263 265 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 266 identifiers to the function's stack space usage, the space available for the 268 267 stack after global variable allocation, a cost label covering the 269 268 execution time for the initialisation of global variables and the call … … 272 271 costs. 273 272 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. 273 An \ocaml{} pretty printer is used to provide a concrete version of 274 the output code and annotated source code. In the case of the 275 annotated source code, it also inserts the actual costs alongside the 276 cost labels, and optionally adds a global cost variable and 277 instrumentation to support further reasoning. 278 278 279 279 \subsection{Revisions to the prototype compiler} … … 285 285 allocation provided by the compiler, so we were able to strengthen the 286 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 287 stack space obeys the \lstinline'c_max_stack' bound calculated by 288 subtracting the global variable requirements from the total memory 289 available. 290 291 The cost labelling checks at the end of Figure~\ref{fig:summary} have been 291 292 introduced to reduce the proof burden, and are described in 292 293 Section~\ref{sec:costchecks}. … … 295 296 invariants makes every front-end pass except \textsf{Clight} to 296 297 \textsf{Cminor} and the cost checks total functions. Hence various 297 well-formedness and type checks are dealt with once in that phase. 298 well-formedness and type safety checks are performed once between 299 \textsf{Clight} and \textsf{Cminor}, and the invariants rule out any 300 difficulties in the later stages. 298 301 With the benefit of hindsight we would have included an initial 299 302 checking phase to produce a `well-formed' variant of \textsf{Clight},
Note: See TracChangeset
for help on using the changeset viewer.