Changeset 1407 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

Oct 19, 2011, 11:17:21 AM (9 years ago)

Author:

mulligan

Message:

almost finished

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (5 diffs)

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -300 +300 @@
 \end{lstlisting}
 
+The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register:
 \begin{lstlisting}
 record more_sem_params (p:params_): Type[1] :=
@@ -320 +321 @@
 }.
 \end{lstlisting}
-
-\begin{lstlisting}
-record sem_params: Type[1] :=
-{
-  spp :> params_;
-  more_sem_pars :> more_sem_params spp
-}.
-\end{lstlisting}
-
+For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
+Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
+Here \texttt{framesT} is the type of stack frames.
+
+We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
 \begin{lstlisting}
 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
 {
   more_sparams1 :> more_sem_params p;
-  fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals);
-  fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address);
-  result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p));
-  init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1;
-  save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1));
-  pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)));
-  fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val);
-  set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1));
-  exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
+  fetch_statement:
+    genv … p → state (mk_sem_params … more_sparams1) →
+    res (joint_statement (mk_sem_params … more_sparams1) globals);
+  ...
+  save_frame:
+    address → nat → paramsT … p → call_args p → call_dest p →
+    state (mk_sem_params … more_sparams1) →
+    res (state (mk_sem_params … more_sparams1));
+  pop_frame:
+    genv globals p → state (mk_sem_params … more_sparams1) →
+    res ((state (mk_sem_params … more_sparams1)));
+  ...
+  set_result:
+    list val → state (mk_sem_params … more_sparams1) →
+    res (state (mk_sem_params … more_sparams1));
+  exec_extended:
+    genv globals p → extend_statements (mk_sem_params … more_sparams1) →
+    succ p → state (mk_sem_params … more_sparams1) →
+    IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
  }.
 \end{lstlisting}
-
+Here, \texttt{fetch\_statement} fetches the next statement to be executed, \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames, \texttt{set\_result} saves the result of the function computation, and \texttt{exec\_extended} is a function that executes the extended statements, peculiar to each individual intermediate language.
+
+We bundle \texttt{params} and \texttt{sem\_params} together into a single record.
+This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language:
 \begin{lstlisting}
 record sem_params2 (globals: list ident): Type[1] :=
@@ -352 +362 @@
 }.
 \end{lstlisting}
-
+\noindent
 The \texttt{state} record holds the current state of the interpreter:
 \begin{lstlisting}
@@ -373 +383 @@
 ...
 \end{lstlisting}
-We examine the type of this function
+We examine the type of this function.
+Note that it returns a monadic action, \texttt{IO}, denoting that it may have an IO \emph{side effect}, where the program reads or writes to some external device or memory address.
+Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}.
+Further, the function returns a new state, updated by the single step of execution of the program.
+Finally, a \emph{trace} is also returned, which records the trace of cost labels that the program passes through, in order to calculate the cost model for the CerCo compiler.
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
@@ -385 +399 @@
 Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.
 
+A monad can be characterised by the following:
+\begin{itemize}
+\item
+A data type, $M$.
+For instance, the \texttt{option} type in O'Caml or Matita.
+\item
+A way to `inject' or `lift' pure values into this data type (usually called \texttt{return}).
+We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad.
+In our example, the `lifting' function for the \texttt{option} monad can be implemented as:
+\begin{lstlisting}
+let return x = Some x
+\end{lstlisting}
+\item
+A way to `sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}.
+Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$.
+We can see that bind `unpacks' a monadic value, applies a function after unpacking, and `repacks' the new value in the monad.
+In our example, the sequencing function for the \texttt{option} monad can be implemented as:
+\begin{lstlisting}
+let bind o f =
+  match o with
+    None -> None
+    Some s -> f s
+\end{lstlisting}
+\item
+A series of algebraic laws that relate \texttt{return} and \texttt{bind}, ensuring that the sequencing operation `does the right thing' by retaining the order of effects.
+These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler.
+\end{itemize}
 In the semantics of both front and backend intermediate languages, we make use of monads.
-In particular, we make use of two forms of monad:
-\begin{enumerate}
-\item
-An `error monad', which signals that a computation either has completed successfully, or returns with an error message.
-The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation.
-This monad is used extensively in the semantics to signal a state which cannot be recovered from.
-For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
-\begin{lstlisting}
-XXX
-\end{lstlisting}
-\item
-An `IO' monad, signalling the emission or reading of data to some external location or memory address.
-Here, the monads sequencing operation ensures that emissions and reads are maintained in the correct order (i.e. it maintains a `trace', or ordered sequence of IO events).
+This monadic infrastructure is shared between the frontend and backend languages.
+
+In particular, an `IO' monad, signalling the emission or reading of data to some external location or memory address, is heavily used in the semantics of the intermediate languages.
+Here, the monad's sequencing operation ensures that emissions and reads are maintained in the correct order.
 Most functions in the intermediate language semantics fall into the IO monad.
-\end{enumerate}
-This monadic infrastructure is shared between the frontend and backend languages.
+In particular, we have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type:
+\begin{lstlisting}
+definition eval_statement:
+  ∀globals: list ident.∀p:sem_params2 globals.
+    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
+...
+\end{lstlisting}
+If we in the body of \texttt{eval\_statement}, we may also see how the monad sequences effects.
+For instance, in the case for the \texttt{LOAD} statement, we have the following:
+\begin{lstlisting}
+definition eval_statement:
+  ∀globals: list ident. ∀p:sem_params2 globals.
+    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
+  $\lambda$globals, p, ge, st.
+  ...
+  match s with
+  | LOAD dst addrl addrh ⇒
+    ! vaddrh $\leftarrow$ dph_retrieve … st addrh;
+    ! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
+    ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;
+    ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
+    ! st $\leftarrow$ acca_store p … dst v st;
+    ! st $\leftarrow$ next … l st ;
+      ret ? $\langle$E0, st$\rangle$
+\end{lstlisting}
+Here, we employ a certain degree of syntactic sugaring.
+The syntax
+\begin{lstlisting}
+  ...
+! vaddrh $\leftarrow$ dph_retrieve … st addrh;
+! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
+  ...
+\end{lstlisting}
+is sugaring for the \texttt{IO} monad's binding operation.
+We can expand this sugaring to the following much more verbose code:
+\begin{lstlisting}
+  ...
+  bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl)
+    ($\lambda$vaddrl. ...))
+\end{lstlisting}
+Note also that the function \texttt{ret} is implementing the `lifting', or return function of the \texttt{IO} monad.
+
+We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about.
+In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic.
+The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad.
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%