Changeset 1407 for Deliverables


Ignore:
Timestamp:
Oct 19, 2011, 11:17:21 AM (9 years ago)
Author:
mulligan
Message:

almost finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1406 r1407  
    300300\end{lstlisting}
    301301
     302The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register:
    302303\begin{lstlisting}
    303304record more_sem_params (p:params_): Type[1] :=
     
    320321}.
    321322\end{lstlisting}
    322 
    323 \begin{lstlisting}
    324 record sem_params: Type[1] :=
    325 {
    326   spp :> params_;
    327   more_sem_pars :> more_sem_params spp
    328 }.
    329 \end{lstlisting}
    330 
     323For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
     324Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
     325Here \texttt{framesT} is the type of stack frames.
     326
     327We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
    331328\begin{lstlisting}
    332329record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
    333330{
    334331  more_sparams1 :> more_sem_params p;
    335   fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals);
    336   fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address);
    337   result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p));
    338   init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1;
    339   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));
    340   pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)));
    341   fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val);
    342   set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1));
    343   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)))
     332  fetch_statement:
     333    genv … p → state (mk_sem_params … more_sparams1) →
     334    res (joint_statement (mk_sem_params … more_sparams1) globals);
     335  ...
     336  save_frame:
     337    address → nat → paramsT … p → call_args p → call_dest p →
     338    state (mk_sem_params … more_sparams1) →
     339    res (state (mk_sem_params … more_sparams1));
     340  pop_frame:
     341    genv globals p → state (mk_sem_params … more_sparams1) →
     342    res ((state (mk_sem_params … more_sparams1)));
     343  ...
     344  set_result:
     345    list val → state (mk_sem_params … more_sparams1) →
     346    res (state (mk_sem_params … more_sparams1));
     347  exec_extended:
     348    genv globals p → extend_statements (mk_sem_params … more_sparams1) →
     349    succ p → state (mk_sem_params … more_sparams1) →
     350    IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
    344351 }.
    345352\end{lstlisting}
    346 
     353Here, \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.
     354
     355We bundle \texttt{params} and \texttt{sem\_params} together into a single record.
     356This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language:
    347357\begin{lstlisting}
    348358record sem_params2 (globals: list ident): Type[1] :=
     
    352362}.
    353363\end{lstlisting}
    354 
     364\noindent
    355365The \texttt{state} record holds the current state of the interpreter:
    356366\begin{lstlisting}
     
    373383...
    374384\end{lstlisting}
    375 We examine the type of this function
     385We examine the type of this function.
     386Note 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.
     387Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}.
     388Further, the function returns a new state, updated by the single step of execution of the program.
     389Finally, 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.
    376390
    377391%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    385399Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.
    386400
     401A monad can be characterised by the following:
     402\begin{itemize}
     403\item
     404A data type, $M$.
     405For instance, the \texttt{option} type in O'Caml or Matita.
     406\item
     407A way to `inject' or `lift' pure values into this data type (usually called \texttt{return}).
     408We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad.
     409In our example, the `lifting' function for the \texttt{option} monad can be implemented as:
     410\begin{lstlisting}
     411let return x = Some x
     412\end{lstlisting}
     413\item
     414A way to `sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}.
     415Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$.
     416We can see that bind `unpacks' a monadic value, applies a function after unpacking, and `repacks' the new value in the monad.
     417In our example, the sequencing function for the \texttt{option} monad can be implemented as:
     418\begin{lstlisting}
     419let bind o f =
     420  match o with
     421    None -> None
     422    Some s -> f s
     423\end{lstlisting}
     424\item
     425A 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.
     426These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler.
     427\end{itemize}
    387428In the semantics of both front and backend intermediate languages, we make use of monads.
    388 In particular, we make use of two forms of monad:
    389 \begin{enumerate}
    390 \item
    391 An `error monad', which signals that a computation either has completed successfully, or returns with an error message.
    392 The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation.
    393 This monad is used extensively in the semantics to signal a state which cannot be recovered from.
    394 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
    395 \begin{lstlisting}
    396 XXX
    397 \end{lstlisting}
    398 \item
    399 An `IO' monad, signalling the emission or reading of data to some external location or memory address.
    400 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).
     429This monadic infrastructure is shared between the frontend and backend languages.
     430
     431In 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.
     432Here, the monad's sequencing operation ensures that emissions and reads are maintained in the correct order.
    401433Most functions in the intermediate language semantics fall into the IO monad.
    402 \end{enumerate}
    403 This monadic infrastructure is shared between the frontend and backend languages.
     434In particular, we have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type:
     435\begin{lstlisting}
     436definition eval_statement:
     437  ∀globals: list ident.∀p:sem_params2 globals.
     438    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
     439...
     440\end{lstlisting}
     441If we in the body of \texttt{eval\_statement}, we may also see how the monad sequences effects.
     442For instance, in the case for the \texttt{LOAD} statement, we have the following:
     443\begin{lstlisting}
     444definition eval_statement:
     445  ∀globals: list ident. ∀p:sem_params2 globals.
     446    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
     447  $\lambda$globals, p, ge, st.
     448  ...
     449  match s with
     450  | LOAD dst addrl addrh ⇒
     451    ! vaddrh $\leftarrow$ dph_retrieve … st addrh;
     452    ! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
     453    ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;
     454    ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     455    ! st $\leftarrow$ acca_store p … dst v st;
     456    ! st $\leftarrow$ next … l st ;
     457      ret ? $\langle$E0, st$\rangle$
     458\end{lstlisting}
     459Here, we employ a certain degree of syntactic sugaring.
     460The syntax
     461\begin{lstlisting}
     462  ...
     463! vaddrh $\leftarrow$ dph_retrieve … st addrh;
     464! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
     465  ...
     466\end{lstlisting}
     467is sugaring for the \texttt{IO} monad's binding operation.
     468We can expand this sugaring to the following much more verbose code:
     469\begin{lstlisting}
     470  ...
     471  bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl)
     472    ($\lambda$vaddrl. ...))
     473\end{lstlisting}
     474Note also that the function \texttt{ret} is implementing the `lifting', or return function of the \texttt{IO} monad.
     475
     476We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about.
     477In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic.
     478The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad.
    404479
    405480%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.