Changeset 3218


Ignore:
Timestamp:
Apr 30, 2013, 12:01:03 AM (4 years ago)
Author:
campbell
Message:

Text about Cminor to RTLabs.

File:
1 edited

Legend:

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

    r3216 r3218  
    822822\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}
    823823
    824 \subsection{Clight to Cminor}
     824\subsubsection{Clight to Cminor}
    825825
    826826This pass is the last one operating on the \textsf{Clight} language.
     
    851851discuss our implementation of memory injections, and then the simulation proof.
    852852
    853 \subparagraph{Memory injections.}
     853\paragraph{Memory injections.}
    854854
    855855Our memory injections are modelled after the work of Blazy \& Leroy.
     
    865865loads after writes were axiomatised, due to a lack of time.
    866866
    867 \subparagraph{Simulation proof.}
     867\paragraph{Simulation proof.}
    868868
    869869The correctness proof for this transformation was not completed. We proved the
     
    874874
    875875\todo{list cases, explain while loop, explain labeling problem}
     876
     877\subsubsection{Cminor to RTLabs}
     878
     879The translation from \textsf{Cminor} to \textsf{RTLabs} is a fairly
     880routine control flow graph (CFG) construction.  As such, we chose to
     881axiomatise its simulation results.  However, we did prove several
     882properties of the generated programs:
     883\begin{itemize}
     884\item All statements are type correct with respect to the declared
     885  pseudo-register type environment.
     886\item The CFG is closed, and has a distinguished entry node and a
     887  unique exit node.
     888\end{itemize}
     889
     890These properties rely on similar properties about type safety and the
     891presence of \lstinline[language=C]'goto'-labels for Cminor programs
     892which are checked at the preceding stage.  As a result, this
     893transformation is total and any compilation failures must occur when
     894the corresponding \textsf{Clight} source is available and a better
     895error message can be generated.
     896
     897The proof obligations for these properties include many instances of
     898graph inclusion.  We automated these proofs using a small amount of
     899reflection, making the obligations much easier to handle.  One
     900drawback to enforcing invariants thoroughly is that temporarily
     901breaking them can be awkward.  For example, \lstinline'return'
     902statements were originally used as placeholders for
     903\lstinline[language=C]'goto' destinations that had not yet been
     904translated.  However, this made establishing the single exit node
     905property rather difficult, and a different placeholder was chosen
     906instead.  In other circumstances it is possible to prove a more
     907complex invariant then simplify it at the end of the transformation.
    876908
    877909\section{Checking cost labelling properties}
Note: See TracChangeset for help on using the changeset viewer.