Changeset 381 for Deliverables


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

Some d3.1 work.

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

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/Report/report.bib

    r197 r381  
    6767}
    6868
     69@misc{d2.1,
     70title = {Compiler design and intermediate languages},
     71author = {Roberto M. Amadio and Nicolas Ayache and Yann R{\'{e}}gis-Gianas and Kayvan Memarian and Ronan Saillard},
     72howpublished = {Deliverable 2.1, Project FP7-ICT-2009-C-243881 CerCo},
     73}
     74
     75@book{schmidt86,
     76  title = "Denotational Semantics: A Methodology for Language Development",
     77  author = "David A. Schmidt",
     78  publisher = "Allyn and Bacon, Inc.",
     79  year = 1986
     80}
  • Deliverables/D3.1/Report/report.tex

    r335 r381  
    203203\end{picture}
    204204\caption{The extended 8051 memory model}
     205\label{fig:memorymodel}
    205206\end{figure}
    206207
     
    336337
    337338\subsection{Small-step inductive semantics}
     339\label{sec:inductive}
    338340
    339341The semantics for \clight{} itself has been ported from the Coq development
     
    567569\lstinline'x' and evaluate \lstinline-e'-, and otherwise propogate the error.
    568570
     571\subsection{Statements}
     572
     573Evaluating a step of a statement is complicated by the presence of the
     574`external' functions for I/O, which can return arbitrary values.  These are
     575handled by a resumption monad, which on encountering some I/O returns a
     576suspension. When the suspension is applied to a value the evaluation of the
     577semantics is resumed.  Resumption monads are a standard tool for providing
     578denotational semantics for input~\cite{Moggi199155} and interleaved
     579concurrency~\cite[Chapter 12]{schmidt86}.
     580The definition also incorporates errors, and uses a coercion to automatically
     581transform values from the plain error monad.
     582\todo{should perhaps give more details of the resumption monad?}
     583
     584The execution of assignments is straightforward,
     585\begin{quote}
     586\begin{lstlisting}
     587nlet 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))) ≝
     588match st with
     589[ State f s k e m $\Rightarrow$
     590  match s with
     591  [ Sassign a1 a2 $\Rightarrow$ Some ? (
     592    ! $\langle$l,tr1$\rangle$ $\leftarrow$ exec_lvalue ge e m a1;:
     593    ! $\langle$v2,tr2$\rangle$ $\leftarrow$ exec_expr ge e m a2;:
     594    ! m' $\leftarrow$ store_value_of_type' (typeof a1) m l v2;:
     595    ret ? $\langle$tr1++tr2, State f Sskip k e m'$\rangle$)
     596...
     597\end{lstlisting}
     598\end{quote}
     599where \lstinline'!' is used in place of \lstinline'do' due to the change in
     600monad.  The content is essentially the same as the inductive rule given on
     601page~\pageref{page:Sassign}.
     602
     603The handling of external calls uses the
     604\begin{quote}
     605\begin{lstlisting}
     606do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval
     607\end{lstlisting}
     608\end{quote}
     609function to suspend execution:
     610\begin{quote}
     611\begin{lstlisting}
     612...
     613  ]
     614| Callstate f0 vargs k m $\Rightarrow$
     615  match f0 with
     616  [ ...
     617  | External f argtys retty $\Rightarrow$ Some ? (
     618      ! evargs $\leftarrow$ check_eventval_list vargs (typlist_of_typelist argtys);:
     619      ! evres $\leftarrow$ do_io f evargs;:
     620      ! vres $\leftarrow$ check_eventval evres (proj_sig_res (signature_of_type argtys rett
     621      ret ? $\langle$(Eextcall f evargs evres), Returnstate vres k m$\rangle$)
     622...
     623\end{lstlisting}
     624\end{quote}
     625\todo{say something more about the rest?}
     626
     627Together with functions to provide the initial state for a program and to
     628detect a final state we can write a function to run the program up to a given
     629number of steps.  Similarly, a corecursive function can return the entire
     630execution as a stream of trace and state pairs.
     631
     632\section{Validation}
     633\label{sec:valid}
     634
     635We have used two methods to validate our executable semantics: we have
     636proven them equivalent to the inductive semantics of
     637Section~\ref{sec:inductive}, and we have animated small examples of
     638key areas.
     639
     640\subsection{Equivalence to inductive semantics}
     641
     642To show that the executable semantics are sound with respect to the
     643inductive semantics we need to prove that any value produced by each
     644function satisfies the corresponding relation, modulo errors and
     645resumption.  To deal with these monads we lift the properties
     646required.  In particular, for the resumption monad we ignore error
     647values, require the property when a value is produced, and quantify
     648over any interaction with the outside world:
     649\begin{quote}
     650\begin{lstlisting}
     651nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop :=
     652match v return $\lambda$_.Prop with
     653[ Wrong $\Rightarrow$ True
     654| Value z $\Rightarrow$ P z
     655| Interact out k $\Rightarrow$ $\forall$v'.P_io O I A P (k v')
     656].
     657\end{lstlisting}
     658\end{quote}
     659We can use this lifting with the relations from the inductive
     660semantics to state soundness properties:
     661\begin{quote}
     662\begin{lstlisting}
     663ntheorem exec_step_sound: $\forall$ge,st.
     664  P_io ??? ($\lambda$r. step ge st (\fst r) (\snd r)) (exec_step ge st).
     665\end{lstlisting}
     666\end{quote}
     667The proofs of these theorems use case analysis over the state, a few
     668lemmas to break up the expressions in the monad and the other
     669soundness results to form the corresponding derivation in the
     670inductive semantics.
     671
     672We experimented with a different way of specifying soundness using
     673dependent types:
     674\begin{quote}
     675\begin{lstlisting}
     676nlet 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))) ≝
     677\end{lstlisting}
     678\end{quote}
    569679Note the $\Sigma$ type for the result of the function, which shows that
    570680successful executions are sound with respect to the inductive semantics.
     
    585695rule from the inductive semantics.
    586696
    587 \subsection{Statements}
    588 
    589 Evaluating a step of a statement is complicated by the presence of the
    590 `external' functions for I/O, which can return arbitrary values.  These are
    591 handled by a resumption monad, which on encountering some I/O returns a
    592 suspension. When the suspension is applied to a value the evaluation of the
    593 semantics is resumed.  Resumption monads are a standard tool for providing
    594 denotational semantics for input~\cite{Moggi199155} and interleaved
    595 concurrency~\cite{??}.
    596 The definition also incorporates errors, and uses a coercion to automatically
    597 transform values from the plain error monad.
    598 \todo{should perhaps give more details of the resumption monad?}
    599 
    600 The execution of assignments is straightforward,
    601 \begin{quote}
    602 \begin{lstlisting}
    603 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))) ≝
    604 match st with
    605 [ State f s k e m $\Rightarrow$
    606   match s with
    607   [ Sassign a1 a2 $\Rightarrow$ Some ? (
    608     ! $\langle$l,tr1$\rangle$ $\leftarrow$ exec_lvalue ge e m a1;:
    609     ! $\langle$v2,tr2$\rangle$ $\leftarrow$ exec_expr ge e m a2;:
    610     ! m' $\leftarrow$ store_value_of_type' (typeof a1) m l v2;:
    611     ret ? $\langle$tr1++tr2, State f Sskip k e m'$\rangle$)
    612 ...
    613 \end{lstlisting}
    614 \end{quote}
    615 where \lstinline'!' is used in place of \lstinline'do' due to the change in
    616 monad.  The content is essentially the same as the inductive rule given on
    617 page~\pageref{page:Sassign}.
    618 
    619 The handling of external calls uses the
    620 \begin{quote}
    621 \begin{lstlisting}
    622 do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval
    623 \end{lstlisting}
    624 \end{quote}
    625 function to suspend execution:
    626 \begin{quote}
    627 \begin{lstlisting}
    628 ...
    629   ]
    630 | Callstate f0 vargs k m $\Rightarrow$
    631   match f0 with
    632   [ ...
    633   | External f argtys retty $\Rightarrow$ Some ? (
    634       ! evargs $\leftarrow$ check_eventval_list vargs (typlist_of_typelist argtys);:
    635       ! evres $\leftarrow$ do_io f evargs;:
    636       ! vres $\leftarrow$ check_eventval evres (proj_sig_res (signature_of_type argtys rett
    637       ret ? $\langle$(Eextcall f evargs evres), Returnstate vres k m$\rangle$)
    638 ...
    639 \end{lstlisting}
    640 \end{quote}
    641 \todo{say something more about the rest?}
    642 
    643 Together with functions to provide the initial state for a program and to
    644 detect a final state we can write a function to run the program up to a given
    645 number of steps.  Similarly, a corecursive function can return the entire
    646 execution as a stream of trace and state pairs.
    647 
    648 \todo{completeness?}
    649 
    650 \section{Validation}
    651 \label{sec:valid}
    652 
    653 \begin{verbatim}
    654 Animation of simple C programs.
    655 \end{verbatim}
     697However, the soundness proofs then pervade the executable semantics,
     698making the correctness proofs more difficult.  We decided to keep the
     699soundness results separate, partly because of the increased difficulty
     700of using the resulting terms in proofs, and partly because they are of
     701little consequence once equivalence has been shown.
     702
     703The completeness results requiring a dual lifting which requires the
     704term to reduce to a particular value, allowing for resumptions with
     705existential quantification:
     706\begin{quote}
     707\begin{lstlisting}
     708nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop :=
     709match a with
     710[ Value v $\Rightarrow$ v' = v
     711| Interact _ k $\Rightarrow$ $\exists$r.yieldsIObare A (k r) v'
     712| _ $\Rightarrow$ False
     713].
     714\end{lstlisting}
     715\end{quote}
     716\begin{quote}
     717We then show the completeness theorems, such as
     718\begin{lstlisting}
     719ntheorem step_complete: $\forall$ge,s,tr,s'.
     720  step ge s tr s' $\rightarrow$ yieldsIObare ? (exec_step ge s) $\langle$tr,s'$\rangle$.
     721\end{lstlisting}
     722\end{quote}
     723by case analysis on the inductive derivation and a mixture of
     724reduction and rewriting.
     725\todo{Whole execution equivalence}
     726
     727\subsection{Animation of simple C programs}
    656728
    657729\begin{verbatim}
Note: See TracChangeset for help on using the changeset viewer.