# Changeset 1836 for Deliverables

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

Revise WP3 presentation.

File:
1 edited

### Legend:

Unmodified
 r1830 \textsf{Clight}\\ \> $\downarrow$ \> cast removal\\ \> $\downarrow$ \> add runtime functions\\ \> $\downarrow$ \> labelling\\ \> \gray{$\downarrow$} \> \gray{add runtime functions}\\ \> $\downarrow$ \> cost labelling\\ \> $\downarrow$ \> stack variable allocation and control structure simplification\\ \begin{itemize} \item Adding invariants \item Structured traces \end{itemize} \begin{itemize} \item Memory, global environments from before. \item Memory, global environments from D3.1 \item Bit vector based arithmetic from D4.1 \begin{itemize} \bigskip \bigskip {\Large \blue{Front end operations}} \bigskip \frame{ \frametitle{Clight: labelling} \frametitle{Clight: cost labelling} Adds cost labels to Clight program. % TODO: update! \begin{lstlisting}[language=matita] \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] inductive expr : typ $\rightarrow$ Type[0] ≝ | Id : $\forall$t. ident $\rightarrow$ expr t | Cst : $\forall$t. constant $\rightarrow$ expr t | Op1 : $\forall$t,t'. unary_operation $\rightarrow$ expr t $\rightarrow$ expr t' | Op1 : $\forall$t,t'. unary_operation t t' $\rightarrow$ expr t $\rightarrow$ expr t' | Op2 : $\forall$t1,t2,t'. binary_operation $\rightarrow$ expr t1 $\rightarrow$ expr t2 $\rightarrow$ expr t' | Mem : $\forall$t,r. memory_chunk $\rightarrow$ expr (ASTptr r) $\rightarrow$ expr t When using or creating function records we prove that we can switch between them: \begin{lstlisting}[language=matita] \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] lemma populates_env : $\forall$l,e,u,l',e',u'. distinct_env ?? l $\rightarrow$ (* distinct names in l *) populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ (* build register mapping *) $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ (* So anything in the environment... *) Env_has e' i t.  (* maps to something of the correct type *) distinct_env ?? l $\rightarrow$                    (* distinct names in l *) populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ (* build register mapping *) $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ (* Anything in the environment... *) Env_has e' i t. (* maps to something of the correct type *) \end{lstlisting} \begin{enumerate} \item All variables are in the parameters or locals lists\\ \quad with the correct type \quad --- with the correct type \item All \lstinline'goto' labels mentioned are defined in the body \end{enumerate} What is \lstinline'stmt_P'? How is \lstinline'stmt_P' defined? \end{frame} \frametitle{Invariants in Cminor} \begin{lstlisting}[language=matita] \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] let rec stmt_P (P:stmt $\rightarrow$ Prop) (s:stmt) on s : Prop ≝ match s with Higher order predicate \begin{itemize} \item When we do pattern matching on associated statement get to unfold predicate \item Pretty easy to do proof obligations for substatements \item When we pattern match on the statement the predicate can unfold \item Easy to discharge proof obligations for substatements \item similar definition for expressions \item not necessary for RTLabs \end{itemize} \item could separate out, have a nice Clight' language \end{itemize} Similarly, check variable environments are sane. Similarly, check variable environments are sane, check all \lstinline'goto' labels are translated. \end{frame} Control flow graph implemented by generic identifiers map: \begin{lstlisting}[language=matita] \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] definition label ≝ identifier LabelTag. definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag. ... \end{lstlisting} \begin{itemize} \item Shares basic operations (including semantics) with Cminor. Use dependent pairs to show invariant along with results. \begin{lstlisting}[language=matita,escapechar=\%] \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%] let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) \frametitle{Cminor to RTLabs: cost labels} Two of the cost label properties are easy to deal with, the third requires more Two of the cost label properties are easy to deal with, the third will require more work: \begin{enumerate} No simple notion of the head of a loop or \lstinline'goto' any more. \medskip Instead will prove in \alert{Cminor} that after following a finite number of instructions we reach either Front-end only uses flat traces consisting of single steps. \bigskip The back-end will need the function call structure and the labelling properties in order to show that the generated costs are correct. \item Traces are structured in sections from cost label to cost label, \item the entire execution of function calls nested as a single step', \item A coinductive definition presents non-terminating traces, using the \item a coinductive definition presents non-terminating traces, using the inductive definition for all terminating function calls \end{itemize} \bigskip RTLabs chosen because it is the first languages where statements: \begin{itemize} \item take one step each (modulo function calls) \item have individual `addresses' \end{itemize} } \frame{ \frametitle{RTLabs structured traces} Have already established the existence of these traces \begin{itemize} \item termination decided classically \item syntactic labelling properties used to build these semantic structure \item syntactic labelling properties used to build the semantic structure \item show stack preservation to ensure that function calls \texttt{return} to the correct location \item tricky to establish guardedness of definitions \end{itemize} \bigskip It remains to prove that flattening these traces yields the original. } been implemented in Matita. \bigskip We have already defined and established \begin{itemize} \end{itemize} \medskip We have plans for \begin{itemize}