Changeset 1748 for Deliverables


Ignore:
Timestamp:
Feb 24, 2012, 4:53:07 PM (8 years ago)
Author:
mulligan
Message:

commit to avoid conflicts

File:
1 edited

Legend:

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

    r1747 r1748  
    270270\> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\
    271271\> $\downarrow$ \> instruction selection\\
     272\> $\downarrow$ \> change of memory models in compiler\\
    272273\textsf{RTL}\\
    273274\> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\
     
    292293\label{subsect.rtlabs.rtl.translation}
    293294
    294 % dpm: type system and casting load (???)
    295 We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:
     295The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project.
     296As a result, we require some method of translating between the values that the two memory models permit.
     297Suppose we have such a translation, $\sigma$.
     298Then the translation between values of the two memory models may be pictured with:
    296299
    297300\begin{displaymath}
     
    299302\end{displaymath}
    300303
     304In the front-end, we have both integer and float values, where integer values are `sized, along with null values and pointers.
     305In the back-end memory model, floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
     306However, the back-end memory model introduces an undefined value ($\bot$) and sized pointer values.
     307
    301308We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
    302309
     
    305312\end{displaymath}
    306313
    307 where
     314Here, \texttt{Block} consists of a \texttt{Region} paired with an identifier.
    308315
    309316\begin{displaymath}
     
    311318\end{displaymath}
    312319
    313 \begin{displaymath}
    314 \mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
    315 \end{displaymath}
     320We now have what we need for defining what is meant by the `memory' in the backend memory model.
     321Namely, we instantiate the previously defined \texttt{Mem} type with the type of back-end memory values.
     322
     323\begin{displaymath}
     324\mathtt{BEMem} = \mathtt{Mem} \mathtt{BEValue}
     325\end{displaymath}
     326
     327Memory addresses consist of a pair of back-end memory values:
    316328
    317329\begin{displaymath}
    318330\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
    319 \end{displaymath}
    320 
    321 \begin{displaymath}
    322 \mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
    323331\end{displaymath}
    324332
Note: See TracChangeset for help on using the changeset viewer.