Changeset 1752 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 24, 2012, 5:18:22 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (4 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -61 +61 @@
 
 In the last section we finally present an estimation of the effort required
-for the certification in Matita of the compiler.
+for the certification in Matita of the compiler and we draw conclusions.
 
 \section{Front-end: Clight to RTLabs}
@@ -321 +321 @@
 
 \begin{displaymath}
-\mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i
-\end{displaymath}
-
-In the front-end, we have both integer and float values, where integer values are `sized, along with null values and pointers.
-In the back-end memory model, floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
-However, the back-end memory model introduces an undefined value ($\bot$) and sized pointer values.
-
-We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
+\mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{null}_i \mid \mathtt{ptr}_i
+\end{displaymath}
+
+In the front-end, we have both integer and float values, where integer values are `sized', along with null values and pointers. Some frontenv values are
+representables in a byte, but some others require more bits.
+
+In the back-end model all values are meant to be represented in a single byte.
+Values can thefore be undefined, be one byte long integers or be indexed
+fragments of a pointer, null or not. Floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
+
+The $\sigma$ map implements a one-to-many relation: a single front-end value
+is mapped to a sequence of back-end values when its size is more then one byte.
+
+We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. Both kinds of memory can be
+thought as an instance of a generic \texttt{Mem} data type parameterized over
+the kind of values stored in memory.
 
 \begin{displaymath}
@@ -337 +345 @@
 
 \begin{displaymath}
-\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
+\mathtt{Block} ::= \mathtt{Region} \times \mathtt{ID}
 \end{displaymath}
 
@@ -356 +364 @@
 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)
-\put(-150,-20){\framebox(25,25)[c]{\texttt{v}}}
-\put(-125,-20){\framebox(25,25)[c]{\texttt{4}}}
-\put(-100,-20){\framebox(25,25)[c]{\texttt{cont}}}
-\put(-75,-20){\framebox(25,25)[c]{\texttt{cont}}}
-\put(-50,-20){\framebox(25,25)[c]{\texttt{cont}}}
-\put(-15,-10){\vector(1, 0){30}}
-\put(25,-20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}}
-\put(50,-20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}}
-\put(75,-20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}}
-\put(100,-20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}}
+\begin{picture}(0, 25)
+\put(-125,0){\framebox(25,25)[c]{\texttt{v,4}}}
+\put(-100,0){\framebox(25,25)[c]{\texttt{cont}}}
+\put(-75,0){\framebox(25,25)[c]{\texttt{cont}}}
+\put(-50,0){\framebox(25,25)[c]{\texttt{cont}}}
+\put(-15,10){\vector(1, 0){30}}
+\put(25,0){\framebox(25,25)[c]{\texttt{\texttt{v$_1$}}}}
+\put(50,0){\framebox(25,25)[c]{\texttt{\texttt{v$_2$}}}}
+\put(75,0){\framebox(25,25)[c]{\texttt{\texttt{v$_3$}}}}
+\put(100,0){\framebox(25,25)[c]{\texttt{\texttt{v$_4$}}}}
 \end{picture}
 \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.
+
 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: