Changeset 1785


Ignore:
Timestamp:
Feb 27, 2012, 5:55:45 PM (7 years ago)
Author:
tranquil
Message:

finished ERTL to LTL sketch

File:
1 edited

Legend:

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

    r1781 r1785  
    1717\usepackage{wasysym}
    1818
    19 \newcolumntype{b}{@{}>{{}}}
    20 \newcolumntype{B}{@{}>{{}}c<{{}}@{}}
    21 \newcolumntype{h}[1]{@{\hspace{#1}}}
     19\newcolumntype{b}{\at{}>{{}}}
     20\newcolumntype{B}{\at{}>{{}}c<{{}}\at{}}
     21\newcolumntype{h}[1]{\at{\hspace{#1}}}
    2222\newcolumntype{L}{>{$}l<{$}}
    2323\newcolumntype{C}{>{$}c<{$}}
    2424\newcolumntype{R}{>{$}r<{$}}
    2525\newcolumntype{S}{>{$(}r<{)$}}
    26 \newcolumntype{n}{@{}}
     26\newcolumntype{n}{\at{}}
    2727
    2828\lstdefinelanguage{matita-ocaml}
     
    839839\declsf{Eliminable}
    840840\declsf{StatementSem}
     841Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$
     842and hardware ones with $\mathtt{hdwregister}$.
     843
    841844For the liveness analysis, we aim at a map
    842845$\ell \in \mathtt{label} \mapsto $ live registers at $\ell$.
     
    844847$$
    845848\begin{array}{lL>{(ex. $}L<{)$}}
    846 \Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}~id\mapsto \text{caller-save}
     849\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}
    847850\\
    848 \Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}~id\mapsto \text{parameters}
     851\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}
    849852\end{array}
    850853$$
    851854Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$
    852 is the type of sets of registers\footnote{More precisely, it is thethe lattice
     855is the type of sets of registers\footnote{More precisely, it is the lattice
    853856of pairs of sets of pseudo-registers and sets of hardware registers,
    854857with pointwise operations.}, we also have have the following
     
    856859$$
    857860\begin{array}{lL}
    858 \Eliminable_{LA}(\ell) & iff $s(\ell)$ has side-effects only on $r\notin LA(\ell)$
     861\Eliminable_{LA}(\ell) & iff executing $\ell$ has side-effects only on $r\notin LA(\ell)$
    859862\\&
    860 (ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset,
     863(ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset),
    861864  \mathtt{CALL}id\mapsto \text{never}$)
    862865\\
     
    864867  \begin{cases}
    865868    LA(\ell) &\text{if $\Eliminable_{LA}(\ell)$,}\\
    866     (LA(\ell)\setminus \Defined(s(\ell)))\cup \Used(s(\ell) &\text{otherwise}.
     869    (LA(\ell)\setminus \Defined(\ell))\cup \Used(\ell) &\text{otherwise}.
    867870  \end{cases}$
    868871\end{array}
     
    872875
    873876The equation on which we build the fixpoint is then
    874 $$\Liveafter(\ell) \doteq \bigcup_{\ell' >_1 \ell} \Livebefore_{\Liveafter}(\ell')$$
    875 where $\ell' >_1 \ell$ denotes that $\ell'$ is an immediate successor of $\ell$
     877$$\Liveafter(\ell) \doteq \bigcup_{\ell <_1 \ell'} \Livebefore_{\Liveafter}(\ell')$$
     878where $\ell <_1 \ell'$ denotes that $\ell'$ is an immediate successor of $\ell$
    876879in the graph. We do not require the fixpoint to be the least one, so the hypothesis
    877880on $\Liveafter$ that we require is
    878 $$\Liveafter(\ell) \supseteq \bigcup_{\ell' >_1 \ell} \Livebefore(\ell')$$
     881\begin{equation}
     882\label{eq:livefixpoint}
     883\Liveafter(\ell) \supseteq \bigcup_{\ell <_1 \ell'} \Livebefore(\ell')
     884\end{equation}
    879885(for shortness we drop the subscript from $\Livebefore$).
     886
     887\subsubsection{Colouring}
     888\declsf{Colour}
     889\newcommand{\at}{\mathrel{@}}
     890The aim of the liveness analysis is to define what properties we need
     891of the colouring function, which is a map (computed separately for each
     892internal function)
     893$$\Colour:\mathtt{register}\to\mathtt{hdwregister}+\mathtt{nat}$$
     894which identifies pseudoregisters with hardware ones if it is able to, otherwise
     895it spills them to the stack. We will just state what property we need from such
     896a map. First, we extend the definition to all types of registers by:
     897$$\begin{aligned}
     898   \Colour^+:\mathtt{hdwregister}+\mathtt{register} &\to \mathtt{hdwregister}+\mathtt{nat}\\
     899   r & \mapsto
     900\begin{cases}
     901  \Colour(r) &\text{if $r\in\mathtt{register}$,}\\
     902  r &\text{if $r\in\mathtt{hdwregister}$,}.
     903\end{cases}
     904  \end{aligned}$$
     905The other piece of information we compute for each function is a \emph{similarity}
     906relation, which is an equivalence relation on all kinds of registers which depends
     907on the point of the program. We write
     908$$x\sim y \at \ell$$
     909to state that registers $x$ and $y$ are similar at $\ell$. The formal definition
     910will be given next, but intuitively it means that those two registers \emph{must}
     911have the same value at $\ell$. The analysis that produces this information can be
     912coarse: in our case, we just set two different registers to be similar at $\ell$
     913if at $\ell$ itself there is a move instruction between the two.
     914
     915The property required of colouring is the following:
     916\begin{equation}
     917\label{eq:colourprop}
     918\forall \ell.\forall x,y. x,y\in \Liveafter(\ell)\Rightarrow
     919  \Colour^+(x)=\Colour^+(y) \Rightarrow x\sim y \at\ell.
     920\end{equation}
     921
     922We mark a certain colouring with a subscript if we want to specify in which
     923internal function it is taken.
     924\subsubsection{The translation}
     925For example:
     926$$\ell : r_1\leftarrow r_2+r_3 \mapsto \begin{cases}
     927                                 \varepsilon & \text{if $\Eliminable(\ell)$},\\
     928                                 \Colour(r_1) \leftarrow \Colour(r_2) + \Colour(r_3) & \text{otherwise}.
     929                                \end{cases}$$
     930where $\varepsilon$ is the empty block of instructions (i.e.\ a \texttt{GOTO}),
     931and $\Colour(r_1) \leftarrow \Colour(r_2) + \Colour(r_3)$ is a notation for a
     932block of instructions that take into account:
     933\begin{itemize}
     934 \item load and store ops on the stack if any colouring is in fact a spilling;
     935 \item using the accumulator to store intermediate values.
     936\end{itemize}
     937The overall effect is that if $T$ is an LTL state with $\ell(T)=\ell$
     938then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$.
     939
     940We skip over the details of correctly dealing with the stack and its size.
     941\subsubsection{The relation between ERTL and LTL states}
     942Given a state $S$ in ERTL, we abuse the notation by using $S$ as the underlying map
     943$$S : \mathtt{hdwregister}+\mathtt{register} \to \mathtt{Value}.$$
     944The program counter in $S$ is written as $\ell(S)$. At this point we can state
     945the property asked from similarity:
     946\begin{equation}
     947\label{eq:similprop}
     948\forall S,S'.S\to S' \Rightarrow \forall x,y.x\sim y \at \ell(S) \Rightarrow S'(x) = S'(y).
     949\end{equation}
     950
     951Next, we relate ERTL states with LTL ones. For a state $T$ in LTL we again
     952abuse the notation using $T$ as a map
     953$$T: \mathtt{hdwregister}+\mathtt{nat} \to \mathtt{Value}$$
     954which maps hardware registers and \emph{local stack offsets} to values (in particular,
     955$T$ as a map depends on the saved frames for computing the correct absolute
     956stack values).
     957
     958The relation existing between the states at the two sides of this translation step,
     959which depends on liveness and colouring, is
     960then defined as
     961$$S\mathrel\sigma T \iff \ldots \wedge \forall x. x\in \Livebefore(\ell(S))\Rightarrow T(\Colour^+(x)) = S(x).$$
     962The ellipsis stands for other straightforward preservation, among which the properties
     963$\ell(T) = \ell(S)$ and, inductively, the preservation of frames.
     964
     965\subsubsection{Proof of preservation}
     966We will prove the following proposition:
     967$$\forall S, T. S \mathrel\sigma T \Rightarrow S \to S' \Rightarrow \exists T'.T\to^+ T' \wedge S'\mathrel\sigma T'$$
     968(with appropriate cost-labelled trace preservation which we omit). We will call $S\mathrel \sigma T$
     969the inductive hypothsis, as it will be such in the complete proof by induction on the trace of the program.
     970As usual, this step be done by cases
     971on the statement at $\ell(S)$ and how it is translated. We carry out in some detail a single case, the one of
     972a binary operation on registers.
     973
     974Suppose that $\ell(S):r_1 \leftarrow r_2+r_3$, so that
     975$$S'(x)=\begin{cases}S(r_1)+S(r_2) &\text{if $x=r_1$,}\\S(x) &\text{otherwise.}\end{cases}$$
     976\paragraph*{Case $\Eliminable(\ell(S))$.}
     977By definition we have $r_1\notin \Liveafter(\ell(S))$, and the translation
     978of the operation yields a \texttt{GOTO}. We take $T'$ the immediate successor
     979of $T$.
     980
     981Now in order to prove $S'\mathrel\sigma T'$, take any
     982$$x\in\Livebefore(\ell(S'))\subseteq \Liveafter(\ell(S)) = \Livebefore(\ell(S))$$
     983where we have used property~\eqref{eq:livefixpoint} and the definition
     984of $\Livebefore$ when $\Eliminable(\ell(S))$. We get the following chain of equalities:
     985$$T'(\Colour^+(x))\stackrel 1=T(\Colour^+(x))\stackrel 2=S(x) \stackrel 3= S'(x)$$
     986where
     987\begin{enumerate}
     988 \item is because $T'$ has the same store as $T$,
     989 \item is by inductive hypothesis as $x\in\Livebefore(\ell(S))$,
     990 \item is because $x\neq r_1$, as $r_1\notin \Liveafter(\ell(S))\ni x$.
     991\end{enumerate}
     992\paragraph*{Case $\neg\Eliminable(\ell(S))$.}
     993We then have $r_1\in\Liveafter(\ell(S))$, and
     994$$\Livebefore(\ell(S))=(\Liveafter(\ell(S))\setminus\{r_1\})\cup\{r_2,r_3\}.$$
     995Moreover the statement is translated to $\Colour(r_1)\leftarrow\Colour(r_2)+\Colour(r_3)$,
     996and we take the $T'\leftarrow^+T$ such that $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_3))$ and
     997$T'(\Colour^+(x))=T(\Colour^+(x))$ for all $x$ with $\Colour^+(x)\neq\Colour(r_1)$.
     998
     999Take any $x\in\Livebefore(\ell(S'))\subseteq \Liveafter(\ell(S))$ (by property~\eqref{eq:livefixpoint}).
     1000
     1001If $\Colour^+(x)=\Colour(r_1)$, we have by property~\eqref{eq:colourprop}
     1002that $x\sim r_1\at \ell(S)$ (as both $r_1,x\in\Liveafter(\ell(S))$, so that
     1003$$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)$$
     1004where
     1005\begin{enumerate}
     1006 \item is by two uses of inductive hypothesis, as $r_2,r_3\in\Livebefore(\ell(S))$,
     1007 \item is by property~\eqref{eq:similprop}\footnote{Notice that in our particular implementation
     1008for this case of binary op $x\sim r_1\at\ell(S)$ implies $x=r_1$. But nothing prevents us from
     1009employing more fine euristics for similarity.}.
     1010\end{enumerate}
     1011
     1012If $\Colour^+(x)\neq\Colour(r_1)$ (so in particular $x\neq r_1$), then $x\in\Livebefore(\ell(S))$,
     1013so by inductive hypothesis we have
     1014$$T'(\Colour^+(x))=T(\Colour^+(x))=S(x)=S'(x).$$
     1015
    8801016\subsection{The LTL to LIN translation}
    8811017\label{subsect.ltl.lin.translation}
Note: See TracChangeset for help on using the changeset viewer.