Changeset 1750 for Deliverables

Timestamp:

Feb 24, 2012, 5:02:06 PM (8 years ago)

Author:

tranquil

Message:

start of ERTL to LTL

File:

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

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -15 +15 @@
 \usepackage{skull}
 \usepackage{stmaryrd}
+\usepackage{array}
+\newcolumntype{b}{@{}>{{}}}
+\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
+\newcolumntype{h}[1]{@{\hspace{#1}}}
+\newcolumntype{L}{>{$}l<{$}}
+\newcolumntype{C}{>{$}c<{$}}
+\newcolumntype{R}{>{$}r<{$}}
+\newcolumntype{S}{>{$(}r<{)$}}
+\newcolumntype{n}{@{}}
 \usepackage{wasysym}
+
 
 \lstdefinelanguage{matita-ocaml} {
@@ -543 +553 @@
 \mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
 \mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
-\mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
+\mathtt{graph} &  \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
 & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
 \end{align*}
@@ -588 +598 @@
 \subsection{The ERTL to LTL translation}
 \label{subsect.ertl.ltl.translation}
-
+\newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}}
+\declsf{Livebefore}
+\declsf{Liveafter}
+\declsf{Defined}
+\declsf{Used}
+\declsf{Eliminable}
+\declsf{StatementSem}
+For the liveness analysis, we aim at a map
+$\ell \in \mathtt{label} \mapsto $ live registers at $\ell$.
+We define the following operators on ERTL statements.
+$$
+\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}
+\\
+\Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \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
+of pairs of sets of pseudo-registers and sets of hardware registers,
+with pointwise operations.}, we also have have the following
+predicates:
+$$
+\begin{array}{lL}
+\Eliminable_{LA}(\ell) & iff $s(\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,
+  \mathtt{CALL}id\mapsto \text{never}$)
+\\
+\Livebefore_{LA}(\ell) &$:=
+  \begin{cases}
+    LA(\ell) &\text{if $\Eliminable_{LA}(\ell)$,}\\
+    (LA(\ell)\setminus \Defined(s(\ell)))\cup \Used(s(\ell) &\text{otherwise}.
+  \end{cases}$
+\end{array}
+$$
+In particular, $\Livebefore$ has type $(\mathtt{label}\to\mathtt{lattice})\to
+\mathtt{label}\to\mathtt{lattice}$.
+
+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$
+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')$$
+(for shortness we drop the subscript from $\Livebefore$).
 \subsection{The LTL to LIN translation}
 \label{subsect.ltl.lin.translation}