Changeset 1760 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 27, 2012, 11:01:16 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1758 r1760 383 383 \end{center} 384 384 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. 385 Chunks for pointers are pairs made of the original pointer and the index of the chunk. 386 Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless. 389 387 390 388 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. … … 395 393 That is, if we are successful in reading a value of size $s$ from memory at address $a$ in frontend memory, then we should successfully be able to read a value from memory in the backend memory at \emph{any} address from address $a$ up to and including address $a + i$, where $i \leq s$. 396 394 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} 395 Next, 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} 399 That is, if we store a value \texttt{v} in the frontend 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 backend memory $\mathtt{\sigma(M)}$. 400 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 backend 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. 404 409 405 410 \begin{displaymath}
Note: See TracChangeset
for help on using the changeset viewer.