review the iterative algorithm

O U T [e n t ry] = \emptyset f or (e a c h ba s i c b l oc k B \entry) O U T [B] = \emptyset w hi l e (c han g es t o an y O U T occ u r) f or (e a c h ba s i c b l oc k B \entry) {I N [B] = P a p re d ecessor o f B ⋃ O U T [P]; O U T [B] = g e n_{B} \cup (I N [B] - ki l l_{B});}

question

1. is the algorithm guaranteed to terminate or reach the fixed point, or does it always have a solution ?
1. if so, is there only one solution or only one fixed point ? if more than one, is our solution the best one (most precise) ?
1. When will the algorithm reach the fixed point, or when can we get the solution ?

We need some math - Lattice. But before introduce Lattice, we need learn some concept.

Partial Order

We define poset as a pair (P, $⊑$ ), where $⊑$ is a binary relation that defines a partial ordering over P, and $⊑$ has the following properties:

$\forall x \in P, x ⊑ x (R e f l e x i v i t y)$
$\forall x, y \in P, x ⊑ y \land y ⊑ x ⟹ x = y (A n t i sy mm e t ry)$
$\forall x, y, z \in P, x ⊑ y \land y ⊑ z ⟹ x ⊑ z (T r an s i t i v i t y)$

Example: Is (S, $⊑$ ) a poset where S is a set of integers and $⊑$ represents $\leq$ ? → Yes

partial means for a pair of set elements in P, they could be incomparable; in other words, not necessary that every pair of set elements must satisfy the ordering $⊑$

Upper and Lower Bounds

Given a poset (P, $⊑$ ) and its subset S that $S \subseteq P$ , we say that $u \in P$ is an upper bound of S, if $\forall x \in S, x ⊑ u$ . Similarly, $l \in P$ is an lower bound of S, if $\forall x \in S, l ⊑ x$ .

We define the least upper bound (lub or join) of S, written $⨆ S$ , if for every upper bound of S, say u, $⨆ S ⊑ u$ . Similarly, we define the greatest lower bound (glb, or meet) of S, written $⊓ S$ , if for every lower bound of S, say l, $l ⊑ ⊓ S$ .

Some properties:

Not every poset has lub or glb
But if a poset has lub or glb, it will be unique

Lattice

lattice 是数学理论用来证明 data-flow analysis 的正确性

Given a poset (P, $⊑$ ), $\forall a, b \in P, i f a ⨆ b an d a ⊓ b e x i s t$ , then (P, $⊑$ ) is called a lattice.

A poset is a lattice if every pair of its elements has a least upper bound and a greatest lower bound

Semilattice

Given a poset (P, $⊑$ ), $\forall a, b \in P$ ,

if only $a ⨆ b e x i s t s$ , then (P, $⊑$ ) is called a join semilattice.
if only $a ⊓ b e x i s t s$ , then (P, $⊑$ ) is called a meet semilattice.

Complete lattice

Given a lattice (P, $⊑$ ), for arbitrary subset S of P, if $⨆ S$ and $⊓ S$ exist, then (P, $⊑$ ) is called a complete lattice.

All subsets of a lattice have a least upper bound and a greatest lower bound.

Every complete lattice (P, $⊑$ ) has

a greatest element $⊤ = ⨆ P$ called top and
a least element $⊥ = ⊓ P$ called bottom

Every finite lattice (P is finite) is a complete lattice.

Product Lattice

Ok, now the math is enough

Data Flow Analysis Framework via Lattice

A data flow analysis framework (D, L, F) consists of:

D: a direction of data flow: forwards or backwards
L: a lattice including domain of values V and a meet $⨆$ or join $⊓$ operator
F: a family of transfer functions from V to V

Data flow analysis can be seen as iteratively applying transfer functions and meet/join operations on the values of a lattice

Now we can review the question of begin, for answering the three question, we need some properties:

monotonicity of lattice
lattice has only one top

Monotonicity

A function f : L → L (L is a lattice) is monotomic if $\forall x, y \in L$ , $x ⊑ y ⟹ f (x) ⊑ f (y)$

Fixed-Point Theorem

Given a complete lattice (L, $⊑$ ), if

f: L → L is monotonic and
L is finite then the least fixed point of f can be found by iterating $f (⊥), f (f (⊥)), \dots, f^{k} (⊥)$ until a fixed point is reached

then the greatest fixed point of f can be found by iterating $f (⊤), f (f (⊤)), \dots, f^{k} (⊤)$ until a fixed point is reached

May and Must Analyses, A Lattice View

Worklist Algorithm, an optimization of Iterative Algorithm

O U T [e n t ry] = \emptyset f or (e a c h ba s i c b l oc k B \entry) O U T [B] = \emptyset W or k l i s t \leftarrow a ll ba s i c b l oc k s w hi l e (W or k l i s t i s n o t e m pt y) P i c k a BB f ro m W or k l i s t o l d_O U T = O U T [B] I N [B] = P a p re d ecessor o f B ⋃ O U T [P]; O U T [B] = g e n_{B} \cup (I N [B] - ki l l_{B}); i f (o l d_O U T \neq = O U T [B]) A dd a ll s u ccessors o f B t o W or k l i s t

Recent Resource

Recent Project

Recent Area

Data Flow Analysis - Foundation