Changeset 1788 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 28, 2012, 11:32:07 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1786 r1788 879 879 Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$ 880 880 is the type of sets of registers\footnote{More precisely, it is the lattice 881 of pairs of sets of pseudoregisters and sets of hardware registers, 881 $\mathtt{set}(\mathtt{register})\times 882 \mathtt{set}(\mathtt{hdwregister})$, 882 883 with pointwise operations.}), we also have have the following 883 884 predicates: … … 933 934 $$x\sim y \at \ell$$ 934 935 to state that registers $x$ and $y$ are similar at $\ell$. The formal definition 935 will be given next, but intuitively it means that those two registers \emph{must}936 have the same value a t$\ell$. The analysis that produces this information can be936 of this relation's property will be given next, but intuitively it means that those two registers \emph{must} 937 have the same value after $\ell$. The analysis that produces this information can be 937 938 coarse: in our case, we just set two different registers to be similar at $\ell$ 938 939 if at $\ell$ itself there is a move instruction between the two. … … 959 960 \end{itemize} 960 961 The overall effect is that if $T$ is an LTL state with $\ell(T)=\ell$ 961 then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$. 962 963 We skip over the details of correctly dealing with the stack and its size. 962 then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$, 963 while $T'(y)=T(y)$ for any $y$ \emph{in the image of $\Colour$} different from 964 $\Colour(r_1)$. Some hardware registers that are used for bookkeeping and which 965 are explicitly excluded from colouring may have different values. 966 967 We skip the details of correctly dealing with the stack and its size. 964 968 \subsubsection{The relation between ERTL and LTL states} 965 969 Given a state $S$ in ERTL, we abuse the notation by using $S$ as the underlying map
Note: See TracChangeset
for help on using the changeset viewer.