Changeset 3269 for Deliverables/Dissemination/frontend/frontend.tex
 Timestamp:
 May 14, 2013, 5:47:32 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/Dissemination/frontend/frontend.tex
r3267 r3269 26 26 \begin{document} 27 27 28 \title{Frontend Correctness Proofs} 29 \author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark} 28 \title{WP3: Verified Compiler  Front End\\[1\jot] 29 D3.4: FrontEnd Correctness Proofs} 30 \author{Brian~Campbell, Ilias~Garnier, James~McKinna, \underline{Ian~Stark}} 30 31 \institute{LFCS, University of Edinburgh\\[1ex] 31 32 \includegraphics[width=.3\linewidth]{cerco_logo.png}\\ … … 35 36 \maketitle 36 37 37 \frame{ 38 \frametitle{Introduction} 39 40 D3.4 consists of the frontend correctness proofs: 41 42 \begin{description} 43 \item[Primary focus:] novel \red{intensional} properties: \blue{cost 44 bound correctness} 45 \end{description} 46 \vskip2ex 47 \begin{itemize} 48 \item Now have \blue{stack} costs as well as \blue{time}\\ 49  yields stronger overall correctness result 50 \item Informed by earlier formal experiment with a toy compiler. 51 \end{itemize} 52 53 \medskip 54 \begin{description} 55 \item[Secondary focus:] usual \red{extensional} result: \blue{functional correctness} 56 \end{description} 57 \vskip2ex 58 \begin{itemize} 59 \item Similar functional correctness already studied in 60 \blue{CompCert} 61 \item Axiomatize similar results 62 \item \red{Intensional} proofs form a layer on top 63 \end{itemize} 64 } 38 39 \begin{frame}{CerCo Outcomes} 40 41 The final results of the CerCo project include the following: 42 43 \medskip % 44 \begin{itemize} 45 \item A compiler from C to executable 8051 binaries, formalised in Matita as 46 \blue{\lstinlinecompiler.ma} \dots 47 \item \dots which adds labels and cost information to C source code 48 \item \dots with exact values for time and space used by the binary. 49 50 \medskip % 51 \item A machinechecked proof of this in Matita 52 \blue{\lstinlinecorrectness.ma}: 53 54 \smallskip % 55 \begin{itemize} 56 \item Addressing \red{intensional} properties  clock cycles, stack bytes 57 58 \smallskip % 59 \item As well as \red{extensional} properties  functional correctness. 60 \end{itemize} 61 \item An executable costannotating compiler \blue{\lstinlinecerco} 62 extracted from the formalisation. 63 \end{itemize} 64 65 \medskip % 66 This talk treats the frontend compiler and proof, describing the technical 67 challenges and contributions from the work in Period~3. 68 69 \end{frame} 70 71 \begin{frame}{Compiler} 72 73 The CerCo compiler, given C source code, will generate: 74 \begin{itemize} 75 \item Labelled Clight source code; 76 \item Labelled 8051 object code; 77 \item Cost maps: for each label a count of time (clock cycles) and space 78 (stack bytes) usage. 79 \end{itemize} 80 81 \medskip % 82 The compiler operates in multiple passes, with each intermediate language 83 having an executable semantics in Matita: % 84 \vspace*{\medskipamount} 85 \begin{center} 86 \includegraphics[width=0.7\linewidth]{compilerplain.pdf} 87 \end{center} 88 \vspace*{\medskipamount} 89 90 \end{frame} 91 92 \begin{frame}{Correctness} 93 94 Suppose we have C source with labelled Clight, labelled 8051 binary, and 95 cost maps all generated from the CerCo compiler. 96 97 \medskip % 98 Then the Matita theorem for correctness is that: 99 \begin{itemize} 100 \item Executing the original and labelled Clight source gives the same 101 behaviour; 102 \item Executing the 8051 binary gives the same observables: labels and 103 call/return; 104 \item Applying the cost maps to the trace of C labels correctly 105 describes the time and space usage of the 8051 execution. 106 \end{itemize} 107 108 In fact we give an exact result on all \red{measurable subtraces}: from any 109 label to the end of its enclosing function. 110 111 \medskip % 112 The machinechecked proof is the concatenation of correctness results for 113 the front end, the back end, and the assembler. 114 115 \end{frame} 116 117 \begin{frame}{FrontEnd Progress} 118 119 \vspace*{\bigskipamount} 120 \begin{center} 121 \includegraphics[width=0.7\linewidth]{compilerplain.pdf} 122 \end{center} 123 \vspace*{\medskipamount} 124 125 At the start of Period~3 the front end included in Matita: 126 \begin{itemize} 127 \item Executable semantics for source and intermediate languages; 128 \item Labelling and compilation of source through these; 129 \item Innovation of \red{structured traces}, originally to support timing 130 computation in the assembler. 131 \end{itemize} 132 133 At the completion of Period~3, the front end included proofs of correctness 134 for all these, extension to stack usage, and considerable refinement of the 135 existing formal development. 136 137 \end{frame} 138 139 \begin{frame}{FrontEnd Contribution} 140 141 Notable features and original elements of the frontend include: 142 \begin{itemize} 143 \item Proof layering: 144 \begin{itemize} 145 \item A \blue{functional correctness proof}; 146 \item A \blue{cost proof}, separate but depending on functional 147 correctness. 148 \end{itemize} 149 \item \blue{Internal checks} as a proof shortcut, like translation 150 validation. 151 \item \blue{Structured traces} for holding detailed data on resource 152 behaviour, not just for assembler cost calculation. 153 \item Introduction of \blue{measurable subtraces} as a unit of cost 154 proof. 155 \end{itemize} 156 These features are significant in particular because: 157 \begin{itemize} 158 \item Compilation is not 11 transliteration: code is rearranged and 159 modified, but label sequencing is preserved; 160 \item The source language has implicit control flow constraints not present 161 in the target (call/return, branches, loops). 162 \end{itemize} 163 164 \end{frame} 165 166 \begin{frame}{Axiomatization} 167 168 The translation in \blue{\lstinlinecompile.ma} is complete  essential 169 for extracting a compiler. 170 171 \medskip % 172 The simulation results in \blue{\lstinlinecorrectness.ma} are fully 173 specified, and with substantially complete proofs. Some parts, however, 174 have been axiomatized and their correctness assumed. 175 176 \medskip % 177 In the frontend there are two sources of this axiomatisation: 178 \begin{itemize} 179 \item \red{Functional correctness.} Other projects, notably 180 \blue{CompCert}, provide assurances that such proofs can be completed; so 181 certain parts of this proof have been assumed. 182 \item Simulation steps with \red{many cases}, sometimes similar; here we 183 have identified representative and more challenging cases for detailed 184 proof. 185 \end{itemize} 186 187 \end{frame} 188 189 \begin{frame}[fragile] 190 \frametitle{Structure of the Proof} 191 192 \begin{center} 193 \includegraphics[width=0.7\linewidth]{compiler.pdf} 194 \end{center} 195 196 The transition from frontend to backend marks the change: 197 \begin{itemize} 198 \item From a language with explicit call/return structure and highlevel 199 control flow; 200 \item To a language with explicit addresses and controlflow graph. 201 \end{itemize} 202 203 Correspondingly, the proof hands over 204 \begin{itemize} 205 \item From measurable subtraces with labelling that must be checked 206 \blue{sound} and \blue{precise}; 207 \item To \blue{structured traces} which embed these invariants. 208 \end{itemize} 209 210 \end{frame} 211 212 213 % \frame{ 214 % \frametitle{Introduction} 215 216 % D3.4 is the frontend correctness proofs: 217 218 % \begin{description} 219 % \item[Primary focus:] novel \red{intensional} properties: \blue{cost 220 % bound correctness} 221 % \item[Secondary:] usual \red{extensional} result: \blue{functional correctness} 222 % \end{description} 223 224 % Functional correctness for similar compilers already studied in 225 % Leroy et al.'s \blue{CompCert}. 226 % \begin{itemize} 227 % \item Axiomatize similar results 228 % \end{itemize} 229 230 % \medskip 231 % Now have \blue{stack} costs as well as \blue{time} 232 % \begin{itemize} 233 % \item yields stronger overall correctness result 234 % \end{itemize} 235 236 % \medskip 237 % \alert{Extract} compiler code from development for practical execution. 238 239 % \medskip 240 % Informed by earlier formal experiment with a toy compiler. 241 % } 65 242 66 243 % TODO: could reuse some of this to make stronger intro? … … 93 270 % } 94 271 95 \frame{ 96 \frametitle{Outline} 97 \tableofcontents 98 } 99 100 \section{CerCo Compiler} 101 102 \frame{ 103 \frametitle{CerCo compiler} 104 105 \begin{center} 106 \includegraphics[width=0.6\linewidth]{compilerplain.pdf} 107 \end{center} 108 109 \begin{itemize} 110 \item Reuse unverified CompCert \alert{parser} 111 %\item Transform away troublesome constructs 112 % \begin{itemize} 113 % \item e.g.~\texttt{switch} 114 % \item fallthrough requires slightly more sophisticated labelling 115 % \item but not fundamentally different 116 % \end{itemize} 117 \item Intermediate language for most passes 118 \item \alert{Executable semantics} for each 119 \item \alert{Extract} OCaml compiler code from development 120 \item Outputs 121 \begin{itemize} 122 \item \alert{8051 machine code} 123 \item Clight code instrumented with costs in 8051 \alert{clock cycles} and 124 \alert{bytes of stack space} 125 \end{itemize} 126 \end{itemize} 127 Instrumentation updates global cost variable; suitable for further analysis and 128 verification. 129 } 130 131 \section{Overall correctness} 132 133 \begin{frame}[fragile] 134 \frametitle{Correctness of labelling approach} 135 136 \begin{tabular}{ccc} 137 138 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 139 emph={[2]_cost3},emphstyle={[2]\color{blue}}] 140 char f(char x) { 141 char y; 142 _cost3: 143 if (x>10) { 144 _cost1: 145 y = g(x); 146 } else { 147 _cost2: 148 y = 5; 149 } 150 return y+1; 151 } 152 \end{lstlisting} 153 154 & 155 156 \begin{minipage}{9em} 157 \begin{center} 158 $\Rightarrow$\\[4ex] 159 \blue{soundness}\\[2ex] 160 \red{precision} 161 \end{center} 162 \end{minipage} 163 164 & 165 166 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 167 emph={[2]_cost3},emphstyle={[2]\color{blue}}] 168 "f" 169 emit _cost3 170 *** Prologue *** 171 move A, R06 172 clear CARRY 173 ... 174 branch A <> 0, f10 175 emit _cost2 176 imm R00, 5 177 ... 178 f10: 179 emit _cost1 180 call "g" 181 ... 182 \end{lstlisting} 183 184 185 \end{tabular} 186 187 From experiments with toy compiler [D2.1, FMICS'12]: 188 \begin{enumerate} 189 \item Functional correctness, \emph{including trace of labels} 190 %\item Source labelling function is sound and precise 191 %\item Preservation of soundness and precision of labelling 192 \item Target labelling function is sound and precise 193 % TODO: detail about soundness and precision? 194 \item Target cost analysis produces a map of labels to times 195 \begin{itemize} 196 \item Accurate for sound and precise labellings 197 \end{itemize} 198 %\item Correctness of instrumentation 199 \end{enumerate} 200 201 \end{frame} 202 203 %\frame{ 204 %\frametitle{} 205 % 206 %Due to resource constraints 207 %\begin{itemize} 208 %\item Instrumentation is done in language semantics 209 %\item Soundness and precision of labelling is checked during compilation 210 % \begin{itemize} 211 % \item c.f.~translation validation 212 % \end{itemize} 213 %\item Focusing effort on novel parts  cost proofs over functional correctness 214 %\end{itemize} 215 % 216 %} 217 218 \begin{frame}[fragile] 219 \frametitle{Overall correctness statement} 220 221 \[ \text{max predicted stack usage} \leq \text{limit} \] 222 implies 223 \begin{itemize} 224 \item successful execution, with 225 \end{itemize} 226 \begin{center} 227 \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} 228 \end{center} 229 \end{frame} 230 231 232 \begin{frame}[fragile] 233 \frametitle{Overall correctness statement} 234 235 \begin{center} 236 \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} 237 \end{center} 238 239 %\pause 240 241 \begin{center} 242 \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c} 243 244 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 245 emph={[2]_cost3},emphstyle={[2]\color{blue}}] 246 int f(int x) { 247 _cost1: 248 int y = 0; 249 while (x) { 250 _cost2: 251 y = g(y); 252 x = x  1; 253 } 254 _cost3: 255 return y; 256 } 257 \end{lstlisting} 258 259 & 260 261 \begin{uncoverenv}<12> 262 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 263 emph={[2]_cost3},emphstyle={[2]\color{blue}}] 264 call f 265 _cost1 266 init y 267 _cost2 268 call g 269 ... 270 return g 271 assign y 272 decrement x 273 test x 274 _cost2 275 ... 276 _cost3 277 return f 278 \end{lstlisting} 279 \end{uncoverenv} 280 281 & 282 283 \begin{uncoverenv}<24> 284 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 285 emph={[2]_cost3},emphstyle={[2]\color{blue}}] 286 call f 287 _cost1 288 289 _cost2 290 call g 291 ... 292 return g 293 294 295 296 _cost2 297 ... 298 _cost3 299 return f 300 \end{lstlisting} 301 \end{uncoverenv} 302 303 \end{tabular} 304 \end{center} 305 306 \begin{overprint} 307 \onslide<12> 308 \begin{itemize} 309 \item Which parts can we measure execution costs of? 310 \item Actual position of unobservable computation is unimportant 311 \item Want to get \alert{exact} execution time 312 \end{itemize} 313 314 \onslide<3> 315 \begin{itemize} 316 \item Use labels and end of function as measurement points 317 \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' 318 \item All costs are considered local to the function 319 \end{itemize} 320 321 \onslide<4> 322 \begin{itemize} 323 \item Use labels and end of function as measurement points 324 \item[$\star$] Call suitable subtraces \alert{measurable} 325 \item[$\star$] Core part is a proof that the trace \alert{terminates} at return 326 \end{itemize} 327 328 % \onslide<1> 272 % \frame{ 273 % \frametitle{Outline} 274 % \tableofcontents 275 % } 276 277 % \section{CerCo Compiler} 278 279 % \frame{ 280 % \frametitle{CerCo compiler} 281 282 % \begin{center} 283 % \includegraphics[width=0.8\linewidth]{compilerplain.pdf} 284 % \end{center} 285 286 % \begin{itemize} 287 % \item Reuse unverified CompCert parser 288 % %\item Transform away troublesome constructs 289 % % \begin{itemize} 290 % % \item e.g.~\texttt{switch} 291 % % \item fallthrough requires slightly more sophisticated labelling 292 % % \item but not fundamentally different 293 % % \end{itemize} 294 % \item Intermediate language for most passes 295 % \item Executable semantics for each 296 % \item Outputs 297 % \begin{itemize} 298 % \item 8051 machine code 299 % \item Clight code instrumented with costs in 8051 clock cycles and 300 % bytes of stack space 301 % \end{itemize} 302 % \end{itemize} 303 % Instrumentation updates global cost variable; suitable for further analysis and 304 % verification. 305 % } 306 307 % \section{Overall correctness} 308 309 % \begin{frame}[fragile] 310 % \frametitle{Correctness of labelling approach} 311 312 % \begin{tabular}{ccc} 313 314 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 315 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 316 % char f(char x) { 317 % char y; 318 % _cost3: 319 % if (x>10) { 320 % _cost1: 321 % y = g(x); 322 % } else { 323 % _cost2: 324 % y = 5; 325 % } 326 % return y+1; 327 % } 328 % \end{lstlisting} 329 330 % & 331 332 % \begin{minipage}{9em} 333 % \begin{center} 334 % $\Rightarrow$\\[4ex] 335 % \blue{soundness}\\[2ex] 336 % \red{precision} 337 % \end{center} 338 % \end{minipage} 339 340 % & 341 342 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 343 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 344 % "f" 345 % emit _cost3 346 % *** Prologue *** 347 % move A, R06 348 % clear CARRY 349 % ... 350 % branch A <> 0, f10 351 % emit _cost2 352 % imm R00, 5 353 % ... 354 % f10: 355 % emit _cost1 356 % call "g" 357 % ... 358 % \end{lstlisting} 359 360 361 % \end{tabular} 362 363 % From experiments with toy compiler [D2.1, FMICS'12]: 364 % \begin{enumerate} 365 % \item Functional correctness, \emph{including trace of labels} 366 % %\item Source labelling function is sound and precise 367 % %\item Preservation of soundness and precision of labelling 368 % \item Target labelling function is sound and precise 369 % % TODO: detail about soundness and precision? 370 % \item Target cost analysis produces a map of labels to times 371 % \begin{itemize} 372 % \item Accurate for sound and precise labellings 373 % \end{itemize} 374 % %\item Correctness of instrumentation 375 % \end{enumerate} 376 377 % \end{frame} 378 379 % %\frame{ 380 % %\frametitle{} 381 % % 382 % %Due to resource constraints 383 % %\begin{itemize} 384 % %\item Instrumentation is done in language semantics 385 % %\item Soundness and precision of labelling is checked during compilation 386 % % \begin{itemize} 387 % % \item c.f.~translation validation 388 % % \end{itemize} 389 % %\item Focusing effort on novel parts  cost proofs over functional correctness 390 % %\end{itemize} 391 % % 392 % %} 393 394 % \begin{frame}[fragile] 395 % \frametitle{Overall correctness statement} 396 397 % \begin{center} 398 % \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} 399 % \end{center} 400 401 % \pause 402 403 % \begin{center} 404 % \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c} 405 406 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 407 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 408 % int f(int x) { 409 % _cost1: 410 % int y = 0; 411 % while (x) { 412 % _cost2: 413 % y = g(y); 414 % x = x  1; 415 % } 416 % _cost3: 417 % return y; 418 % } 419 % \end{lstlisting} 420 421 % & 422 423 % \begin{uncoverenv}<23> 424 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 425 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 426 % call f 427 % _cost1 428 % init y 429 % _cost2 430 % call g 431 % ... 432 % return g 433 % assign y 434 % decrement x 435 % test x 436 % _cost2 437 % ... 438 % _cost3 439 % return f 440 % \end{lstlisting} 441 % \end{uncoverenv} 442 443 % & 444 445 % \begin{uncoverenv}<35> 446 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 447 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 448 % call f 449 % _cost1 450 451 % _cost2 452 % call g 453 % ... 454 % return g 455 456 457 458 % _cost2 459 % ... 460 % _cost3 461 % return f 462 % \end{lstlisting} 463 % \end{uncoverenv} 464 465 % \end{tabular} 466 % \end{center} 467 468 % \begin{overprint} 469 % \onslide<2> 329 470 % \begin{itemize} 330 471 % \item Use labels and end of function as measurement points … … 332 473 % \end{itemize} 333 474 334 % \onslide< 23>475 % \onslide<34> 335 476 % \begin{itemize} 336 477 % \item Use labels and end of function as measurement points … … 339 480 % \end{itemize} 340 481 341 % \onslide< 4>482 % \onslide<5> 342 483 % \begin{itemize} 343 484 % \item Use labels and end of function as measurement points … … 345 486 % \item[$\star$] Core part is a proof of \alert{termination} 346 487 % \end{itemize} 347 \end{overprint}348 349 \end{frame}350 351 \begin{frame}[fragile]352 \frametitle{Correct cost analysis depends on call structure}353 354 Two straightline functions:355 356 \begin{center}357 \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}358 359 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},360 emph={[2]_cost3},emphstyle={[2]\color{blue}}]361 "f"362 emit _cost1363 ...364 call "g"365 ...366 return367 \end{lstlisting}368 369 &370 371 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},372 emph={[2]_cost3},emphstyle={[2]\color{blue}},373 escapechar=\%]374 "g"375 emit _cost2376 ...377 %\only<2>{\blue{increase return address}}%378 return379 \end{lstlisting}380 381 \end{tabular}382 \end{center}383 384 Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).385 386 \begin{itemize}387 \item<2> Changing return address skips code from \lstinline'f'388 \item<2> Cost no longer equals sum of cost labels389 \end{itemize}390 391 \onslide<2>392 \alert{Need to observe correct call/return structure.}393 394 \onslide<3>395 \emph{Not easy at ASM  observe earlier in compiler \& maintain.}396 397 \end{frame}398 399 \section{Frontend correctness}400 401 \frame{402 \frametitle{Frontend correctness}403 404 Recalling the toy compiler, need405 \begin{enumerate}406 \item Functional correctness407 \item Cost labelling sound and precise408 \item\label{it:return} To demonstrate return addresses are correct409 \end{enumerate}410 % TODO: stack space? from obs, from fnl correctness411 412 \bigskip413 For~\ref{it:return} we generalise notion of \emph{structured traces}414 originally introduced for the correctness of timing analysis.415 }488 % \end{overprint} 489 490 % \end{frame} 491 492 % \begin{frame}[fragile] 493 % \frametitle{Correct cost analysis depends on call structure} 494 495 % Two straightline functions: 496 497 % \begin{center} 498 % \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}} 499 500 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 501 % emph={[2]_cost3},emphstyle={[2]\color{blue}}] 502 % "f" 503 % emit _cost1 504 % ... 505 % call "g" 506 % ... 507 % return 508 % \end{lstlisting} 509 510 % & 511 512 % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 513 % emph={[2]_cost3},emphstyle={[2]\color{blue}}, 514 % escapechar=\%] 515 % "g" 516 % emit _cost2 517 % ... 518 % %\only<2>{\blue{increase return address}}% 519 % return 520 % \end{lstlisting} 521 522 % \end{tabular} 523 % \end{center} 524 525 % Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}). 526 527 % \begin{itemize} 528 % \item<2> Changing return address skips code from \lstinline'f' 529 % \item<2> Cost no longer equals sum of cost labels 530 % \end{itemize} 531 532 % \onslide<2> 533 % \alert{Need to observe correct call/return structure.} 534 535 % \onslide<3> 536 % \emph{Not easy at ASM  observe earlier in compiler \& maintain.} 537 538 % \end{frame} 539 540 % \section{Frontend correctness} 541 542 % \frame{ 543 % \frametitle{Frontend correctness} 544 545 % Recalling the toy compiler, need 546 % \begin{enumerate} 547 % \item Functional correctness 548 % \item Cost labelling sound and precise 549 % \item\label{it:return} To demonstrate return addresses are correct 550 % \end{enumerate} 551 % % TODO: stack space? from obs, from fnl correctness 552 553 % \bigskip 554 % For~\ref{it:return} we generalise notion of \emph{structured traces} 555 % originally introduced for the correctness of timing analysis. 556 % } 416 557 417 558 \begin{frame}[fragile] 418 559 \frametitle{Structured traces} 419 560 420 \alert{Embed} the call/return structureinto execution traces.561 Embed call structure and label invariants into execution traces. 421 562 422 563 \begin{center} … … 425 566 426 567 \begin{itemize} 427 \item Traces of \alert{called functions} are nested 428 \item Invariants on positions of cost labels enforced 429 \item Steps are \alert{grouped} according to cost label 430 \item Forbid \alert{repeating} addresses in grouped steps for 431 \blue{sound} labelling 432 \end{itemize} 433 434 % moved later 435 %\onslide<2> 436 %Construct by folding up \alert{measurable} subtrace, using soundness 437 %and preciseness of labelling. 438 439 \end{frame} 440 441 \frame{ 442 \frametitle{Frontend correctness statement} 443 444 Given a \red{measurable} subtrace of a \textbf{Clight} execution, including 445 the \textbf{prefix} of that trace from initial state, 446 447 \medskip 448 we have in \textbf{RTLabs} 449 \begin{itemize} 450 \item a new \textbf{prefix} 451 \item a \blue{structured trace} corresponding to \red{measurable} 452 subtrace 453 \item the no \blue{repeating} addresses property 454 \item proof that the same \textbf{stack limit} is observed 455 \end{itemize} 456 which the backend requires, and 457 \begin{itemize} 458 \item the observables for the \textbf{prefix} and \blue{structured 459 trace} are the same as their \textbf{Clight} counterparts 460 \end{itemize} 461 which links the behaviour and costs to the original program. 462 } 463 464 \begin{frame}[fragile] 465 \frametitle{Structure in the compiler proof} 466 467 \begin{center} 468 \includegraphics[width=0.8\linewidth]{compiler.pdf} 469 \end{center} 470 471 %\onslide<1> 472 %\green{Assembler} provides part of local cost analysis (CPP'12). 473 474 %\onslide<24> 475 Switch at RTLabs: 476 \begin{itemize} 477 \item from \red{measurable} subtrace of \alert{sound} and \alert{precise} 478 labelling 479 \item to \blue{structured trace} where they are embedded 480 \end{itemize} 481 482 %\onslide<3> 483 %Changes \blue{syntactic} properties of labelling into \blue{semantic} 484 %properties. 485 486 %\onslide<4> 487 Reason for choice: first language with explicit \alert{addresses}, implicit 488 \alert{call handling}. 489 490 \end{frame} 491 492 \section{Correctness proofs} 493 \subsection{Generic lifting result} 568 \item Enforces \blue{invariants} on positions of cost labels. 569 \item \blue{Groups} execution steps according to preceding cost label. 570 \item Forbids \blue{repeating} addresses in grouped steps. 571 \end{itemize} 572 573 Constructed by folding up measurable subtraces, using the fact that labelling 574 is sound and precise. 575 576 \end{frame} 577 578 \begin{frame}{StepbyStep: Getting to Labelled Source} 579 580 \blue{C $\to$ Clight} 581 582 \smallskip % 583 To translate from C to Clight we reuse the CompCert parser. 584 585 \bigskip % 586 \blue{Switch Removal} 587 588 \smallskip % 589 Control flow for \red{\lstinline'switch'} is too subtle for simple labelling; 590 we replace with an \red{\lstinline'if .. then .. else'} tree. Proof requires 591 tracking memory extension for an extra test variable. 592 593 \bigskip % 594 \blue{Cost Labels} 595 596 \smallskip % 597 Labels added at function start, branch targets, \dots 598 599 \smallskip % 600 Simulation of execution is exact, just skipping over labels. 601 602 \end{frame} 603 604 \begin{frame}{FrontEnd Correctness} 605 606 Suppose we have a \blue{measurable} subtrace of Clight execution, including 607 the \blue{prefix} of that trace from initial state. 608 609 \medskip % 610 Then for handover to the backend we have in RTLabs: 611 \begin{itemize} 612 \item A corresponding \red{prefix}; 613 \item A \red{structured trace} corresponding to the measurable subtrace; 614 \item The required invariants, including \red{no repeating addresses}; 615 \item A proof that the same \red{stack limit} is observed. 616 \end{itemize} 617 618 \medskip % 619 In addition, to link this with the source program: 620 \begin{itemize} 621 \item The observables for the RLabs \blue{prefix} and \blue{structured 622 trace} are the same as for their counterparts in Clight. 623 \end{itemize} 624 625 \end{frame} 626 627 628 % \section{Correctness proofs} 629 % \subsection{Generic lifting result} 494 630 495 631 \begin{frame}[fragile] … … 572 708 %\end{frame} 573 709 574 \subsection{Simulations for compiler passes}710 % \subsection{Simulations for compiler passes} 575 711 576 712 %\frame{ … … 579 715 580 716 % TODO: perhaps much earlier for the premeasurable bits? 581 \frame{582 \frametitle{Simulation between input and annotated code}583 584 Two stages provide the annotated version of input:585 586 \bigskip587 Switch removal588 \begin{itemize}589 \item \lstinline[language=C]'switch' statement control flow too subtle590 for simple labelling591 \item Replaces with \lstinline[language=C]'if ... then ... else' tree592 \item Tricky part of proof: memory extension for extra variable593 \item Partial proof: enough to validate approach;\\594 \quad  this stage not relevant to intensional properties595 \end{itemize}596 597 \bigskip598 Cost labelling599 \begin{itemize}600 \item For simulation don't care \emph{which} labels are added601 \item Just have to skip over extra cost label expressions and602 statements603 \item Complete simulation proof, simple604 \end{itemize}605 606 % TODO: consider whether to mention full simulation607 % terminationpreserving proof?608 }609 717 610 718 \frame{ … … 639 747 \item But do have invariants: 640 748 \begin{itemize} 641 \item [$\bullet$] Statementswelltyped with respect to pseudoregister749 \item Statement welltyped with respect to pseudoregister 642 750 environment 643 \item [$\bullet$]CFG complete644 \item [$\bullet$] Entry and exit nodes present, unique751 \item CFG complete 752 \item Entry and exit nodes complete, unique 645 753 \end{itemize} 646 754 \item Translation function is \emph{total} as a result … … 650 758 % TODO: sloganize: proved more about unusual bits 651 759 652 \section{Checking cost labelling properties}760 % \section{Checking cost labelling properties} 653 761 654 762 \frame{ … … 721 829 } 722 830 723 \section{Construction of structured traces}831 % \section{Construction of structured traces} 724 832 725 833 \frame{ … … 739 847 } 740 848 741 \section{Whole compiler}849 % \section{Whole compiler} 742 850 743 851 \begin{frame}[fragile] … … 749 857 750 858 \begin{itemize} 751 \item Instantiate measurable subtracing lifting with simulations 752 \item Show existence of \textbf{RTLabs} structured trace 753 \item Apply backend to show \textbf{RTLabs} costs correct 754 \item Use equivalence of observables to show \textbf{Clight} costs correct 755 % \item `Clock' difference in Clight is sum of cost labels 756 % \item Observables, including trace of labels, is preserved to ASM 757 % \item Labelling at bottom level is sound and precise 758 % \item Sum of labels at ASM is equal to difference in real clock 859 \item `Clock' difference in Clight is sum of cost labels 860 \item Observables, including trace of labels, is preserved to ASM 861 \item Labelling at bottom level is sound and precise 862 \item Sum of labels at ASM is equal to difference in real clock 759 863 \end{itemize} 760 864
Note: See TracChangeset
for help on using the changeset viewer.