Changeset 3267 for Deliverables/Dissemination
- Timestamp:
- May 13, 2013, 11:26:11 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/front-end/front-end.tex
r3266 r3267 38 38 \frametitle{Introduction} 39 39 40 D3.4 isthe front-end correctness proofs:40 D3.4 consists of the front-end correctness proofs: 41 41 42 42 \begin{description} 43 43 \item[Primary focus:] novel \red{intensional} properties: \blue{cost 44 44 bound correctness} 45 \item[Secondary:] usual \red{extensional} result: \blue{functional correctness}46 45 \end{description} 47 48 Functional correctness for similar compilers already studied in 49 Leroy et al.'s \blue{CompCert}. 50 \begin{itemize} 46 \vskip-2ex 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 \vskip-2ex 58 \begin{itemize} 59 \item Similar functional correctness already studied in 60 \blue{CompCert} 51 61 \item Axiomatize similar results 52 \end{itemize} 53 54 \medskip 55 Now have \blue{stack} costs as well as \blue{time} 56 \begin{itemize} 57 \item yields stronger overall correctness result 58 \end{itemize} 59 60 \medskip 61 \alert{Extract} compiler code from development for practical execution. 62 63 \medskip 64 Informed by earlier formal experiment with a toy compiler. 62 \item \red{Intensional} proofs form a layer on top 63 \end{itemize} 65 64 } 66 65 … … 105 104 106 105 \begin{center} 107 \includegraphics[width=0. 8\linewidth]{compiler-plain.pdf}108 \end{center} 109 110 \begin{itemize} 111 \item Reuse unverified CompCert parser106 \includegraphics[width=0.6\linewidth]{compiler-plain.pdf} 107 \end{center} 108 109 \begin{itemize} 110 \item Reuse unverified CompCert \alert{parser} 112 111 %\item Transform away troublesome constructs 113 112 % \begin{itemize} … … 117 116 % \end{itemize} 118 117 \item Intermediate language for most passes 119 \item Executable semantics for each 118 \item \alert{Executable semantics} for each 119 \item \alert{Extract} OCaml compiler code from development 120 120 \item Outputs 121 121 \begin{itemize} 122 \item 8051 machine code123 \item Clight code instrumented with costs in 8051 clock cyclesand124 bytes of stack space122 \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 125 \end{itemize} 126 126 \end{itemize} … … 219 219 \frametitle{Overall correctness statement} 220 220 221 \[ \text{max predicted stack usage} \leq \text{limit} \] 222 implies 223 \begin{itemize} 224 \item successful execution, with 225 \end{itemize} 221 226 \begin{center} 222 227 \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} 223 228 \end{center} 224 225 \pause 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 226 240 227 241 \begin{center} … … 245 259 & 246 260 247 \begin{uncoverenv}< 2-3>261 \begin{uncoverenv}<1-2> 248 262 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 249 263 emph={[2]_cost3},emphstyle={[2]\color{blue}}] … … 267 281 & 268 282 269 \begin{uncoverenv}< 3-5>283 \begin{uncoverenv}<2-4> 270 284 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 271 285 emph={[2]_cost3},emphstyle={[2]\color{blue}}] … … 291 305 292 306 \begin{overprint} 293 \onslide<2> 294 \begin{itemize} 295 \item Use labels and end of function as measurement points 296 \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' 297 \end{itemize} 298 299 \onslide<3-4> 300 \begin{itemize} 301 \item Use labels and end of function as measurement points 302 \item All costs are considered local to the function 303 \item Actual position of unobservable computation is unimportant 304 \end{itemize} 305 306 \onslide<5> 307 \begin{itemize} 308 \item Use labels and end of function as measurement points 309 \item[$\star$] Call suitable subtraces \alert{measurable} 310 \item[$\star$] Core part is a proof of \alert{termination} 311 \end{itemize} 307 \onslide<1-2> 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> 329 % \begin{itemize} 330 % \item Use labels and end of function as measurement points 331 % \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' 332 % \end{itemize} 333 334 % \onslide<2-3> 335 % \begin{itemize} 336 % \item Use labels and end of function as measurement points 337 % \item All costs are considered local to the function 338 % \item Actual position of unobservable computation is unimportant 339 % \end{itemize} 340 341 % \onslide<4> 342 % \begin{itemize} 343 % \item Use labels and end of function as measurement points 344 % \item[$\star$] Call suitable subtraces \alert{measurable} 345 % \item[$\star$] Core part is a proof of \alert{termination} 346 % \end{itemize} 312 347 \end{overprint} 313 348 … … 407 442 \frametitle{Front-end correctness statement} 408 443 409 Given a \ blue{measurable} subtrace of a \textbf{Clight} execution, including444 Given a \red{measurable} subtrace of a \textbf{Clight} execution, including 410 445 the \textbf{prefix} of that trace from initial state, 411 446 … … 414 449 \begin{itemize} 415 450 \item a new \textbf{prefix} 416 \item a \ red{structured trace} corresponding to \blue{measurable}451 \item a \blue{structured trace} corresponding to \red{measurable} 417 452 subtrace 418 \item the no \ red{repeating} addresses property453 \item the no \blue{repeating} addresses property 419 454 \item proof that the same \textbf{stack limit} is observed 420 455 \end{itemize} 421 456 which the back-end requires, and 422 457 \begin{itemize} 423 \item the observables for the \textbf{prefix} and \ red{structured458 \item the observables for the \textbf{prefix} and \blue{structured 424 459 trace} are the same as their \textbf{Clight} counterparts 425 460 \end{itemize} … … 555 590 for simple labelling 556 591 \item Replaces with \lstinline[language=C]'if ... then ... else' tree 557 \item Tricky part of proof memory extension for extra variable558 \item Partial proof: validate approach, but not relevant to559 intensional properties592 \item Tricky part of proof: memory extension for extra variable 593 \item Partial proof: enough to validate approach;\\ 594 \quad --- this stage not relevant to intensional properties 560 595 \end{itemize} 561 596 … … 604 639 \item But do have invariants: 605 640 \begin{itemize} 606 \item Statementwell-typed with respect to pseudo-register641 \item[$\bullet$] Statements well-typed with respect to pseudo-register 607 642 environment 608 \item CFG complete609 \item Entry and exit nodes complete, unique643 \item[$\bullet$] CFG complete 644 \item[$\bullet$] Entry and exit nodes present, unique 610 645 \end{itemize} 611 646 \item Translation function is \emph{total} as a result … … 714 749 715 750 \begin{itemize} 716 \item `Clock' difference in Clight is sum of cost labels 717 \item Observables, including trace of labels, is preserved to ASM 718 \item Labelling at bottom level is sound and precise 719 \item Sum of labels at ASM is equal to difference in real clock 751 \item Instantiate measurable subtracing lifting with simulations 752 \item Show existence of \textbf{RTLabs} structured trace 753 \item Apply back-end 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 720 759 \end{itemize} 721 760
Note: See TracChangeset
for help on using the changeset viewer.