Changeset 1760 for Deliverables/D1.2/CompilerProofOutline/outline.tex

Ignore:
Timestamp:
Feb 27, 2012, 11:01:16 AM (9 years ago)
Message:

avoiding conflicts

File:
1 edited

Legend:

Unmodified
 r1758 \end{center} Chunks for pointers are pairs made of the original pointer and the index of the chunk. Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless. Chunks for pointers are pairs made of the original pointer and the index of the chunk. Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless. 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. 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} \sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M) \end{displaymath} \begin{displaymath} \texttt{load}^* (\mathtt{store}\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M) \end{displaymath} Next, we must show that \texttt{store} properly commutes with the $\sigma$-map between memory spaces: \begin{displaymath} \sigma(\mathtt{store}\ a\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(a)\ \sigma(M) \end{displaymath} That 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)}$. Finally, we must prove that \texttt{load}, \texttt{store} and $\sigma$ all properly commute. Writing \texttt{load}$^*$ for multiple consecutive iterations of \texttt{load}, we must prove: \begin{displaymath} \texttt{load}^* (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M) \end{displaymath} 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)$. 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. This will entail more proof obligations, demonstrating that the $\sigma$-map between memory spaces respects memory regions. \begin{displaymath}