Changeset 3227


Ignore:
Timestamp:
Apr 30, 2013, 1:20:53 PM (4 years ago)
Author:
campbell
Message:

Last bits about lifting proof in 3.4.

File:
1 edited

Legend:

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

    r3226 r3227  
    674674have an initial state in the simulation relation with the original
    675675program's initial state.
     676
     677The back-end has similar requirements for lifting simulations to
     678structured traces.  Fortunately, our treatment of calls and returns
     679can be slightly simpler because we have special call and return states
     680that correspond to function entry and return that are separate from
     681the actual instructions.  This was originally inherited from our port
     682of CompCert's \textsf{Clight} semantics, but proves useful here
     683because we only need to consider adding extra steps \emph{after} a
     684call or return state, because the instruction step deals with extra
     685steps that occur before.  The back-end makes all of the call and
     686return machinery explicit, and thus needs more complex statements
     687about extra steps before and after each call and return.
    676688
    677689\begin{figure}
     
    738750shorter trace.
    739751
    740 This then gives us an overall result for any simulation fitting the
     752Combining the lemmas about the prefix and the measurable subtrace
     753requires a little care because the states joining the two might not be
     754in the simulation relation.  In particular, if the measurable subtrace
     755starts from the cost label at the beginning of the function there may
     756be some extra instructions in the target code to execute to complete
     757function entry before the states are back in the relation.  Hence we
     758carefully phrased the lemmas to allow for these extra steps.
     759
     760Together, these then gives us an overall result for any simulation fitting the
    741761requirements above (contained in the \lstinline'meas_sim' record):
    742762\begin{lstlisting}[language=matita]
     
    753773is a consequence of the preservation of observables, because it is
    754774determined by the functions called and returned from, which are observable.
    755 
    756 TODO: how to deal with untidy edges wrt to sim rel; anything to
    757 say about obs?
    758 
    759 TODO: cost labels are
    760 statements/exprs in these languages; split call/return gives simpler
    761 simulations
    762775
    763776\subsection{Simulation results for each pass}
Note: See TracChangeset for help on using the changeset viewer.