Changeset 1750 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 24, 2012, 5:02:06 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1749 r1750 15 15 \usepackage{skull} 16 16 \usepackage{stmaryrd} 17 \usepackage{array} 18 \newcolumntype{b}{@{}>{{}}} 19 \newcolumntype{B}{@{}>{{}}c<{{}}@{}} 20 \newcolumntype{h}[1]{@{\hspace{#1}}} 21 \newcolumntype{L}{>{$}l<{$}} 22 \newcolumntype{C}{>{$}c<{$}} 23 \newcolumntype{R}{>{$}r<{$}} 24 \newcolumntype{S}{>{$(}r<{)$}} 25 \newcolumntype{n}{@{}} 17 26 \usepackage{wasysym} 27 18 28 19 29 \lstdefinelanguage{matitaocaml} { … … 543 553 \mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\ 544 554 \mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\ 545 \mathtt{graph} & \mapsto\mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\555 \mathtt{graph} & \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\ 546 556 & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\ 547 557 \end{align*} … … 588 598 \subsection{The ERTL to LTL translation} 589 599 \label{subsect.ertl.ltl.translation} 590 600 \newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}} 601 \declsf{Livebefore} 602 \declsf{Liveafter} 603 \declsf{Defined} 604 \declsf{Used} 605 \declsf{Eliminable} 606 \declsf{StatementSem} 607 For the liveness analysis, we aim at a map 608 $\ell \in \mathtt{label} \mapsto $ live registers at $\ell$. 609 We define the following operators on ERTL statements. 610 $$ 611 \begin{array}{lL>{(ex. $}L<{)$}} 612 \Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}id\mapsto \text{callersave} 613 \\ 614 \Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}id\mapsto \text{parameters} 615 \end{array} 616 $$ 617 Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$ 618 is the type of sets of registers\footnote{More precisely, it is thethe lattice 619 of pairs of sets of pseudoregisters and sets of hardware registers, 620 with pointwise operations.}, we also have have the following 621 predicates: 622 $$ 623 \begin{array}{lL} 624 \Eliminable_{LA}(\ell) & iff $s(\ell)$ has sideeffects only on $r\notin LA(\ell)$ 625 \\& 626 (ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset, 627 \mathtt{CALL}id\mapsto \text{never}$) 628 \\ 629 \Livebefore_{LA}(\ell) &$:= 630 \begin{cases} 631 LA(\ell) &\text{if $\Eliminable_{LA}(\ell)$,}\\ 632 (LA(\ell)\setminus \Defined(s(\ell)))\cup \Used(s(\ell) &\text{otherwise}. 633 \end{cases}$ 634 \end{array} 635 $$ 636 In particular, $\Livebefore$ has type $(\mathtt{label}\to\mathtt{lattice})\to 637 \mathtt{label}\to\mathtt{lattice}$. 638 639 The equation on which we build the fixpoint is then 640 $$\Liveafter(\ell) \doteq \bigcup_{\ell' >_1 \ell} \Livebefore_{\Liveafter}(\ell')$$ 641 where $\ell' >_1 \ell$ denotes that $\ell'$ is an immediate successor of $\ell$ 642 in the graph. We do not require the fixpoint to be the least one, so the hypothesis 643 on $\Liveafter$ that we require is 644 $$\Liveafter(\ell) \supseteq \bigcup_{\ell' >_1 \ell} \Livebefore(\ell')$$ 645 (for shortness we drop the subscript from $\Livebefore$). 591 646 \subsection{The LTL to LIN translation} 592 647 \label{subsect.ltl.lin.translation}
Note: See TracChangeset
for help on using the changeset viewer.