Changeset 1751

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

Commit to avoid conflicts with Claudio

File:
1 edited

Legend:

Unmodified
 r1750 \end{displaymath} The back- and front-end memory models differ in how they represent sized integeer values in memory. In 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. In contrast, the layout of sized integer values in the back-end memory model consists of a series of byte-sized chunks': \begin{center} \begin{picture}(2, 2) \end{picture} \end{center} The 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. The first lemma required has the following statement: \begin{displaymath} \mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i \end{displaymath} 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$. \begin{displaymath}