Changeset 1785 for Deliverables/D1.2/CompilerProofOutline
- Timestamp:
- Feb 27, 2012, 5:55:45 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1781 r1785 17 17 \usepackage{wasysym} 18 18 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}}} 22 22 \newcolumntype{L}{>{$}l<{$}} 23 23 \newcolumntype{C}{>{$}c<{$}} 24 24 \newcolumntype{R}{>{$}r<{$}} 25 25 \newcolumntype{S}{>{$(}r<{)$}} 26 \newcolumntype{n}{ @{}}26 \newcolumntype{n}{\at{}} 27 27 28 28 \lstdefinelanguage{matita-ocaml} … … 839 839 \declsf{Eliminable} 840 840 \declsf{StatementSem} 841 Throughout this section, we denote pseudoregisters with the type $\mathtt{register}$ 842 and hardware ones with $\mathtt{hdwregister}$. 843 841 844 For the liveness analysis, we aim at a map 842 845 $\ell \in \mathtt{label} \mapsto $ live registers at $\ell$. … … 844 847 $$ 845 848 \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} 847 850 \\ 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} 849 852 \end{array} 850 853 $$ 851 854 Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$ 852 is the type of sets of registers\footnote{More precisely, it is the thelattice855 is the type of sets of registers\footnote{More precisely, it is the lattice 853 856 of pairs of sets of pseudo-registers and sets of hardware registers, 854 857 with pointwise operations.}, we also have have the following … … 856 859 $$ 857 860 \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)$ 859 862 \\& 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), 861 864 \mathtt{CALL}id\mapsto \text{never}$) 862 865 \\ … … 864 867 \begin{cases} 865 868 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}. 867 870 \end{cases}$ 868 871 \end{array} … … 872 875 873 876 The 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')$$ 878 where $\ell <_1 \ell'$ denotes that $\ell'$ is an immediate successor of $\ell$ 876 879 in the graph. We do not require the fixpoint to be the least one, so the hypothesis 877 880 on $\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} 879 885 (for shortness we drop the subscript from $\Livebefore$). 886 887 \subsubsection{Colouring} 888 \declsf{Colour} 889 \newcommand{\at}{\mathrel{@}} 890 The aim of the liveness analysis is to define what properties we need 891 of the colouring function, which is a map (computed separately for each 892 internal function) 893 $$\Colour:\mathtt{register}\to\mathtt{hdwregister}+\mathtt{nat}$$ 894 which identifies pseudoregisters with hardware ones if it is able to, otherwise 895 it spills them to the stack. We will just state what property we need from such 896 a 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}$$ 905 The other piece of information we compute for each function is a \emph{similarity} 906 relation, which is an equivalence relation on all kinds of registers which depends 907 on the point of the program. We write 908 $$x\sim y \at \ell$$ 909 to state that registers $x$ and $y$ are similar at $\ell$. The formal definition 910 will be given next, but intuitively it means that those two registers \emph{must} 911 have the same value at $\ell$. The analysis that produces this information can be 912 coarse: in our case, we just set two different registers to be similar at $\ell$ 913 if at $\ell$ itself there is a move instruction between the two. 914 915 The 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 922 We mark a certain colouring with a subscript if we want to specify in which 923 internal function it is taken. 924 \subsubsection{The translation} 925 For 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}$$ 930 where $\varepsilon$ is the empty block of instructions (i.e.\ a \texttt{GOTO}), 931 and $\Colour(r_1) \leftarrow \Colour(r_2) + \Colour(r_3)$ is a notation for a 932 block 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} 937 The overall effect is that if $T$ is an LTL state with $\ell(T)=\ell$ 938 then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$. 939 940 We skip over the details of correctly dealing with the stack and its size. 941 \subsubsection{The relation between ERTL and LTL states} 942 Given 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}.$$ 944 The program counter in $S$ is written as $\ell(S)$. At this point we can state 945 the 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 951 Next, we relate ERTL states with LTL ones. For a state $T$ in LTL we again 952 abuse the notation using $T$ as a map 953 $$T: \mathtt{hdwregister}+\mathtt{nat} \to \mathtt{Value}$$ 954 which 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 956 stack values). 957 958 The relation existing between the states at the two sides of this translation step, 959 which depends on liveness and colouring, is 960 then defined as 961 $$S\mathrel\sigma T \iff \ldots \wedge \forall x. x\in \Livebefore(\ell(S))\Rightarrow T(\Colour^+(x)) = S(x).$$ 962 The 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} 966 We 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$ 969 the inductive hypothsis, as it will be such in the complete proof by induction on the trace of the program. 970 As usual, this step be done by cases 971 on the statement at $\ell(S)$ and how it is translated. We carry out in some detail a single case, the one of 972 a binary operation on registers. 973 974 Suppose 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))$.} 977 By definition we have $r_1\notin \Liveafter(\ell(S))$, and the translation 978 of the operation yields a \texttt{GOTO}. We take $T'$ the immediate successor 979 of $T$. 980 981 Now in order to prove $S'\mathrel\sigma T'$, take any 982 $$x\in\Livebefore(\ell(S'))\subseteq \Liveafter(\ell(S)) = \Livebefore(\ell(S))$$ 983 where we have used property~\eqref{eq:livefixpoint} and the definition 984 of $\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)$$ 986 where 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))$.} 993 We then have $r_1\in\Liveafter(\ell(S))$, and 994 $$\Livebefore(\ell(S))=(\Liveafter(\ell(S))\setminus\{r_1\})\cup\{r_2,r_3\}.$$ 995 Moreover the statement is translated to $\Colour(r_1)\leftarrow\Colour(r_2)+\Colour(r_3)$, 996 and 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 999 Take any $x\in\Livebefore(\ell(S'))\subseteq \Liveafter(\ell(S))$ (by property~\eqref{eq:livefixpoint}). 1000 1001 If $\Colour^+(x)=\Colour(r_1)$, we have by property~\eqref{eq:colourprop} 1002 that $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)$$ 1004 where 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 1008 for this case of binary op $x\sim r_1\at\ell(S)$ implies $x=r_1$. But nothing prevents us from 1009 employing more fine euristics for similarity.}. 1010 \end{enumerate} 1011 1012 If $\Colour^+(x)\neq\Colour(r_1)$ (so in particular $x\neq r_1$), then $x\in\Livebefore(\ell(S))$, 1013 so by inductive hypothesis we have 1014 $$T'(\Colour^+(x))=T(\Colour^+(x))=S(x)=S'(x).$$ 1015 880 1016 \subsection{The LTL to LIN translation} 881 1017 \label{subsect.ltl.lin.translation}
Note: See TracChangeset
for help on using the changeset viewer.