Changeset 1768


Ignore:
Timestamp:
Feb 27, 2012, 2:46:08 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1767 r1768  
    356356
    357357\begin{displaymath}
    358 \mathtt{BEMem} = \mathtt{Mem} \mathtt{BEValue}
     358\mathtt{BEMem} = \mathtt{Mem}~\mathtt{BEValue}
    359359\end{displaymath}
    360360
     
    391391\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
    392392\end{displaymath}
    393 That is, if we are successful in reading a value of size $s$ from memory at address $a$ in front-end memory, then we should successfully be able to read a value from memory in the back-end memory at \emph{any} address from address $a$ up to and including address $a + i$, where $i \leq s$.
     393That is, if we are successful in reading a value of size $s$ from memory at address $a$ in front-end memory, then we should successfully be able to read all of its chunks from memory in the back-end memory at appropriate address (from address $a$ up to and including address $a + i$, where $i \leq s$).
    394394
    395395Next, we must show that \texttt{store} properly commutes with the $\sigma$-map between memory spaces:
     
    399399That is, if we store a value \texttt{v} in the front-end memory \texttt{M} at address \texttt{a} and transform the resulting memory with $\sigma$, then this is equivalent to storing a transformed value $\mathtt{\sigma(v)}$ at address $\mathtt{\sigma(a)}$ into the back-end memory $\mathtt{\sigma(M)}$.
    400400
    401 Finally, we must prove that \texttt{load}, \texttt{store} and $\sigma$ all properly commute.
    402 Writing \texttt{load}$^*$ for multiple consecutive iterations of \texttt{load}, we must prove:
    403 \begin{displaymath}
    404 \texttt{load}^* (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
    405 \end{displaymath}
    406 That is, suppose we store a transformed value $\mathtt{\sigma(v)}$ into a back-end memory $\mathtt{\sigma(M)}$ at address $\mathtt{\sigma(a')}$, using \texttt{store}, and then load the correct number of bytes (for the size of $\mathtt{\sigma(v)}$ at address $\sigma(a)$.
    407 Then, this should be equivalent to loading the correct number of bytes from address $\sigma(a)$ in an unaltered version of $\mathtt{\sigma(M)}$, \emph{providing} that the memory regions occupied by the two sequences of bytes at the two addresses do not overlap.
    408 This will entail more proof obligations, demonstrating that the $\sigma$-map between memory spaces respects memory regions.
     401Finally, the commutation properties between \texttt{load} and \texttt{store} are weakened in the $\sigma$-image of the memory.
     402Writing \texttt{load}$^*$ for the multiple consecutive iterations of \texttt{load} used to fetch all chunks of a value, we must prove that, when $a \neq a'$:
     403\begin{displaymath}
     404\texttt{load}^* \sigma(a)\ (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M)) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
     405\end{displaymath}
     406That is, suppose we store a transformed value $\mathtt{\sigma(v)}$ into a back-end memory $\mathtt{\sigma(M)}$ at address $\mathtt{\sigma(a')}$, using \texttt{store}, and then load from the address $\sigma(a)$. Even if $a$ and $a'$ are
     407distinct by hypothesis, there is a priori no guarantee that the consecutive
     408bytes for the value stored at $\sigma(a)$ are disjoint from those for the
     409values stored at $\sigma(a')$. The fact that this holds is a non-trivial
     410property of $\sigma$ to be proved.
    409411
    410412RTLabs states come in three flavours:
     
    430432As a result, we have two stack pointers in our state: \texttt{ISP}, which is the real, hardware stack, and \texttt{SP}, which is the stack pointer of the emulated stack in memory.
    431433The emulated stack is used for pushing and popping stack frames when calling or returning from function calls, however this is done using the hardware stack, indexed by \texttt{ISP} as an intermediary.
    432 Instructions like \texttt{LCALL} and \texttt{ACALL} are hardwired by the processor's design to push on to the hardware stack, therefore after a call has been made, and after a call returns, the compiler emits code to move parameters and return addresses to-and-from the hardware stack.
     434Instructions like \texttt{LCALL} and \texttt{ACALL} are hardwired by the processor's design to push the return address on to the hardware stack. Therefore after a call has been made, and before a call returns, the compiler emits code to move the return address back and forth the two stacks. Parameters, return values
     435and local variables are only present in the external stack.
    433436As a result, for most of the execution of the processor, the hardware stack is empty, or contains a single item ready to be moved into external memory.
    434437
    435 Once more, we require a map from RTLabs states to RTL states.
    436 Call it $\sigma$:
     438Once more, we require a relation $\sigma$ between RTLabs states and RTL states.
     439Because $\sigma$ is one-to-many and, morally, a multi-function,
     440we use in the following the functional notation for $\sigma$, using $\star$
     441in the output of $\sigma$ to mean that any value is accepted.
    437442\begin{displaymath}
    438443\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
     
    442447For \texttt{State} we perform a further case analysis of the top stack frame, which decomposes into a tuple holding the current program counter value, the current stack pointer and the value of the registers:
    443448\begin{displaymath}
    444 \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{\langle PC, REGS, SP \rangle})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
    445 \end{displaymath}
    446 Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame, and setting all untranslated values to zero, their default value.
     449\sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{\langle PC, REGS, SP \rangle})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), \star, \star, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
     450\end{displaymath}
     451Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame. Any value for the internal stack pointer
     452and the carry bit is admitted.
    447453
    448454Translating \texttt{Call} and \texttt{Return} states is more involved, as a commutation between a single step of execution and the translation process must hold:
     
    456462
    457463Here \emph{return one step} and \emph{call one step} refer to a pair of commuting diagrams relating the one-step execution of a call and return state and translation of both.
    458 We provide the one step commuting diagrams in Figure~\ref{fig.commuting.diagrams}.
     464We provide the one step commuting diagrams in Figure~\ref{fig.commuting.diagrams}. The fact that one execution step in the source language is not performed
     465in the target language is not problematic for preservation of divergence
     466because it is easy to show that every step from a \texttt{Call} or
     467\texttt{Return} state is always preceeded/followed by one step that is always
     468simulated.
    459469
    460470\begin{figure}
     
    478488\end{figure}
    479489
    480 We now outline how states are executed:
     490The forward simulation proof for all steps that do not involve function
     491calls is trivial because $\sigma$ does not alter the memory or the
     492pseudo-registers. We outline here the invocation of functions and return
     493from a function.
     494
    481495\begin{displaymath}
    482496\begin{array}{rcl}
Note: See TracChangeset for help on using the changeset viewer.