Changeset 1370


Ignore:
Timestamp:
Oct 14, 2011, 10:56:50 AM (8 years ago)
Author:
campbell
Message:

D3.3: Added a subsection on the SmallstepExec?.ma definitions, plus a few related
comments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/Report/report.tex

    r1346 r1370  
    193193
    194194The semantics for many of the languages in the compiler share some core parts:
    195 the memory model, environments, runtime values, definitions of operations and
    196 a monad for encapsulating failure and I/O (using resumptions).  The executable
     195the memory model, environments, runtime values, definitions of operations,
     196a monad for encapsulating failure and I/O (using resumptions), and a common
     197abstraction for small-step executable semantics.  The executable
    197198memory model was ported from CompCert as part of the work on \textsf{Clight}
    198199and was reused for the front-end languages\footnote{However, it is likely that
    199 we will revise the memory model to make it better suited for describing the
    200 back-end of our compiler.}.  The failure and I/O monad was introduced in the
     200we will revise the memory model to make it better suited for describing
     201all of our compiler, not just the front-end.}.  The failure and I/O monad was introduced in the
    201202previous deliverable on \textsf{Clight}~\cite[\S4.2]{d3.1}.  In all of the
    202203languages except \textsf{Clight} we have a basic form of type, \lstinline'typ'
     
    259260A common semantics is given for these operations in the form of simple
    260261CIC functions on the operation and runtime values.
     262
     263\subsection{Presentation of small-step executable semantics}
     264\label{sec:smallstepexec}
     265
     266Each language's semantics is described by an instantiation of two records for
     267defining transition systems.  We already use these to animate the semantics of
     268the languages for testing, but they will also be used to state the simulation
     269properties we will prove in Tasks~3.4 and~4.4.
     270
     271First we describe suitable transition systems,
     272\begin{lstlisting}
     273  record trans_system (outty:Type[0]) (inty:outty $\rightarrow$ Type[0]) : Type[2] :=
     274  { global : Type[1]
     275  ; state  : global $\rightarrow$ Type[0]
     276  ; is_final : $\forall$g. state g $\rightarrow$ option int
     277  ; step : $\forall$g. state g $\rightarrow$ IO outty inty (trace$\times$(state g))
     278  }.
     279\end{lstlisting}
     280where we have some type of \lstinline'global' data that remains fixed
     281throughout evaluation (typically used for the global environment), a type for
     282states, a function to detect a final successful state and a step function
     283which can also return an error or request for I/O.  The type of states may
     284depend on the fixed data so that we will be able to add invariants asserting
     285that (for example) all the global variables referenced by the program state
     286exist.
     287
     288We also define a coinductive description of executions and a cofixpoint to
     289produce them.  The second record extends the transition system with
     290a type of programs and functions to initialise the transition system:
     291\begin{lstlisting}
     292  record fullexec (outty:Type[0]) (inty:outty $\rightarrow$ Type[0]) : Type[2] :=
     293  { program : Type[0]
     294  ; es1 :> trans_system outty inty
     295  ; make_global : program $\rightarrow$ global ?? es1
     296  ; make_initial_state : $\forall$p:program. res (state ?? es1 (make_global p))
     297  }.
     298\end{lstlisting}
     299Finally another function is given which uses them to produce a full execution
     300starting from the program alone.
    261301
    262302\section{\textsf{Clight} modifications}
     
    303343
    304344The definition of the semantics is routine: a functional definition of a
    305 single small step of the machine is given, reusing the memory model,
     345single small-step of the machine is given, reusing the memory model,
    306346environments, arithmetic and operations mentioned above.
    307347
     
    350390terms for the syntax of each language described above.
    351391
    352 A few common definitions were added for animating the small step semantics
    353 definitions for any of the front-end languages in \matita.  We then used a
    354 small selection of test cases to ensure basic functionality.  However, this is
    355 still a time consuming process, so more testing will carried out once the
    356 extraction of CIC terms to \ocaml{} programs is implemented in \matita.
     392A few common definitions were added for animating the small-step semantics
     393of any of the front-end languages in \matita{}, given a bound on
     394the number of steps to execute and any input required.  These use the
     395definitions described in Section~\ref{sec:smallstepexec} to perform the actual
     396execution.  We then used a small selection of test cases to ensure basic
     397functionality.  However, this is still a time consuming process, so more
     398testing will carried out once the extraction of CIC terms to \ocaml{} programs
     399is implemented in \matita.
    357400
    358401\section{Embedding invariants}
Note: See TracChangeset for help on using the changeset viewer.