Changeset 1773 for Deliverables

Timestamp:

Feb 27, 2012, 3:53:15 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

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

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -317 +317 @@
 
 \subsection{Graph translations}
+RTLabs and most intermediate languages in the back-end have a graph
+representation:
+the code of each function is represented by a graph of instructions.
+The graph maps a set of labels (the names of the nodes) to the instruction
+stored at that label (the nodes of the graph).
+Instructions reference zero or more additional labels that are the immediate
+successors of the instruction: zero for return from functions; more than one
+for conditional jumps and calls; one in all other cases. The references
+from one instruction to its immediates are the arcs of the graph.
+
+Status of graph languages always have a program counter that holds a
+representation of a reference to the current instruction.
+
+A translation between two consecutive graph languages maps each instruction
+stored at location $l$ in the first graph and with immediate successors
+$\{l_1,\ldots,l_n\}$ to a subgraph of the output graph that has a single
+entry point at location $l$ and exit arcs to $\{l_1,\ldots,l_n\}$. Moreover,
+the labels of all non entry nodes in the subgraph are distinct from all the
+labels in the source graph.
+
+In order to simplify the translations and the relative proofs of forward
+simulation, after the release of D4.2 and D4.3, we have provided:
+\begin{itemize}
+ \item a new data type (called \texttt{blist}) that represents a
+   sequence of instructions to be added to the output graph.
+   The ``b'' in the name stands for binder, since a \texttt{blist} is
+   either empty, an extension of a \texttt{blist} with an instruction
+   at the front, or the generation of a fresh quantity followed by a
+   \texttt{blist}. The latter feature is used, for instance, to generate
+   fresh register names. The instructions in the list are unlabelled and
+   all of them but the last one are also sequential, like in a linear program.
+ \item a new iterator (called \texttt{b\_graph\_translate}) of type
+\begin{displaymath}
+\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist})
+\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
+\end{displaymath}
+   The iterator transform the input graph in the output graph by replacing
+   each node with the graph that corresponds to the linear \texttt{blist}
+   obtained by applying the function in input to the node label.
+\end{itemize}
+
+Using the iterator above, the code can be written in such a way that
+the programmer does not see any distinction between writing a transformation
+on linear or graph languages.
+
+In order to prove simulations for translations obtained using the iterator,
+we will prove the following theorem:
+
+\begin{align*}
+\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
+& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
+&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (next \ l \ G_i)\ G_{\sigma}
+\end{align*}
+
+Here \texttt{subgraph} is a computational predicate that given a \texttt{blist}
+$[i_1, \ldots, i_n]$, an entry label $l$, an exit label $l'$ and a graph $G$
+expands to the fact that fetching from $G$ at address $l$ one retrieves a node
+$i_1$ with a successor $l_1$ that, when fetched, yields a node $i_2$ with a
+successor $l_2$ such that \ldots. The successor of $i_n$ is $l'$.
+
+Proving a forward simulation diagram of the following kind using the theorem
+above is now as simple as doing the same using standard small step operational
+semantics over linear languages.
+
+\begin{align*}
+\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
+&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
+&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
+&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
+\end{align*}
+
+Because of the fact that graph translation preserves entry and exit labels of
+translated statements, the state translation function $\sigma$ will simply
+preserve the value of the program counter. The program code, which is
+part of the state, is translated using the iterator.
+
+The proof is then roughly the following. Let $l$ be the program counter of the
+input state $s$. We proceed by cases on the current instruction of $s$.
+Let $[i_1, \ldots, i_n]$ be the \texttt{blist} associated to $l$ and $s$
+by the translation function. The witness required for the existential
+statement is simply $n$. By applying the theorem above we know that the
+next $n$ instructions that will be fetched from $s\ \sigma$ will be
+$[i_1, \ldots, i_n]$ and it is now sufficient to prove that they simulate
+the original instruction.
 
 \subsection{The RTLabs to RTL translation}
@@ -583 +667 @@
 \end{diagram}
 \end{displaymath}
-
-\subsection{The RTL to ERTL translation}
-\label{subsect.rtl.ertl.translation}
-
-\begin{displaymath}
-\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
-\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
-\end{displaymath}
-
-\begin{align*}
-\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
-& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
-&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
-\end{align*}
-
-\begin{align*}
-\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
-&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
-&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
-&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
-\end{align*}
 
 \begin{align*}