Changeset 1773

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


1 edited


  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1772 r1773  
    318318\subsection{Graph translations}
     319RTLabs and most intermediate languages in the back-end have a graph
     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.
     329Status of graph languages always have a program counter that holds a
     330representation of a reference to the current instruction.
     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.
     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:
     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
     352\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist})
     353\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
     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.
     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.
     364In order to prove simulations for translations obtained using the iterator,
     365we will prove the following theorem:
     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}
     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'$.
     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.
     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
     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.
     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.
    320404\subsection{The RTLabs to RTL translation}
    586 \subsection{The RTL to ERTL translation}
    587 \label{subsect.rtl.ertl.translation}
    589 \begin{displaymath}
    590 \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
    591 \rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
    592 \end{displaymath}
    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*}
    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*}
Note: See TracChangeset for help on using the changeset viewer.