Changeset 1760


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

avoiding conflicts

File:
1 edited

Legend:

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

    r1758 r1760  
    383383\end{center}
    384384
    385 Chunks for pointers are pairs made of the original pointer and the index of
    386 the chunk. Therefore, when assembling the chunks together, we can always
    387 recognize if all chunks refer to the same value or if the operation is
    388 meaningless.
     385Chunks for pointers are pairs made of the original pointer and the index of the chunk.
     386Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless.
    389387
    390388The 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.
     
    395393That 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$.
    396394
    397 \begin{displaymath}
    398 \sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
    399 \end{displaymath}
    400 
    401 \begin{displaymath}
    402 \texttt{load}^* (\mathtt{store}\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
    403 \end{displaymath}
     395Next, we must show that \texttt{store} properly commutes with the $\sigma$-map between memory spaces:
     396\begin{displaymath}
     397\sigma(\mathtt{store}\ a\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(a)\ \sigma(M)
     398\end{displaymath}
     399That 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)}$.
     400
     401Finally, we must prove that \texttt{load}, \texttt{store} and $\sigma$ all properly commute.
     402Writing \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}
     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 the correct number of bytes (for the size of $\mathtt{\sigma(v)}$ at address $\sigma(a)$.
     407Then, 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.
     408This will entail more proof obligations, demonstrating that the $\sigma$-map between memory spaces respects memory regions.
    404409
    405410\begin{displaymath}
Note: See TracChangeset for help on using the changeset viewer.