Changeset 1852 for Deliverables/D1.2
 Timestamp:
 Mar 15, 2012, 4:02:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/Presentations/WP3.tex
r1845 r1852 34 34 %\setbeamertemplate{footline}[page number] 35 35 %\setbeamertemplate{sidebar right}{} 36 \setbeamertemplate{navigation symbols}{} 36 37 37 38 \lstdefinelanguage{coq} … … 75 76 76 77 \frame{ 77 \frametitle{Introduction} 78 79 An interleaved presentation of work on: 80 \begin{description} 81 \item[T3.2] The encoding of the frontend of the \cerco{} compiler in CIC 82 \item[T3.3] Defining the executable semantics of the frontend's intermediate 83 language 84 \item[T3.4] Correctness proofs 78 \frametitle{Achievements in period 2} 79 80 \begin{description}[T3.2] 81 \item[T3.2] \alert{Completed}: Matita encoding of compiler frontend 82 \item[T3.3] \alert{Completed}: Executable semantics for intermediate languages 83 \item[T3.4] \alert{In progress}: Correctness proofs 85 84 \end{description} 86 85 87 86 \bigskip 88 Deliverables D3.2 and D3.3 have been produced. 87 Deliverables D3.2 and D3.3 submitted. 88 89 \bigskip 90 This talk is an interleaved presentation of these results. 91 89 92 90 93 } … … 95 98 96 99 \begin{itemize} 97 \item Common definitions for everything98 \item The front end:99 \end{itemize}100 101 \ begin{tabbing}100 \item Shared definitions 101 %\item The front end: 102 %\end{itemize} 103 %\vspace{3ex} 104 \item \begin{tabbing} 102 105 \quad \= $\downarrow$ \quad \= \kill 103 106 \gray{\textsf{C} (unformalized)}\\ … … 115 118 \> \,\gray{\vdots} \> \gray{start of target specific backend} 116 119 \end{tabbing} 117 118 \begin{itemize}120 %\vspace{3ex} 121 %\begin{itemize} 119 122 \item Structured traces 120 123 \end{itemize} … … 122 125 } 123 126 124 \section{ Common}125 126 \begin{frame}[fragile] 127 \frametitle{ Common: identifiers}128 129 Variable and function names, cost labels, registers, CFG labels, \dots127 \section{Shared} 128 129 \begin{frame}[fragile] 130 \frametitle{Shared definitions} 131 132 Identifiers: variables, cost labels, CFG labels, \dots 130 133 131 134 \begin{itemize} 132 135 \item Represented by arbitrarily large binary numbers and trees 133 136 \begin{itemize} 134 \item D3.3 described a `lazy failure' approach reusing existing structures 135 \item Impractical for adding invariants (types may depend on success of 136 name generation) 137 \item Use this CompCertlike system instead 137 \item D3.3 `lazy failure' approach reusing existing structures 138 \item Invariant's types may depend on success of name generation 139 %\item Use this CompCertlike system instead 138 140 \end{itemize} 139 141 \item Tags for some type safety: … … 144 146 \end{itemize} 145 147 146 \end{frame} 147 148 \frame{ 149 \frametitle{Other common definitions} 150 151 \begin{itemize} 152 \item Memory, global environments from D3.1 153 \item Bit vector based arithmetic from D4.1 148 Memory, global environments from D3.1\\ 149 Bit vector based arithmetic from D4.1 154 150 \begin{itemize} 155 151 \item added extra operations, increased efficiency 156 152 \end{itemize} 157 \item Common record type for smallstep executable semantics 158 \begin{itemize} 159 \item used for animation 160 \item intended to be used when defining simulations 161 \end{itemize} 162 \end{itemize} 163 164 \bigskip 165 166 \bigskip 153 %Common record type for smallstep executable semantics 154 % \begin{itemize} 155 % \item used for animation 156 % \item intended to be used when defining simulations 157 % \end{itemize} 158 159 160 167 161 \textsf{Cminor} and \textsf{RTLabs} share operations on values. 168 162 169 \begin{itemize} 170 \item one syntax, one semantics 171 \item straightforward 172 \item no overloading (unlike \textsf{Clight}) 173 \end{itemize} 174 175 } 163 164 \end{frame} 176 165 177 166 \section{Clight} … … 179 168 \frametitle{Clight: syntax and semantics} 180 169 181 Largely unchangedfrom D3.1, except:170 Modest evolution from D3.1, except: 182 171 183 172 \medskip … … 197 186 \frametitle{Clight: cast simplification} 198 187 199 \begin{itemize} 200 \ item C insists on arithmetic promotion188 C insists on arithmetic promotion 189 \begin{itemize} 201 190 \item CILbased \ocaml{} parser adds suitable casts 202 191 \item bad for our target (32bit ops instead of 8bit) 203 192 \end{itemize} 204 193 205 Prototype recognises fixed patterns: 194 \medskip 195 Prototype recognises fixed patterns to simplify: 206 196 \[ (t)((t_1)e_1\ op\ (t_2)e_2) \] 207 and replaces when types are right. Have done some preliminary proofs that this 208 works. 197 \vspace{4ex} 209 198 \begin{itemize} 210 199 \item Deep pattern matching is awkward in Matita … … 212 201 \end{itemize} 213 202 214 \red{Instead}: recursive `coerce to desired type' approach.\\ 203 \medskip 204 \red{Instead}: recursive `coerce to desired type' approach. 205 206 Have done some preliminary proofs that this 207 works. 215 208 % (Doesn't get some things, 216 209 % e.g., \lstinline'==') … … 223 216 224 217 \begin{itemize} 225 \item Implemented asa simple recursive function, like prototype218 \item a simple recursive function, like prototype 226 219 \item uses common identifiers definition to produce fresh cost labels 227 220 \end{itemize} … … 241 234 \frametitle{Cminor syntax and semantics} 242 235 243 Similar language to CompCert'sbut developed from prototype.236 Similar to CompCert's  but developed from prototype. 244 237 245 238 \begin{itemize} … … 288 281 \frametitle{Invariants for identifiers} 289 282 290 Invariants change between language syntax/semantics and compilation stages: 283 284 Invariants change between languages and compilation: 291 285 292 286 \begin{description} … … 296 290 \end{description} 297 291 298 When using or creating function records we provethat we can switch between299 them:292 When using or creating function definitions have proved that we can switch between 293 invariants: 300 294 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 301 295 lemma populates_env : $\forall$l,e,u,l',e',u'. … … 303 297 populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ (* build register mapping *) 304 298 $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ (* Anything in the environment... *) 305 Env_has e' i t. 306 (* maps to something of the correct type *) 307 \end{lstlisting} 308 299 Env_has e' i t. (* maps to something of the correct type *) 300 \end{lstlisting} 301 302 \vfill 309 303 \end{frame} 310 304 … … 313 307 314 308 Embedded invariant in the function record: 315 \begin{lstlisting}[language=matita,basicstyle=\scriptsize\tt ]309 \begin{lstlisting}[language=matita,basicstyle=\scriptsize\tt,morekeywords=f_inv] 316 310 record internal_function : Type[0] ≝ 317 311 { f_return : option typ … … 333 327 \end{enumerate} 334 328 335 How is \lstinline'stmt_P' defined? 336 \end{frame} 329 \end{frame} 330 331 332 \section{Clight to Cminor} 333 334 \begin{frame} 335 \frametitle{Clight to Cminor} 336 337 Two main jobs: 338 \begin{enumerate} 339 \item make memory allocation of variables explicit 340 \item use simpler control structures 341 \end{enumerate} 342 Again, based on prototype rather than CompCert. 343 344 \bigskip 345 Added type checking: 346 \begin{itemize} 347 \item satisfies the restrictions for Cminor expressions 348 \item could separate out, have a `nice Clight' language 349 \end{itemize} 350 Similarly, code checks 351 \begin{itemize} 352 \item variable environments are wellformed 353 \item all \lstinline'goto' labels are translated 354 \end{itemize} 355 \end{frame} 356 357 \begin{frame} 358 \frametitle{Clight to Cminor proofs} 359 360 Beyond the invariants already shown, we will prove: 361 362 \medskip 363 \begin{enumerate} 364 \item a simulation relation 365 \begin{itemize} 366 \item between statement and continuation pairs 367 \item using memory injection (similar to CompCert) 368 \end{itemize} 369 \item syntactic cost labelling properties are preserved 370 \begin{itemize} 371 \item structural induction on function body 372 \end{itemize} 373 \end{enumerate} 374 \end{frame} 375 376 \section{Initialisation} 377 \begin{frame} 378 \frametitle{Cminor: initialization} 379 380 Replace initialization data by code in the initial function. 381 382 \begin{itemize} 383 \item straightforward to define 384 \item instantiate a slightly different version of the semantics for it 385 \begin{itemize} 386 \item Can't accidentally forget the pass 387 \end{itemize} 388 \end{itemize} 389 390 \bigskip 391 Correctness should follow because the state after the initialisation will 392 be the same as the initial state of the original. 393 \end{frame} 394 395 \section{RTLabs} 396 \begin{frame}[fragile] 397 \frametitle{RTLabs: syntax and semantics} 398 399 Register Transfer Language with frontend operations. 400 401 Control flow graph implemented by generic identifiers map: 402 403 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 404 definition label := identifier LabelTag. 405 definition graph : Type[0] $\rightarrow$ Type[0] := identifier_map LabelTag. 406 407 inductive statement : Type[0] ≝ 408  St_skip : label $\rightarrow$ statement 409  St_const : register $\rightarrow$ constant $\rightarrow$ label $\rightarrow$ statement 410  St_op1 : $\forall$t,t'. unary_operation t' t $\rightarrow$ register 411 $\rightarrow$ register $\rightarrow$ label $\rightarrow$ statement 412 ... 413 \end{lstlisting} 414 \vspace{1.5ex} 415 \begin{itemize} 416 \item Shares basic operations (including semantics) with Cminor. 417 \item Tags prevent confusion of labels (graph vs.~goto vs.~cost). 418 \end{itemize} 419 420 Semantics straightforward interpretation of statements. 421 \end{frame} 422 423 \begin{frame}[fragile] 424 \frametitle{RTLabs: syntax and semantics} 425 426 \begin{lstlisting}[language=matita] 427 record internal_function : Type[0] ≝ 428 { f_labgen : universe LabelTag 429 ; f_reggen : universe RegisterTag 430 ... 431 ; f_graph : graph statement 432 ; f_closed : graph_closed f_graph 433 ; f_typed : graph_typed (f_locals @ f_params) f_graph 434 ... 435 \end{lstlisting} 436 437 Enforce that 438 \begin{itemize} 439 \item every statement's successor labels are present in the CFG 440 \item every statement should be welltyped (for limited type system) 441 \end{itemize} 442 443 \end{frame} 444 445 \section{Cminor to RTLabs} 446 \begin{frame} 447 \frametitle{Cminor to RTLabs} 448 449 Break down statements and expressions into RTL graph. 450 451 \begin{itemize} 452 \item Incrementally build function backwards 453 \item all state is in function record, like prototype 454 \end{itemize} 455 456 %\bigskip 457 %May investigate whether a state monad makes invariant management easier. 458 459 \bigskip 460 Showing graph closure requires 461 \begin{itemize} 462 \item monotonicity of graph construction 463 \item eventual insertion of all \lstinline'goto' destinations 464 \end{itemize} 465 466 Carry these along in the partially built function record. 467 468 \end{frame} 469 470 % \begin{frame}[fragile] 471 % \frametitle{Cminor nesting depth} 472 473 % Want to prevent 474 % \begin{lstlisting}[language=C] 475 % void f() { 476 % block { loop { exit 5; } } 477 % } 478 % \end{lstlisting} 479 480 % Index statements by block depth 481 % \begin{lstlisting}[language=matita] 482 % inductive stmt : $\forall$blockdepth:nat. Type[0] ≝ 483 %  St_skip : $\forall$n. stmt n 484 % ... 485 %  St_block : $\forall$n. stmt (S n) $\rightarrow$ stmt n 486 %  St_exit : $\forall$n. Fin n $\rightarrow$ stmt n 487 % ... 488 % \end{lstlisting} 489 490 % \begin{itemize} 491 % \item In semantics index continuations too 492 % \item Use \lstinline[language=matita]'Fin n' to make \lstinline'k_exit' 493 % a total function 494 % \end{itemize} 495 496 % (May be able to remove entirely if we redo \lstinline[language=C]{switch}?) 497 % \end{frame} 498 499 \begin{frame}[fragile] 500 \frametitle{Establishing RTLabs invariants} 501 502 Use dependent pairs to show invariant along with results. 503 504 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%] 505 let rec add_expr ... (e:expr ty) 506 (Env:expr_vars ty e (present ?? env)) 507 (f:partial_fn le) 508 on e: $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝ 509 510 match e return 511 $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$ ... with 512 [ ... 513  Cst _ c $\Rightarrow$ $\lambda$_. %\guillemotleft%add_fresh_to_graph ? (St_const dst c) f ?, ?%\guillemotright% 514 ... 515 \end{lstlisting} 516 517 Continually appeal to monotonicity (\lstinline'fn_graph_included').\\ 518 Use unification hints to simplify stepping back. 519 520 \end{frame} 521 522 \frame{ 523 \frametitle{Cminor to RTLabs: cost labels} 524 525 Two cost label properties are the same, the third will require more 526 work: 527 \begin{enumerate} 528 \item cost label at head of function 529 \item cost label after branching instructions 530 \item cost labels at the head of each loop / \lstinline'goto' destination 531 \end{enumerate} 532 533 No simple notion of the head of a loop or \lstinline'goto' any more. 534 535 \medskip 536 Instead: will prove in \alert{Cminor} that after following a finite 537 number of instructions we reach either 538 \begin{itemize} 539 \item a cost label, or 540 \item the end of the function 541 \end{itemize} 542 543 } 544 545 \section{Structured traces} 546 \frame{ 547 \frametitle{RTLabs structured traces} 548 549 Frontend only uses flat traces consisting of single steps. 550 551 \bigskip 552 The backend will need the function call structure and the labelling 553 properties in order to show that the generated costs are correct. 554 555 \begin{itemize} 556 \item Traces are structured in sections from cost label to cost label, 557 \item the entire execution of function calls nested as a single `step', 558 \item a coinductive definition presents nonterminating traces, using the 559 inductive definition for all terminating function calls 560 \end{itemize} 561 562 \bigskip 563 RTLabs chosen because it is the first languages where statements: 564 \begin{itemize} 565 \item take one step each (modulo function calls) 566 \item have individual `addresses' 567 \end{itemize} 568 } 569 570 \frame{ 571 \frametitle{RTLabs structured traces} 572 Have already established the existence of such traces 573 \begin{itemize} 574 \item termination decided classically 575 \item syntactic labelling properties used to build semantic structure 576 \item show stack preservation to ensure that function calls \texttt{return} 577 to the correct location 578 \item tricky to establish guardedness of definitions 579 \end{itemize} 580 581 \bigskip 582 Next, prove that flattening these traces yields the original. 583 } 584 585 \frame{ 586 \frametitle{Conclusion} 587 588 Syntax, semantics and translations of prototype now implemented in Matita. 589 590 \bigskip 591 Have defined and established 592 \begin{itemize} 593 \item invariants regarding variables, typing and program structure 594 \item a rich form of execution trace to pass to the backend 595 \end{itemize} 596 597 \medskip 598 Work in progress: 599 \begin{itemize} 600 \item showing functional correctness of the frontend 601 \item proving that cost labelling is appropriate, and preserved 602 \end{itemize} 603 604 Finally, \alert{endtoend} functional and cost correctness results. 605 606 } 607 608 \frame{ 609 \frametitle{Extra detail beyond here...} 610 } 337 611 338 612 \begin{frame}[fragile] … … 360 634 361 635 \end{frame} 362 363 364 \section{Clight to Cminor}365 366 \begin{frame}367 \frametitle{Clight to Cminor}368 369 Two main jobs:370 \begin{enumerate}371 \item make memory allocation of variables explicit372 \item use simpler control structures373 \end{enumerate}374 Again, based on prototype rather than CompCert.375 376 \bigskip377 Added type checking:378 \begin{itemize}379 \item satisfies the restrictions for Cminor expressions380 \item could separate out, have a `nice Clight' language381 \end{itemize}382 Similarly, check variable environments are sane, check all \lstinline'goto'383 labels are translated.384 \end{frame}385 386 \begin{frame}387 \frametitle{Clight to Cminor proofs}388 389 Beyond the invariants already shown, we need to prove:390 \begin{enumerate}391 \item a simulation using392 \begin{itemize}393 \item memory injection (similar to CompCert)394 \item relation based around source and target's statements and continuations395 \end{itemize}396 \item syntactic cost labelling properties are preserved397 \begin{itemize}398 \item structural induction on function body399 \end{itemize}400 \end{enumerate}401 \end{frame}402 403 \section{Initialisation}404 \begin{frame}405 \frametitle{Cminor: initialization}406 407 Replace initialization data by code in the initial function.408 409 \begin{itemize}410 \item straightforward to define411 \item instantiate a slightly different version of the semantics for it412 \begin{itemize}413 \item Can't accidentally forget the pass414 \end{itemize}415 \end{itemize}416 417 \bigskip418 Correctness should follow because the state after the initialisation will419 be the same as the initial state of the original.420 \end{frame}421 422 \section{RTLabs}423 \begin{frame}[fragile]424 \frametitle{RTLabs: syntax and semantics}425 426 Register Transfer Language with frontend operations.427 428 Control flow graph implemented by generic identifiers map:429 430 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]431 definition label ≝ identifier LabelTag.432 definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag.433 434 inductive statement : Type[0] ≝435  St_skip : label $\rightarrow$ statement436  St_cost : costlabel $\rightarrow$ label $\rightarrow$ statement437  St_const : register $\rightarrow$ constant $\rightarrow$ label $\rightarrow$ statement438  St_op1 : $\forall$t,t'. unary_operation t' t $\rightarrow$ register439 $\rightarrow$ register $\rightarrow$ label $\rightarrow$ statement440 ...441 \end{lstlisting}442 \begin{itemize}443 \item Shares basic operations (including semantics) with Cminor.444 \item Tags prevent confusion of labels (graph vs.~goto vs.~cost).445 \end{itemize}446 447 Semantics are straightforward interpretation of statements.448 \end{frame}449 450 \begin{frame}[fragile]451 \frametitle{RTLabs: syntax and semantics}452 453 \begin{lstlisting}[language=matita]454 record internal_function : Type[0] ≝455 { f_labgen : universe LabelTag456 ; f_reggen : universe RegisterTag457 ...458 ; f_graph : graph statement459 ; f_closed : graph_closed f_graph460 ; f_typed : graph_typed (f_locals @ f_params) f_graph461 ...462 \end{lstlisting}463 464 Enforce that465 \begin{itemize}466 \item every statement's successor labels are present in the CFG467 \item every statement should be welltyped (for limited type system)468 \end{itemize}469 470 \end{frame}471 472 \section{Cminor to RTLabs}473 \begin{frame}474 \frametitle{Cminor to RTLabs}475 476 Break down statements and expressions into RTL graph.477 478 \begin{itemize}479 \item Incrementally build function backwards480 \item all state is in function record, like prototype481 \end{itemize}482 483 \bigskip484 May investigate whether a state monad makes invariant management easier.485 486 \bigskip487 Showing graph closure requires488 \begin{itemize}489 \item monotonicity of graph construction490 \item eventual insertion of all \lstinline'goto' destinations491 \end{itemize}492 493 Carry these along in the partially built function record.494 495 \end{frame}496 497 % \begin{frame}[fragile]498 % \frametitle{Cminor nesting depth}499 500 % Want to prevent501 % \begin{lstlisting}[language=C]502 % void f() {503 % block { loop { exit 5; } }504 % }505 % \end{lstlisting}506 507 % Index statements by block depth508 % \begin{lstlisting}[language=matita]509 % inductive stmt : $\forall$blockdepth:nat. Type[0] ≝510 %  St_skip : $\forall$n. stmt n511 % ...512 %  St_block : $\forall$n. stmt (S n) $\rightarrow$ stmt n513 %  St_exit : $\forall$n. Fin n $\rightarrow$ stmt n514 % ...515 % \end{lstlisting}516 517 % \begin{itemize}518 % \item In semantics index continuations too519 % \item Use \lstinline[language=matita]'Fin n' to make \lstinline'k_exit'520 % a total function521 % \end{itemize}522 523 % (May be able to remove entirely if we redo \lstinline[language=C]{switch}?)524 % \end{frame}525 526 \begin{frame}[fragile]527 \frametitle{Establishing RTLabs invariants}528 529 Use dependent pairs to show invariant along with results.530 531 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%]532 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)533 (Env:expr_vars ty e (present ?? env))534 (dst:register)535 (f:partial_fn le)536 on e: $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝537 538 match e return539 $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$540 $\Sigma$f':partial_fn le. fn_graph_included le f f' with541 [ ...542  Cst _ c $\Rightarrow$ $\lambda$_. %\guillemotleft%add_fresh_to_graph ? (St_const dst c) f ?, ?%\guillemotright%543 ...544 \end{lstlisting}545 546 Continually appeal to monotonicity (\lstinline'fn_graph_included'),547 use unification hints to simplify stepping back.548 549 \end{frame}550 551 \frame{552 \frametitle{Cminor to RTLabs: cost labels}553 554 Two of the cost label properties are easy to deal with, the third will require more555 work:556 \begin{enumerate}557 \item cost label at head of function558 \item cost label after branching instructions559 \item cost labels at the head of each loop / \lstinline'goto' destination560 \end{enumerate}561 562 No simple notion of the head of a loop or \lstinline'goto' any more.563 564 \medskip565 Instead will prove in \alert{Cminor} that after following a finite566 number of instructions we reach either567 \begin{itemize}568 \item a cost label, or569 \item the end of the function570 \end{itemize}571 572 }573 574 \section{Structured traces}575 \frame{576 \frametitle{RTLabs structured traces}577 578 Frontend only uses flat traces consisting of single steps.579 580 \bigskip581 The backend will need the function call structure and the labelling582 properties in order to show that the generated costs are correct.583 584 \begin{itemize}585 \item Traces are structured in sections from cost label to cost label,586 \item the entire execution of function calls nested as a single `step',587 \item a coinductive definition presents nonterminating traces, using the588 inductive definition for all terminating function calls589 \end{itemize}590 591 \bigskip592 RTLabs chosen because it is the first languages where statements:593 \begin{itemize}594 \item take one step each (modulo function calls)595 \item have individual `addresses'596 \end{itemize}597 }598 599 \frame{600 \frametitle{RTLabs structured traces}601 Have already established the existence of these traces602 \begin{itemize}603 \item termination decided classically604 \item syntactic labelling properties used to build the semantic structure605 \item show stack preservation to ensure that function calls \texttt{return}606 to the correct location607 \item tricky to establish guardedness of definitions608 \end{itemize}609 610 \bigskip611 Next, prove that flattening these traces yields the original.612 }613 614 \frame{615 \frametitle{Conclusion}616 617 The syntax, semantics and translations of the prototype compiler have618 been implemented in Matita.619 620 \bigskip621 We have already defined and established622 \begin{itemize}623 \item invariants regarding variables, typing and program structure624 \item a rich form of execution trace to pass to the backend625 \end{itemize}626 627 \medskip628 We have plans for629 \begin{itemize}630 \item showing functional correctness of the frontend631 \item proving that the cost labelling is appropriate, and is preserved632 \item using the above in the whole compiler functional and cost correctness results.633 \end{itemize}634 635 }636 637 636 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.