Changeset 1793


Ignore:
Timestamp:
Feb 28, 2012, 5:57:46 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1792 r1793  
    577577\begin{displaymath}
    578578\begin{diagram}
    579 s & \rTo^{\text{one step of execution}} & s'   \\
     579s & \rTo^1 & s'   \\
    580580  & \rdTo                             & \dTo \\
    581581  &                                   & \llbracket s'' \rrbracket
     
    583583\end{displaymath}
    584584
    585 \begin{displaymath}
    586 \begin{diagram}
    587 s & \rTo^{\text{one step of execution}} & s'   \\
    588   & \rdTo                             & \dTo \\
    589   &                                   & \llbracket s'' \rrbracket
    590 \end{diagram}
    591 \end{displaymath}
    592 \caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations}
     585\caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations.}
    593586\label{fig.commuting.diagrams}
    594587\end{figure}
     
    719712
    720713To summarize, the forward simulation diagrams for function call/return
    721 XXX
    722 
    723 Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases.
    724 Starting from any \texttt{Return} or \texttt{Call} state, translating and then executing a single step must be the same as executing exactly two steps and then translating, with the intermediate state obtained by executing once also being translatable to the final state.
    725 This is exemplified by the following diagram:
     714have the following form where the triangle is the one given in
     715Figure~\ref{fig.commuting.diagrams}, the next instruction to be
     716executed in state $s$ is either a function call or return and the intermediate
     717state $s'$ is either a \texttt{Call} or a \texttt{Return} state.
    726718\begin{displaymath}
    727719\begin{diagram}
     
    731723\end{diagram}
    732724\end{displaymath}
     725Two steps of execution are simulated by a single step.
    733726
    734727\subsection{The RTL to ERTL translation}
Note: See TracChangeset for help on using the changeset viewer.