Changeset 1752 for Deliverables


Ignore:
Timestamp:
Feb 24, 2012, 5:18:22 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1751 r1752  
    6161
    6262In the last section we finally present an estimation of the effort required
    63 for the certification in Matita of the compiler.
     63for the certification in Matita of the compiler and we draw conclusions.
    6464
    6565\section{Front-end: Clight to RTLabs}
     
    321321
    322322\begin{displaymath}
    323 \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
    324 \end{displaymath}
    325 
    326 In the front-end, we have both integer and float values, where integer values are `sized, along with null values and pointers.
    327 In the back-end memory model, floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
    328 However, the back-end memory model introduces an undefined value ($\bot$) and sized pointer values.
    329 
    330 We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
     323\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
     324\end{displaymath}
     325
     326In 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
     327representables in a byte, but some others require more bits.
     328
     329In the back-end model all values are meant to be represented in a single byte.
     330Values can thefore be undefined, be one byte long integers or be indexed
     331fragments of a pointer, null or not. Floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler.
     332
     333The $\sigma$ map implements a one-to-many relation: a single front-end value
     334is mapped to a sequence of back-end values when its size is more then one byte.
     335
     336We 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
     337thought as an instance of a generic \texttt{Mem} data type parameterized over
     338the kind of values stored in memory.
    331339
    332340\begin{displaymath}
     
    337345
    338346\begin{displaymath}
    339 \mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
     347\mathtt{Block} ::= \mathtt{Region} \times \mathtt{ID}
    340348\end{displaymath}
    341349
     
    356364In 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.
    357365In contrast, the layout of sized integer values in the back-end memory model consists of a series of byte-sized `chunks':
     366
    358367\begin{center}
    359 \begin{picture}(2, 2)
    360 \put(-150,-20){\framebox(25,25)[c]{\texttt{v}}}
    361 \put(-125,-20){\framebox(25,25)[c]{\texttt{4}}}
    362 \put(-100,-20){\framebox(25,25)[c]{\texttt{cont}}}
    363 \put(-75,-20){\framebox(25,25)[c]{\texttt{cont}}}
    364 \put(-50,-20){\framebox(25,25)[c]{\texttt{cont}}}
    365 \put(-15,-10){\vector(1, 0){30}}
    366 \put(25,-20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}}
    367 \put(50,-20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}}
    368 \put(75,-20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}}
    369 \put(100,-20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}}
     368\begin{picture}(0, 25)
     369\put(-125,0){\framebox(25,25)[c]{\texttt{v,4}}}
     370\put(-100,0){\framebox(25,25)[c]{\texttt{cont}}}
     371\put(-75,0){\framebox(25,25)[c]{\texttt{cont}}}
     372\put(-50,0){\framebox(25,25)[c]{\texttt{cont}}}
     373\put(-15,10){\vector(1, 0){30}}
     374\put(25,0){\framebox(25,25)[c]{\texttt{\texttt{v$_1$}}}}
     375\put(50,0){\framebox(25,25)[c]{\texttt{\texttt{v$_2$}}}}
     376\put(75,0){\framebox(25,25)[c]{\texttt{\texttt{v$_3$}}}}
     377\put(100,0){\framebox(25,25)[c]{\texttt{\texttt{v$_4$}}}}
    370378\end{picture}
    371379\end{center}
     380
     381Chunks for pointers are pairs made of the original pointer and the index of
     382the chunk. Therefore, when assembling the chunks together, we can always
     383recognize if all chunks refer to the same value or if the operation is
     384meaningless.
     385
    372386The 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.
    373387The first lemma required has the following statement:
Note: See TracChangeset for help on using the changeset viewer.