Changeset 1751


Ignore:
Timestamp:
Feb 24, 2012, 5:09:03 PM (7 years ago)
Author:
mulligan
Message:

Commit to avoid conflicts with Claudio

File:
1 edited

Legend:

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

    r1750 r1751  
    353353\end{displaymath}
    354354
     355The back- and front-end memory models differ in how they represent sized integeer values in memory.
     356In particular, the front-end stores integer values as a header, with size information, followed by a string of `continuation' blocks, marking out the full representation of the value in memory.
     357In contrast, the layout of sized integer values in the back-end memory model consists of a series of byte-sized `chunks':
    355358\begin{center}
    356359\begin{picture}(2, 2)
     
    367370\end{picture}
    368371\end{center}
    369 
     372The differing memory representations of values in the two memory models imply the need for a series of lemmas on the actions of \texttt{load} and \texttt{store} to ensure correctness.
     373The first lemma required has the following statement:
    370374\begin{displaymath}
    371375\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
    372376\end{displaymath}
     377That 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$.
    373378
    374379\begin{displaymath}
Note: See TracChangeset for help on using the changeset viewer.