<aside> 💡 Key Points

• Understand the functional view of iterative algorithm
• The definitions of lattice and complete lattice
• Understand the fixed-point theorem
• How to summarize may and must analyses in lattices
• The relation between MOP and the solution produced by the iterative algorithm
• Constant propagation analysis
• Worklist algorithm </aside>

I. Iterative Algorithm, Another View

• Given a CFG (program) with k nodes, the iterative algorithm updates OUT[n] for every node n in each iteration.

• Assume the domain of the values in data flow analysis is V, then we can define a k-tuple

  $$ \rm (OUT[n_1 ], OUT[n_2 ], …, OUT[n_k ]) $$

  as an element of set $(V_1 × V_2 … × V_k )$ denoted as $V^k$ , to hold the values of the analysis after each iteration.

• Each iteration can be considered as taking an action to map an element of $V^k$ to a new element of $V^k$ , through applying the transfer functions and control-flow handing, abstracted as a function $F: V^k → V^k$

• Then the algorithm outputs a series of k-tuples iteratively until a k-tuple is the same as the last one in two consecutive iterations

$$ \begin{aligned} &\mathrm{X~is~a~fixed~point~of~function~F~if~\blue{X=F(X)}} \\ &\mathrm{The~iterative~algorithm~reaches~a~\orange{fixed~point}} \\ \end{aligned} $$

<aside> 💡 Fundamental problems to be solved

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

II. Mathematical Knowledge

1. 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:

$$ \begin{aligned}

&\mathrm{(1)~∀x ∈ P;~x ⊑ x~} &\textrm{(Reflexivity)} \\

&\mathrm{(2)~∀x, y ∈ P;~x ⊑ y ∧ y ⊑ x ⟹ x = y~} &\textrm{(Antisymmetry)} \\

&\mathrm{(3)~∀x, y, z ∈ P;~x ⊑ y ∧ y ⊑ z ⟹ x ⊑ z~} &\textrm{(Transitivity)} \\ \end{aligned} $$

2. Upper and Lower Bounds

Given a poset (P, ⊑) and its subset S that S ⊆ P, we say that

$$

\begin{aligned}&u\in P\mathrm{~is~an~\red{upper~bound}~of~S,~if~∀x∈S,x⊑u.~} \\ &\mathrm{Similarly,~l~∈~P~is~an~\blue{lower~bound}~of~S,~if~∀x∈S,~l⊑x.} \\ \end{aligned} $$

• 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$.