Changeset 1746
 Timestamp:
 Feb 24, 2012, 4:09:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1745 r1746 80 80 \item syntactic proofs about the cost labelling. 81 81 \end{enumerate} 82 The first will support both function correctness and allow us to show83 the totality of some of the compiler stages (that is, th ese stages of82 The first will support both functional correctness and allow us to show 83 the totality of some of the compiler stages (that is, those stages of 84 84 the compiler cannot fail). The second provides the main functional 85 85 correctness result, and the last will be crucial for applying … … 88 88 We will also prove that a suitably labelled RTLabs trace can be turned 89 89 into a \emph{structured trace} which splits the execution trace into 90 costlabel tocostlabel chunks with nested function calls. This90 costlabel to costlabel chunks with nested function calls. This 91 91 structure was identified during work on the correctness of the 92 92 backend cost analysis as retaining important information about the … … 94 94 the compiler. 95 95 96 \subsection{Clight Cast removal} 97 98 This removes some casts inserted by the parser to make arithmetic 99 promotion explicit when they are superfluous (such as 100 \lstinline[language=C]'c = (short)((int)a + (int)b);'). 101 102 The transformation only affects Clight expressions, recursively 103 detecting casts that can be safely eliminated. The semantics provides 104 a bigstep definition for expression, so we should be able to show a 105 lockstep forward simulation using a lemma showing that cast 106 elimination does not change the evaluation of expressions. This lemma 107 will follow from a structural induction on the source expression. We 108 have already proved a few of the underlying arithmetic results 109 necessary to validate the approach. 96 \subsection{Clight cast removal} 97 98 This transformation removes some casts inserted by the parser to make 99 arithmetic promotion explicit but which are superfluous (such as 100 \lstinline[language=C]'c = (short)((int)a + (int)b);' where 101 \lstinline'a' and \lstinline'b' are \lstinline[language=C]'short'). 102 This is necessary for producing good code for our target architecture. 103 104 It only affects Clight expressions, recursively detecting casts that 105 can be safely eliminated. The semantics provides a bigstep 106 definition for expression, so we should be able to show a lockstep 107 forward simulation between otherwise identical states using a lemma 108 showing that cast elimination does not change the evaluation of 109 expressions. This lemma will follow from a structural induction on 110 the source expression. We have already proved a few of the underlying 111 arithmetic results necessary to validate the approach. 110 112 111 113 \subsection{Clight cost labelling} … … 113 115 This adds cost labels before and after selected statements and 114 116 expressions, and the execution traces ought to be equivalent modulo 115 cost labels. Hence it requires a simple forward simulation with a 116 limited amount of stuttering whereever a new cost label is introduced. 117 A bound can be given for the amount of stuttering allowed can be given 117 the new cost labels. Hence it requires a simple forward simulation 118 with a limited amount of stuttering whereever a new cost label is 119 introduced. A bound can be given for the amount of stuttering allowed 118 120 based on the statement or continuation to be evaluated next. 119 121 120 122 We also intend to show three syntactic properties about the cost 121 123 labelling: 122 \begin{ itemize}124 \begin{enumerate} 123 125 \item every function starts with a cost label, 124 \item every branching instruction is followed by a label (note that126 \item every branching instruction is followed by a cost label (note that 125 127 exiting a loop is treated as a branch), and 126 128 \item the head of every loop (and any \lstinline'goto' destination) is 127 129 a cost label. 128 \end{ itemize}130 \end{enumerate} 129 131 These can be shown by structural induction on the source term. 130 132 … … 143 145 \item that variables used in the generated code are present in the 144 146 resulting environment (either by checking their presence in the 145 source environment, or from a list of freshly temporary variables);147 source environment, or from a list of freshly generated temporary variables); 146 148 and 147 149 \item that all \lstinline[language=C]'goto' labels are present (by … … 152 154 The simulation will be similar to the relevant stages of CompCert 153 155 (Clight to Csharpminor and Csharpminor to Cminor  in the event that 154 the direct proof is unwieldy we could introduce a corresponding155 intermediate language). During early experimentation with porting 156 CompCert definitions to the Matita proof assistant we found little157 difficulty reproving the results for the memory model, so we plan to158 port the memory injection properties and use them to relate Clight 159 inmemory variables with either a local variable valuation or a stack 160 s lot, depending on how it was classified.156 the direct proof is unwieldy we could introduce an intermediate 157 language corresponding to Csharpminor). During early experimentation 158 with porting CompCert definitions to the Matita proof assistant we 159 found little difficulty reproving the results for the memory model, so 160 we plan to port the memory injection properties and use them to relate 161 Clight inmemory variables with either the value of the local variable or a 162 stack slot, depending on how it was classified. 161 163 162 164 This should be sufficient to show the equivalence of (bigstep) … … 190 192 191 193 We already enforce several invariants with dependent types: some type 192 safety is enforced mostlyusing the type information from Cminor; and194 safety, mostly shown using the type information from Cminor; and 193 195 that the graph is closed (by showing that each successor was recently 194 196 added, or corresponds to a \lstinline[language=C]'goto' label which … … 199 201 later stages using the same method as Cminor. 200 202 201 The simulation will relate Cminor states to RTLabs states about to202 execute the co rresponding code (with a corresponding continuation).203 The simulation will relate Cminor states to RTLabs states which are about to 204 execute the code corresponding to the Cminor statement or continuation. 203 205 Each Cminor statement becomes zero or more RTLabs statements, with a 204 206 decreasing measure based on the statement and continuations similar to … … 209 211 The first two labelling properties remain as before; we will show that 210 212 cost labels are preserved, so the function entry point will be a cost 211 label, and successors t hat are cost labels map still map to cost212 labels, preserving the condition on branches. We replace the property 213 for loops with the notion that we will always reach a cost label or 214 the end of the function by following a bounded number of successors. 215 This can be easily seen in Cminor using the requirement for cost216 labels at the head of loops and after gotos. It remains to show that 217 this is preserved by the translation to RTLabs. % how?213 label, and successors to any statement that are cost labels map still 214 map to cost labels, preserving the condition on branches. We replace 215 the property for loops with the notion that we will always reach a 216 cost label or the end of the function after following a bounded number of 217 successors. This can be easily seen in Cminor using the requirement 218 for cost labels at the head of loops and after gotos. It remains to 219 show that this is preserved by the translation to RTLabs. % how? 218 220 219 221 \subsection{RTLabs structured trace generation} … … 222 224 labelling properties into the execution trace. As the function calls 223 225 are nested within the trace, we need to distinguish between 224 terminating and nonterminating function calls. 225 226 Thus we use the excluded middle (specialised to a function termination 227 property) to do this. Terminating functions are built by following 228 the trace, breaking it into chunks between cost labels and recursively 229 processing function calls. The main difficulties here are the 230 nonstructurally recursive nature of the function (instead we use the 231 size of the termination proof as a measure) and using the properties 232 on RTLabs cost labelling to create the correct structure. We also 233 show that the lower stack frames are preserved during function calls 234 in order to prove that after returning from a function call we execute 235 the correct code. This part of the work has already been constructed, 236 but still requires a simple proof to show that flattening the structured 226 terminating and nonterminating function calls. Thus we use the 227 excluded middle (specialised to a function termination property) to do 228 this. 229 230 Structured traces for terminating functions are built by following the 231 flat trace, breaking it into chunks between cost labels and 232 recursively processing function calls. The main difficulties here are 233 the nonstructurally recursive nature of the function (instead we use 234 the size of the termination proof as a measure) and using the RTLabs 235 cost labelling properties to show that the constraints of the 236 structured traces are observed. We also show that the lower stack 237 frames are preserved during function calls in order to prove that 238 after returning from a function call we resume execution of the 239 correct code. This part of the work has already been constructed, but 240 still requires a simple proof to show that flattening the structured 237 241 trace recreates the original flat trace. 238 242 239 The nonterminating case uses the excluded middle to decide whether to 240 use the function described above to construct an inductive terminating 241 structured trace, or a coinductive version for nontermination. It 242 follows the trace like the terminating version to build up chunks of 243 trace from costlabel to costlabel (which, by the finite distance to 244 a cost label property shown before, can be represented by an inductive 245 type), unless it encounters a nonterminating function in which case 246 it corecursively processes that. This part of the trace 247 transformation is currently under construction, and will also need a 248 flattening result to show that it is correct. 243 The nonterminating case follows the trace like the terminating 244 version to build up chunks of trace from costlabel to costlabel 245 (which, by the finite distance to a cost label property shown before, 246 can be represented by an inductive type). These chunks are chained 247 together in a coinductive data structure that can represent 248 nonterminating traces. The excluded middle is used to decide whether 249 function calls terminate, in which case the function described above 250 constructs an inductive terminating structured trace which is nested 251 in the caller's trace. Otherwise, another coinductive constructor is 252 used to embed the nonterminating trace of the callee, generated by 253 corecursion. This part of the trace transformation is currently under 254 construction, and will also need a flattening result to show that it 255 is correct. 256 249 257 250 258 \section{Backend: RTLabs to machine code}
Note: See TracChangeset
for help on using the changeset viewer.