Changeset 381
 Timestamp:
 Dec 6, 2010, 5:17:40 PM (9 years ago)
 Location:
 Deliverables/D3.1/Report
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Report/report.bib
r197 r381 67 67 } 68 68 69 @misc{d2.1, 70 title = {Compiler design and intermediate languages}, 71 author = {Roberto M. Amadio and Nicolas Ayache and Yann R{\'{e}}gisGianas and Kayvan Memarian and Ronan Saillard}, 72 howpublished = {Deliverable 2.1, Project FP7ICT2009C243881 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 203 203 \end{picture} 204 204 \caption{The extended 8051 memory model} 205 \label{fig:memorymodel} 205 206 \end{figure} 206 207 … … 336 337 337 338 \subsection{Smallstep inductive semantics} 339 \label{sec:inductive} 338 340 339 341 The semantics for \clight{} itself has been ported from the Coq development … … 567 569 \lstinline'x' and evaluate \lstinlinee', and otherwise propogate the error. 568 570 571 \subsection{Statements} 572 573 Evaluating 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 575 handled by a resumption monad, which on encountering some I/O returns a 576 suspension. When the suspension is applied to a value the evaluation of the 577 semantics is resumed. Resumption monads are a standard tool for providing 578 denotational semantics for input~\cite{Moggi199155} and interleaved 579 concurrency~\cite[Chapter 12]{schmidt86}. 580 The definition also incorporates errors, and uses a coercion to automatically 581 transform values from the plain error monad. 582 \todo{should perhaps give more details of the resumption monad?} 583 584 The execution of assignments is straightforward, 585 \begin{quote} 586 \begin{lstlisting} 587 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))) ≝ 588 match 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} 599 where \lstinline'!' is used in place of \lstinline'do' due to the change in 600 monad. The content is essentially the same as the inductive rule given on 601 page~\pageref{page:Sassign}. 602 603 The handling of external calls uses the 604 \begin{quote} 605 \begin{lstlisting} 606 do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval 607 \end{lstlisting} 608 \end{quote} 609 function 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 627 Together with functions to provide the initial state for a program and to 628 detect a final state we can write a function to run the program up to a given 629 number of steps. Similarly, a corecursive function can return the entire 630 execution as a stream of trace and state pairs. 631 632 \section{Validation} 633 \label{sec:valid} 634 635 We have used two methods to validate our executable semantics: we have 636 proven them equivalent to the inductive semantics of 637 Section~\ref{sec:inductive}, and we have animated small examples of 638 key areas. 639 640 \subsection{Equivalence to inductive semantics} 641 642 To show that the executable semantics are sound with respect to the 643 inductive semantics we need to prove that any value produced by each 644 function satisfies the corresponding relation, modulo errors and 645 resumption. To deal with these monads we lift the properties 646 required. In particular, for the resumption monad we ignore error 647 values, require the property when a value is produced, and quantify 648 over any interaction with the outside world: 649 \begin{quote} 650 \begin{lstlisting} 651 nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop := 652 match 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} 659 We can use this lifting with the relations from the inductive 660 semantics to state soundness properties: 661 \begin{quote} 662 \begin{lstlisting} 663 ntheorem 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} 667 The proofs of these theorems use case analysis over the state, a few 668 lemmas to break up the expressions in the monad and the other 669 soundness results to form the corresponding derivation in the 670 inductive semantics. 671 672 We experimented with a different way of specifying soundness using 673 dependent types: 674 \begin{quote} 675 \begin{lstlisting} 676 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))) ≝ 677 \end{lstlisting} 678 \end{quote} 569 679 Note the $\Sigma$ type for the result of the function, which shows that 570 680 successful executions are sound with respect to the inductive semantics. … … 585 695 rule from the inductive semantics. 586 696 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} 697 However, the soundness proofs then pervade the executable semantics, 698 making the correctness proofs more difficult. We decided to keep the 699 soundness results separate, partly because of the increased difficulty 700 of using the resulting terms in proofs, and partly because they are of 701 little consequence once equivalence has been shown. 702 703 The completeness results requiring a dual lifting which requires the 704 term to reduce to a particular value, allowing for resumptions with 705 existential quantification: 706 \begin{quote} 707 \begin{lstlisting} 708 nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop := 709 match 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} 717 We then show the completeness theorems, such as 718 \begin{lstlisting} 719 ntheorem 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} 723 by case analysis on the inductive derivation and a mixture of 724 reduction and rewriting. 725 \todo{Whole execution equivalence} 726 727 \subsection{Animation of simple C programs} 656 728 657 729 \begin{verbatim}
Note: See TracChangeset
for help on using the changeset viewer.