Changeset 1785 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 27, 2012, 5:55:45 PM (8 years ago)

Author:

tranquil

Message:

finished ERTL to LTL sketch

File:

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

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -17 +17 @@
 \usepackage{wasysym}
 
-\newcolumntype{b}{@{}>{{}}}
-\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
-\newcolumntype{h}[1]{@{\hspace{#1}}}
+\newcolumntype{b}{\at{}>{{}}}
+\newcolumntype{B}{\at{}>{{}}c<{{}}\at{}}
+\newcolumntype{h}[1]{\at{\hspace{#1}}}
 \newcolumntype{L}{>{$}l<{$}}
 \newcolumntype{C}{>{$}c<{$}}
 \newcolumntype{R}{>{$}r<{$}}
 \newcolumntype{S}{>{$(}r<{)$}}
-\newcolumntype{n}{@{}}
+\newcolumntype{n}{\at{}}
 
 \lstdefinelanguage{matita-ocaml}
@@ -839 +839 @@
 \declsf{Eliminable}
 \declsf{StatementSem}
+Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$
+and hardware ones with $\mathtt{hdwregister}$.
+
 For the liveness analysis, we aim at a map
 $\ell \in \mathtt{label} \mapsto $ live registers at $\ell$.
@@ -844 +847 @@
 $$
 \begin{array}{lL>{(ex. $}L<{)$}}
-\Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}~id\mapsto \text{caller-save}
+\Defined(\ell) & registers defined at $\ell$ & \ell:r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \ell:\mathtt{CALL}~id\mapsto \text{caller-save}
 \\
-\Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}~id\mapsto \text{parameters}
+\Used(\ell) & registers used at $\ell$ & \ell:r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \ell:\mathtt{CALL}~id\mapsto \text{parameters}
 \end{array}
 $$
 Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$
-is the type of sets of registers\footnote{More precisely, it is thethe lattice
+is the type of sets of registers\footnote{More precisely, it is the lattice
 of pairs of sets of pseudo-registers and sets of hardware registers,
 with pointwise operations.}, we also have have the following
@@ -856 +859 @@
 $$
 \begin{array}{lL}
-\Eliminable_{LA}(\ell) & iff $s(\ell)$ has side-effects only on $r\notin LA(\ell)$
+\Eliminable_{LA}(\ell) & iff executing $\ell$ has side-effects only on $r\notin LA(\ell)$
 \\&
-(ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset,
+(ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset),
   \mathtt{CALL}id\mapsto \text{never}$)
 \\
@@ -864 +867 @@
   \begin{cases}
     LA(\ell) &\text{if $\Eliminable_{LA}(\ell)$,}\\
-    (LA(\ell)\setminus \Defined(s(\ell)))\cup \Used(s(\ell) &\text{otherwise}.
+    (LA(\ell)\setminus \Defined(\ell))\cup \Used(\ell) &\text{otherwise}.
   \end{cases}$
 \end{array}
@@ -872 +875 @@
 
 The equation on which we build the fixpoint is then
-$$\Liveafter(\ell) \doteq \bigcup_{\ell' >_1 \ell} \Livebefore_{\Liveafter}(\ell')$$
-where $\ell' >_1 \ell$ denotes that $\ell'$ is an immediate successor of $\ell$
+$$\Liveafter(\ell) \doteq \bigcup_{\ell <_1 \ell'} \Livebefore_{\Liveafter}(\ell')$$
+where $\ell <_1 \ell'$ denotes that $\ell'$ is an immediate successor of $\ell$
 in the graph. We do not require the fixpoint to be the least one, so the hypothesis
 on $\Liveafter$ that we require is
-$$\Liveafter(\ell) \supseteq \bigcup_{\ell' >_1 \ell} \Livebefore(\ell')$$
+\begin{equation}
+\label{eq:livefixpoint}
+\Liveafter(\ell) \supseteq \bigcup_{\ell <_1 \ell'} \Livebefore(\ell')
+\end{equation}
 (for shortness we drop the subscript from $\Livebefore$).
+
+\subsubsection{Colouring}
+\declsf{Colour}
+\newcommand{\at}{\mathrel{@}}
+The aim of the liveness analysis is to define what properties we need
+of the colouring function, which is a map (computed separately for each
+internal function)
+$$\Colour:\mathtt{register}\to\mathtt{hdwregister}+\mathtt{nat}$$
+which identifies pseudoregisters with hardware ones if it is able to, otherwise
+it spills them to the stack. We will just state what property we need from such
+a map. First, we extend the definition to all types of registers by:
+$$\begin{aligned}
+   \Colour^+:\mathtt{hdwregister}+\mathtt{register} &\to \mathtt{hdwregister}+\mathtt{nat}\\
+   r & \mapsto
+\begin{cases}
+  \Colour(r) &\text{if $r\in\mathtt{register}$,}\\
+  r &\text{if $r\in\mathtt{hdwregister}$,}.
+\end{cases}
+  \end{aligned}$$
+The other piece of information we compute for each function is a \emph{similarity}
+relation, which is an equivalence relation on all kinds of registers which depends
+on the point of the program. We write
+$$x\sim y \at \ell$$
+to state that registers $x$ and $y$ are similar at $\ell$. The formal definition
+will be given next, but intuitively it means that those two registers \emph{must}
+have the same value at $\ell$. The analysis that produces this information can be
+coarse: in our case, we just set two different registers to be similar at $\ell$
+if at $\ell$ itself there is a move instruction between the two.
+
+The property required of colouring is the following:
+\begin{equation}
+\label{eq:colourprop}
+\forall \ell.\forall x,y. x,y\in \Liveafter(\ell)\Rightarrow
+  \Colour^+(x)=\Colour^+(y) \Rightarrow x\sim y \at\ell.
+\end{equation}
+
+We mark a certain colouring with a subscript if we want to specify in which
+internal function it is taken.
+\subsubsection{The translation}
+For example:
+$$\ell : r_1\leftarrow r_2+r_3 \mapsto \begin{cases}
+                                 \varepsilon & \text{if $\Eliminable(\ell)$},\\
+                                 \Colour(r_1) \leftarrow \Colour(r_2) + \Colour(r_3) & \text{otherwise}.
+                                \end{cases}$$
+where $\varepsilon$ is the empty block of instructions (i.e.\ a \texttt{GOTO}),
+and $\Colour(r_1) \leftarrow \Colour(r_2) + \Colour(r_3)$ is a notation for a
+block of instructions that take into account:
+\begin{itemize}
+ \item load and store ops on the stack if any colouring is in fact a spilling;
+ \item using the accumulator to store intermediate values.
+\end{itemize}
+The overall effect is that if $T$ is an LTL state with $\ell(T)=\ell$
+then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$.
+
+We skip over the details of correctly dealing with the stack and its size.
+\subsubsection{The relation between ERTL and LTL states}
+Given a state $S$ in ERTL, we abuse the notation by using $S$ as the underlying map
+$$S : \mathtt{hdwregister}+\mathtt{register} \to \mathtt{Value}.$$
+The program counter in $S$ is written as $\ell(S)$. At this point we can state
+the property asked from similarity:
+\begin{equation}
+\label{eq:similprop}
+\forall S,S'.S\to S' \Rightarrow \forall x,y.x\sim y \at \ell(S) \Rightarrow S'(x) = S'(y).
+\end{equation}
+
+Next, we relate ERTL states with LTL ones. For a state $T$ in LTL we again
+abuse the notation using $T$ as a map
+$$T: \mathtt{hdwregister}+\mathtt{nat} \to \mathtt{Value}$$
+which maps hardware registers and \emph{local stack offsets} to values (in particular,
+$T$ as a map depends on the saved frames for computing the correct absolute
+stack values).
+
+The relation existing between the states at the two sides of this translation step,
+which depends on liveness and colouring, is
+then defined as
+$$S\mathrel\sigma T \iff \ldots \wedge \forall x. x\in \Livebefore(\ell(S))\Rightarrow T(\Colour^+(x)) = S(x).$$
+The ellipsis stands for other straightforward preservation, among which the properties
+$\ell(T) = \ell(S)$ and, inductively, the preservation of frames.
+
+\subsubsection{Proof of preservation}
+We will prove the following proposition:
+$$\forall S, T. S \mathrel\sigma T \Rightarrow S \to S' \Rightarrow \exists T'.T\to^+ T' \wedge S'\mathrel\sigma T'$$
+(with appropriate cost-labelled trace preservation which we omit). We will call $S\mathrel \sigma T$
+the inductive hypothsis, as it will be such in the complete proof by induction on the trace of the program.
+As usual, this step be done by cases
+on the statement at $\ell(S)$ and how it is translated. We carry out in some detail a single case, the one of
+a binary operation on registers.
+
+Suppose that $\ell(S):r_1 \leftarrow r_2+r_3$, so that
+$$S'(x)=\begin{cases}S(r_1)+S(r_2) &\text{if $x=r_1$,}\\S(x) &\text{otherwise.}\end{cases}$$
+\paragraph*{Case $\Eliminable(\ell(S))$.}
+By definition we have $r_1\notin \Liveafter(\ell(S))$, and the translation
+of the operation yields a \texttt{GOTO}. We take $T'$ the immediate successor
+of $T$.
+
+Now in order to prove $S'\mathrel\sigma T'$, take any
+$$x\in\Livebefore(\ell(S'))\subseteq \Liveafter(\ell(S)) = \Livebefore(\ell(S))$$
+where we have used property~\eqref{eq:livefixpoint} and the definition
+of $\Livebefore$ when $\Eliminable(\ell(S))$. We get the following chain of equalities:
+$$T'(\Colour^+(x))\stackrel 1=T(\Colour^+(x))\stackrel 2=S(x) \stackrel 3= S'(x)$$
+where
+\begin{enumerate}
+ \item is because $T'$ has the same store as $T$,
+ \item is by inductive hypothesis as $x\in\Livebefore(\ell(S))$,
+ \item is because $x\neq r_1$, as $r_1\notin \Liveafter(\ell(S))\ni x$.
+\end{enumerate}
+\paragraph*{Case $\neg\Eliminable(\ell(S))$.}
+We then have $r_1\in\Liveafter(\ell(S))$, and
+$$\Livebefore(\ell(S))=(\Liveafter(\ell(S))\setminus\{r_1\})\cup\{r_2,r_3\}.$$
+Moreover the statement is translated to $\Colour(r_1)\leftarrow\Colour(r_2)+\Colour(r_3)$,
+and we take the $T'\leftarrow^+T$ such that $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_3))$ and
+$T'(\Colour^+(x))=T(\Colour^+(x))$ for all $x$ with $\Colour^+(x)\neq\Colour(r_1)$.
+
+Take any $x\in\Livebefore(\ell(S'))\subseteq \Liveafter(\ell(S))$ (by property~\eqref{eq:livefixpoint}).
+
+If $\Colour^+(x)=\Colour(r_1)$, we have by property~\eqref{eq:colourprop}
+that $x\sim r_1\at \ell(S)$ (as both $r_1,x\in\Liveafter(\ell(S))$, so that
+$$T'(\Colour^+(x))=T(\Colour(r_2))+T(\Colour(r_3))\stackrel 1=S(r_2)+S(r_3)=S'(r_1)\stackrel 2=S(x)$$
+where
+\begin{enumerate}
+ \item is by two uses of inductive hypothesis, as $r_2,r_3\in\Livebefore(\ell(S))$,
+ \item is by property~\eqref{eq:similprop}\footnote{Notice that in our particular implementation
+for this case of binary op $x\sim r_1\at\ell(S)$ implies $x=r_1$. But nothing prevents us from
+employing more fine euristics for similarity.}.
+\end{enumerate}
+
+If $\Colour^+(x)\neq\Colour(r_1)$ (so in particular $x\neq r_1$), then $x\in\Livebefore(\ell(S))$,
+so by inductive hypothesis we have
+$$T'(\Colour^+(x))=T(\Colour^+(x))=S(x)=S'(x).$$
+
 \subsection{The LTL to LIN translation}
 \label{subsect.ltl.lin.translation}