Changeset 1836
 Timestamp:
 Mar 14, 2012, 12:02:08 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/Presentations/WP3.tex
r1830 r1836 105 105 \textsf{Clight}\\ 106 106 \> $\downarrow$ \> cast removal\\ 107 \> $\downarrow$ \> add runtime functions\\108 \> $\downarrow$ \> labelling\\107 \> \gray{$\downarrow$} \> \gray{add runtime functions}\\ 108 \> $\downarrow$ \> cost labelling\\ 109 109 \> $\downarrow$ \> stack variable allocation and control structure 110 110 simplification\\ … … 117 117 118 118 \begin{itemize} 119 \item Adding invariants119 \item Structured traces 120 120 \end{itemize} 121 121 … … 150 150 151 151 \begin{itemize} 152 \item Memory, global environments from before.152 \item Memory, global environments from D3.1 153 153 \item Bit vector based arithmetic from D4.1 154 154 \begin{itemize} … … 163 163 164 164 \bigskip 165 \bigskip166 {\Large \blue{Front end operations}}167 165 168 166 \bigskip … … 221 219 222 220 \frame{ 223 \frametitle{Clight: labelling}221 \frametitle{Clight: cost labelling} 224 222 225 223 Adds cost labels to Clight program. … … 275 273 276 274 % TODO: update! 277 \begin{lstlisting}[language=matita ]275 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 278 276 inductive expr : typ $\rightarrow$ Type[0] ≝ 279 277  Id : $\forall$t. ident $\rightarrow$ expr t 280 278  Cst : $\forall$t. constant $\rightarrow$ expr t 281  Op1 : $\forall$t,t'. unary_operation $\rightarrow$ expr t $\rightarrow$ expr t'279  Op1 : $\forall$t,t'. unary_operation t t' $\rightarrow$ expr t $\rightarrow$ expr t' 282 280  Op2 : $\forall$t1,t2,t'. binary_operation $\rightarrow$ expr t1 $\rightarrow$ expr t2 $\rightarrow$ expr t' 283 281  Mem : $\forall$t,r. memory_chunk $\rightarrow$ expr (ASTptr r) $\rightarrow$ expr t … … 326 324 When using or creating function records we prove that we can switch between 327 325 them: 328 \begin{lstlisting}[language=matita ]326 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 329 327 lemma populates_env : $\forall$l,e,u,l',e',u'. 330 distinct_env ?? l $\rightarrow$ (* distinct names in l *) 331 populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ 332 (* build register mapping *) 333 $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ 334 (* So anything in the environment... *) 335 Env_has e' i t. (* maps to something of the correct type *) 328 distinct_env ?? l $\rightarrow$ (* distinct names in l *) 329 populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ (* build register mapping *) 330 $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ (* Anything in the environment... *) 331 Env_has e' i t. 332 (* maps to something of the correct type *) 336 333 \end{lstlisting} 337 334 … … 358 355 \begin{enumerate} 359 356 \item All variables are in the parameters or locals lists\\ 360 \quad with the correct type357 \quad  with the correct type 361 358 \item All \lstinline'goto' labels mentioned are defined in the body 362 359 \end{enumerate} 363 360 364 What is \lstinline'stmt_P'?361 How is \lstinline'stmt_P' defined? 365 362 \end{frame} 366 363 … … 368 365 \frametitle{Invariants in Cminor} 369 366 370 \begin{lstlisting}[language=matita ]367 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 371 368 let rec stmt_P (P:stmt $\rightarrow$ Prop) (s:stmt) on s : Prop ≝ 372 369 match s with … … 383 380 Higher order predicate 384 381 \begin{itemize} 385 \item When we do pattern matching on associated statement get to unfold 386 predicate 387 \item Pretty easy to do proof obligations for substatements 382 \item When we pattern match on the statement the predicate can unfold 383 \item Easy to discharge proof obligations for substatements 388 384 \item similar definition for expressions 389 \item not necessary for RTLabs390 385 \end{itemize} 391 386 … … 411 406 \item could separate out, have a `nice Clight' language 412 407 \end{itemize} 413 Similarly, check variable environments are sane. 408 Similarly, check variable environments are sane, check all \lstinline'goto' 409 labels are translated. 414 410 \end{frame} 415 411 … … 458 454 Control flow graph implemented by generic identifiers map: 459 455 460 \begin{lstlisting}[language=matita ]456 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 461 457 definition label ≝ identifier LabelTag. 462 458 definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag. … … 470 466 ... 471 467 \end{lstlisting} 472 473 468 \begin{itemize} 474 469 \item Shares basic operations (including semantics) with Cminor. … … 560 555 Use dependent pairs to show invariant along with results. 561 556 562 \begin{lstlisting}[language=matita, escapechar=\%]557 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%] 563 558 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) 564 559 (Env:expr_vars ty e (present ?? env)) … … 583 578 \frametitle{Cminor to RTLabs: cost labels} 584 579 585 Two of the cost label properties are easy to deal with, the third requiresmore580 Two of the cost label properties are easy to deal with, the third will require more 586 581 work: 587 582 \begin{enumerate} … … 593 588 No simple notion of the head of a loop or \lstinline'goto' any more. 594 589 590 \medskip 595 591 Instead will prove in \alert{Cminor} that after following a finite 596 592 number of instructions we reach either … … 608 604 Frontend only uses flat traces consisting of single steps. 609 605 606 \bigskip 610 607 The backend will need the function call structure and the labelling 611 608 properties in order to show that the generated costs are correct. … … 614 611 \item Traces are structured in sections from cost label to cost label, 615 612 \item the entire execution of function calls nested as a single `step', 616 \item Acoinductive definition presents nonterminating traces, using the613 \item a coinductive definition presents nonterminating traces, using the 617 614 inductive definition for all terminating function calls 618 615 \end{itemize} 619 616 617 \bigskip 618 RTLabs chosen because it is the first languages where statements: 619 \begin{itemize} 620 \item take one step each (modulo function calls) 621 \item have individual `addresses' 622 \end{itemize} 623 } 624 625 \frame{ 626 \frametitle{RTLabs structured traces} 620 627 Have already established the existence of these traces 621 628 \begin{itemize} 622 629 \item termination decided classically 623 \item syntactic labelling properties used to build these semantic structure 630 \item syntactic labelling properties used to build the semantic structure 631 \item show stack preservation to ensure that function calls \texttt{return} 632 to the correct location 624 633 \item tricky to establish guardedness of definitions 625 634 \end{itemize} 635 636 \bigskip 637 It remains to prove that flattening these traces yields the original. 626 638 } 627 639 … … 655 667 been implemented in Matita. 656 668 669 \bigskip 657 670 We have already defined and established 658 671 \begin{itemize} … … 661 674 \end{itemize} 662 675 676 \medskip 663 677 We have plans for 664 678 \begin{itemize}
Note: See TracChangeset
for help on using the changeset viewer.