Changeset 1788


Ignore:
Timestamp:
Feb 28, 2012, 11:32:07 AM (7 years ago)
Author:
tranquil
Message:

small modifications

File:
1 edited

Legend:

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

    r1786 r1788  
    879879Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$
    880880is the type of sets of registers\footnote{More precisely, it is the lattice
    881 of pairs of sets of pseudo-registers and sets of hardware registers,
     881$\mathtt{set}(\mathtt{register})\times
     882\mathtt{set}(\mathtt{hdwregister})$,
    882883with pointwise operations.}), we also have have the following
    883884predicates:
     
    933934$$x\sim y \at \ell$$
    934935to 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 at $\ell$. The analysis that produces this information can be
     936of this relation's property will be given next, but intuitively it means that those two registers \emph{must}
     937have the same value after $\ell$. The analysis that produces this information can be
    937938coarse: in our case, we just set two different registers to be similar at $\ell$
    938939if at $\ell$ itself there is a move instruction between the two.
     
    959960\end{itemize}
    960961The 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.
     962then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$,
     963while $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 book-keeping and which
     965are explicitly excluded from colouring may have different values.
     966
     967We skip the details of correctly dealing with the stack and its size.
    964968\subsubsection{The relation between ERTL and LTL states}
    965969Given 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.