Changeset 1836


Ignore:
Timestamp:
Mar 14, 2012, 12:02:08 PM (8 years ago)
Author:
campbell
Message:

Revise WP3 presentation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP3.tex

    r1830 r1836  
    105105\textsf{Clight}\\
    106106\> $\downarrow$ \> cast removal\\
    107 \> $\downarrow$ \> add runtime functions\\
    108 \> $\downarrow$ \> labelling\\
     107\> \gray{$\downarrow$} \> \gray{add runtime functions}\\
     108\> $\downarrow$ \> cost labelling\\
    109109\> $\downarrow$ \> stack variable allocation and control structure
    110110 simplification\\
     
    117117
    118118\begin{itemize}
    119 \item Adding invariants
     119\item Structured traces
    120120\end{itemize}
    121121
     
    150150
    151151\begin{itemize}
    152 \item Memory, global environments from before.
     152\item Memory, global environments from D3.1
    153153\item Bit vector based arithmetic from D4.1
    154154  \begin{itemize}
     
    163163
    164164\bigskip
    165 \bigskip
    166 {\Large \blue{Front end operations}}
    167165
    168166\bigskip
     
    221219
    222220\frame{
    223 \frametitle{Clight: labelling}
     221\frametitle{Clight: cost labelling}
    224222
    225223Adds cost labels to Clight program.
     
    275273
    276274% TODO: update!
    277 \begin{lstlisting}[language=matita]
     275\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    278276inductive expr : typ $\rightarrow$ Type[0] ≝
    279277| Id : $\forall$t. ident $\rightarrow$ expr t
    280278| 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'
    282280| Op2 : $\forall$t1,t2,t'. binary_operation $\rightarrow$ expr t1 $\rightarrow$ expr t2 $\rightarrow$ expr t'
    283281| Mem : $\forall$t,r. memory_chunk $\rightarrow$ expr (ASTptr r) $\rightarrow$ expr t
     
    326324When using or creating function records we prove that we can switch between
    327325them:
    328 \begin{lstlisting}[language=matita]
     326\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    329327lemma 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 *)
    336333\end{lstlisting}
    337334
     
    358355\begin{enumerate}
    359356\item All variables are in the parameters or locals lists\\
    360 \quad with the correct type
     357\quad --- with the correct type
    361358\item All \lstinline'goto' labels mentioned are defined in the body
    362359\end{enumerate}
    363360
    364 What is \lstinline'stmt_P'?
     361How is \lstinline'stmt_P' defined?
    365362\end{frame}
    366363
     
    368365\frametitle{Invariants in Cminor}
    369366
    370 \begin{lstlisting}[language=matita]
     367\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    371368let rec stmt_P (P:stmt $\rightarrow$ Prop) (s:stmt) on s : Prop ≝
    372369match s with
     
    383380Higher order predicate
    384381\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
    388384\item similar definition for expressions
    389 \item not necessary for RTLabs
    390385\end{itemize}
    391386
     
    411406\item could separate out, have a `nice Clight' language
    412407\end{itemize}
    413 Similarly, check variable environments are sane.
     408Similarly, check variable environments are sane, check all \lstinline'goto'
     409labels are translated.
    414410\end{frame}
    415411
     
    458454Control flow graph implemented by generic identifiers map:
    459455
    460 \begin{lstlisting}[language=matita]
     456\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    461457definition label ≝ identifier LabelTag.
    462458definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag.
     
    470466...
    471467\end{lstlisting}
    472 
    473468\begin{itemize}
    474469\item Shares basic operations (including semantics) with Cminor.
     
    560555Use dependent pairs to show invariant along with results.
    561556
    562 \begin{lstlisting}[language=matita,escapechar=\%]
     557\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%]
    563558let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
    564559   (Env:expr_vars ty e (present ?? env))
     
    583578\frametitle{Cminor to RTLabs: cost labels}
    584579
    585 Two of the cost label properties are easy to deal with, the third requires more
     580Two of the cost label properties are easy to deal with, the third will require more
    586581work:
    587582\begin{enumerate}
     
    593588No simple notion of the head of a loop or \lstinline'goto' any more.
    594589
     590\medskip
    595591Instead will prove in \alert{Cminor} that after following a finite
    596592number of instructions we reach either
     
    608604Front-end only uses flat traces consisting of single steps.
    609605
     606\bigskip
    610607The back-end will need the function call structure and the labelling
    611608properties in order to show that the generated costs are correct.
     
    614611\item Traces are structured in sections from cost label to cost label,
    615612\item the entire execution of function calls nested as a single `step',
    616 \item A coinductive definition presents non-terminating traces, using the
     613\item a coinductive definition presents non-terminating traces, using the
    617614  inductive definition for all terminating function calls
    618615\end{itemize}
    619616
     617\bigskip
     618RTLabs 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}
    620627Have already established the existence of these traces
    621628\begin{itemize}
    622629\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
    624633\item tricky to establish guardedness of definitions
    625634\end{itemize}
     635
     636\bigskip
     637It remains to prove that flattening these traces yields the original.
    626638}
    627639
     
    655667been implemented in Matita.
    656668
     669\bigskip
    657670We have already defined and established
    658671\begin{itemize}
     
    661674\end{itemize}
    662675
     676\medskip
    663677We have plans for
    664678\begin{itemize}
Note: See TracChangeset for help on using the changeset viewer.