Changeset 1773


Ignore:
Timestamp:
Feb 27, 2012, 3:53:15 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1772 r1773  
    317317
    318318\subsection{Graph translations}
     319RTLabs and most intermediate languages in the back-end have a graph
     320representation:
     321the code of each function is represented by a graph of instructions.
     322The graph maps a set of labels (the names of the nodes) to the instruction
     323stored at that label (the nodes of the graph).
     324Instructions reference zero or more additional labels that are the immediate
     325successors of the instruction: zero for return from functions; more than one
     326for conditional jumps and calls; one in all other cases. The references
     327from one instruction to its immediates are the arcs of the graph.
     328
     329Status of graph languages always have a program counter that holds a
     330representation of a reference to the current instruction.
     331
     332A translation between two consecutive graph languages maps each instruction
     333stored at location $l$ in the first graph and with immediate successors
     334$\{l_1,\ldots,l_n\}$ to a subgraph of the output graph that has a single
     335entry point at location $l$ and exit arcs to $\{l_1,\ldots,l_n\}$. Moreover,
     336the labels of all non entry nodes in the subgraph are distinct from all the
     337labels in the source graph.
     338
     339In order to simplify the translations and the relative proofs of forward
     340simulation, after the release of D4.2 and D4.3, we have provided:
     341\begin{itemize}
     342 \item a new data type (called \texttt{blist}) that represents a
     343   sequence of instructions to be added to the output graph.
     344   The ``b'' in the name stands for binder, since a \texttt{blist} is
     345   either empty, an extension of a \texttt{blist} with an instruction
     346   at the front, or the generation of a fresh quantity followed by a
     347   \texttt{blist}. The latter feature is used, for instance, to generate
     348   fresh register names. The instructions in the list are unlabelled and
     349   all of them but the last one are also sequential, like in a linear program.
     350 \item a new iterator (called \texttt{b\_graph\_translate}) of type
     351\begin{displaymath}
     352\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist})
     353\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
     354\end{displaymath}
     355   The iterator transform the input graph in the output graph by replacing
     356   each node with the graph that corresponds to the linear \texttt{blist}
     357   obtained by applying the function in input to the node label.
     358\end{itemize}
     359
     360Using the iterator above, the code can be written in such a way that
     361the programmer does not see any distinction between writing a transformation
     362on linear or graph languages.
     363
     364In order to prove simulations for translations obtained using the iterator,
     365we will prove the following theorem:
     366
     367\begin{align*}
     368\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
     369& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
     370&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (next \ l \ G_i)\ G_{\sigma}
     371\end{align*}
     372
     373Here \texttt{subgraph} is a computational predicate that given a \texttt{blist}
     374$[i_1, \ldots, i_n]$, an entry label $l$, an exit label $l'$ and a graph $G$
     375expands to the fact that fetching from $G$ at address $l$ one retrieves a node
     376$i_1$ with a successor $l_1$ that, when fetched, yields a node $i_2$ with a
     377successor $l_2$ such that \ldots. The successor of $i_n$ is $l'$.
     378
     379Proving a forward simulation diagram of the following kind using the theorem
     380above is now as simple as doing the same using standard small step operational
     381semantics over linear languages.
     382
     383\begin{align*}
     384\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
     385&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
     386&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
     387&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
     388\end{align*}
     389
     390Because of the fact that graph translation preserves entry and exit labels of
     391translated statements, the state translation function $\sigma$ will simply
     392preserve the value of the program counter. The program code, which is
     393part of the state, is translated using the iterator.
     394
     395The proof is then roughly the following. Let $l$ be the program counter of the
     396input state $s$. We proceed by cases on the current instruction of $s$.
     397Let $[i_1, \ldots, i_n]$ be the \texttt{blist} associated to $l$ and $s$
     398by the translation function. The witness required for the existential
     399statement is simply $n$. By applying the theorem above we know that the
     400next $n$ instructions that will be fetched from $s\ \sigma$ will be
     401$[i_1, \ldots, i_n]$ and it is now sufficient to prove that they simulate
     402the original instruction.
    319403
    320404\subsection{The RTLabs to RTL translation}
     
    583667\end{diagram}
    584668\end{displaymath}
    585 
    586 \subsection{The RTL to ERTL translation}
    587 \label{subsect.rtl.ertl.translation}
    588 
    589 \begin{displaymath}
    590 \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
    591 \rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
    592 \end{displaymath}
    593 
    594 \begin{align*}
    595 \mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
    596 & \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
    597 &       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
    598 \end{align*}
    599 
    600 \begin{align*}
    601 \mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
    602 &       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
    603 &       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
    604 &       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
    605 \end{align*}
    606669
    607670\begin{align*}
Note: See TracChangeset for help on using the changeset viewer.