# Changeset 381 for Deliverables

Ignore:
Timestamp:
Dec 6, 2010, 5:17:40 PM (9 years ago)
Message:

Some d3.1 work.

Location:
Deliverables/D3.1/Report
Files:
3 edited

### Legend:

Unmodified
 r335 \end{picture} \caption{The extended 8051 memory model} \label{fig:memorymodel} \end{figure} \subsection{Small-step inductive semantics} \label{sec:inductive} The semantics for \clight{} itself has been ported from the Coq development \lstinline'x' and evaluate \lstinline-e'-, and otherwise propogate the error. \subsection{Statements} Evaluating a step of a statement is complicated by the presence of the external' functions for I/O, which can return arbitrary values.  These are handled by a resumption monad, which on encountering some I/O returns a suspension. When the suspension is applied to a value the evaluation of the semantics is resumed.  Resumption monads are a standard tool for providing denotational semantics for input~\cite{Moggi199155} and interleaved concurrency~\cite[Chapter 12]{schmidt86}. The definition also incorporates errors, and uses a coercion to automatically transform values from the plain error monad. \todo{should perhaps give more details of the resumption monad?} The execution of assignments is straightforward, \begin{quote} \begin{lstlisting} nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out ($\Sigma$r:trace $\times$ state. step ge st (\fst r) (\snd r))) ≝ match st with [ State f s k e m $\Rightarrow$ match s with [ Sassign a1 a2 $\Rightarrow$ Some ? ( ! $\langle$l,tr1$\rangle$ $\leftarrow$ exec_lvalue ge e m a1;: ! $\langle$v2,tr2$\rangle$ $\leftarrow$ exec_expr ge e m a2;: ! m' $\leftarrow$ store_value_of_type' (typeof a1) m l v2;: ret ? $\langle$tr1++tr2, State f Sskip k e m'$\rangle$) ... \end{lstlisting} \end{quote} where \lstinline'!' is used in place of \lstinline'do' due to the change in monad.  The content is essentially the same as the inductive rule given on page~\pageref{page:Sassign}. The handling of external calls uses the \begin{quote} \begin{lstlisting} do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval \end{lstlisting} \end{quote} function to suspend execution: \begin{quote} \begin{lstlisting} ... ] | Callstate f0 vargs k m $\Rightarrow$ match f0 with [ ... | External f argtys retty $\Rightarrow$ Some ? ( ! evargs $\leftarrow$ check_eventval_list vargs (typlist_of_typelist argtys);: ! evres $\leftarrow$ do_io f evargs;: ! vres $\leftarrow$ check_eventval evres (proj_sig_res (signature_of_type argtys rett ret ? $\langle$(Eextcall f evargs evres), Returnstate vres k m$\rangle$) ... \end{lstlisting} \end{quote} \todo{say something more about the rest?} Together with functions to provide the initial state for a program and to detect a final state we can write a function to run the program up to a given number of steps.  Similarly, a corecursive function can return the entire execution as a stream of trace and state pairs. \section{Validation} \label{sec:valid} We have used two methods to validate our executable semantics: we have proven them equivalent to the inductive semantics of Section~\ref{sec:inductive}, and we have animated small examples of key areas. \subsection{Equivalence to inductive semantics} To show that the executable semantics are sound with respect to the inductive semantics we need to prove that any value produced by each function satisfies the corresponding relation, modulo errors and resumption.  To deal with these monads we lift the properties required.  In particular, for the resumption monad we ignore error values, require the property when a value is produced, and quantify over any interaction with the outside world: \begin{quote} \begin{lstlisting} nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop := match v return $\lambda$_.Prop with [ Wrong $\Rightarrow$ True | Value z $\Rightarrow$ P z | Interact out k $\Rightarrow$ $\forall$v'.P_io O I A P (k v') ]. \end{lstlisting} \end{quote} We can use this lifting with the relations from the inductive semantics to state soundness properties: \begin{quote} \begin{lstlisting} ntheorem exec_step_sound: $\forall$ge,st. P_io ??? ($\lambda$r. step ge st (\fst r) (\snd r)) (exec_step ge st). \end{lstlisting} \end{quote} The proofs of these theorems use case analysis over the state, a few lemmas to break up the expressions in the monad and the other soundness results to form the corresponding derivation in the inductive semantics. We experimented with a different way of specifying soundness using dependent types: \begin{quote} \begin{lstlisting} nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out ($\Sigma$r:trace $\times$ state. step ge st (\fst r) (\snd r))) ≝ \end{lstlisting} \end{quote} Note the $\Sigma$ type for the result of the function, which shows that successful executions are sound with respect to the inductive semantics. rule from the inductive semantics. \subsection{Statements} Evaluating a step of a statement is complicated by the presence of the external' functions for I/O, which can return arbitrary values.  These are handled by a resumption monad, which on encountering some I/O returns a suspension. When the suspension is applied to a value the evaluation of the semantics is resumed.  Resumption monads are a standard tool for providing denotational semantics for input~\cite{Moggi199155} and interleaved concurrency~\cite{??}. The definition also incorporates errors, and uses a coercion to automatically transform values from the plain error monad. \todo{should perhaps give more details of the resumption monad?} The execution of assignments is straightforward, \begin{quote} \begin{lstlisting} nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out ($\Sigma$r:trace $\times$ state. step ge st (\fst r) (\snd r))) ≝ match st with [ State f s k e m $\Rightarrow$ match s with [ Sassign a1 a2 $\Rightarrow$ Some ? ( ! $\langle$l,tr1$\rangle$ $\leftarrow$ exec_lvalue ge e m a1;: ! $\langle$v2,tr2$\rangle$ $\leftarrow$ exec_expr ge e m a2;: ! m' $\leftarrow$ store_value_of_type' (typeof a1) m l v2;: ret ? $\langle$tr1++tr2, State f Sskip k e m'$\rangle$) ... \end{lstlisting} \end{quote} where \lstinline'!' is used in place of \lstinline'do' due to the change in monad.  The content is essentially the same as the inductive rule given on page~\pageref{page:Sassign}. The handling of external calls uses the \begin{quote} \begin{lstlisting} do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval \end{lstlisting} \end{quote} function to suspend execution: \begin{quote} \begin{lstlisting} ... ] | Callstate f0 vargs k m $\Rightarrow$ match f0 with [ ... | External f argtys retty $\Rightarrow$ Some ? ( ! evargs $\leftarrow$ check_eventval_list vargs (typlist_of_typelist argtys);: ! evres $\leftarrow$ do_io f evargs;: ! vres $\leftarrow$ check_eventval evres (proj_sig_res (signature_of_type argtys rett ret ? $\langle$(Eextcall f evargs evres), Returnstate vres k m$\rangle$) ... \end{lstlisting} \end{quote} \todo{say something more about the rest?} Together with functions to provide the initial state for a program and to detect a final state we can write a function to run the program up to a given number of steps.  Similarly, a corecursive function can return the entire execution as a stream of trace and state pairs. \todo{completeness?} \section{Validation} \label{sec:valid} \begin{verbatim} Animation of simple C programs. \end{verbatim} However, the soundness proofs then pervade the executable semantics, making the correctness proofs more difficult.  We decided to keep the soundness results separate, partly because of the increased difficulty of using the resulting terms in proofs, and partly because they are of little consequence once equivalence has been shown. The completeness results requiring a dual lifting which requires the term to reduce to a particular value, allowing for resumptions with existential quantification: \begin{quote} \begin{lstlisting} nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop := match a with [ Value v $\Rightarrow$ v' = v | Interact _ k $\Rightarrow$ $\exists$r.yieldsIObare A (k r) v' | _ $\Rightarrow$ False ]. \end{lstlisting} \end{quote} \begin{quote} We then show the completeness theorems, such as \begin{lstlisting} ntheorem step_complete: $\forall$ge,s,tr,s'. step ge s tr s' $\rightarrow$ yieldsIObare ? (exec_step ge s) $\langle$tr,s'$\rangle$. \end{lstlisting} \end{quote} by case analysis on the inductive derivation and a mixture of reduction and rewriting. \todo{Whole execution equivalence} \subsection{Animation of simple C programs} \begin{verbatim}