Chaotic Iteration

Author

Bor-Yuh Evan Chang

Published

Tuesday, November 18, 2025

$\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} $

What questions do you have? What questions does your neighbor have?

Announcements

Project presentation (Mon Dec 8 1:30-4 p.m.)
Project paper (Fri Dec 12 AoE)
Extra support
- Extra office hours (before and after class Thu 8:30am-1:00pm)
- Happy to review your “proposals” over break

See advice on final projects.

Questions?

Review: Dataflow Analysis

Exercise: Dataflow Equations

For a given program $g$, the set of locations is finite. Describe a program invariant $\hat{\Sigma}$ as a finite set of dataflow equations for each program location. Assume an entry location $\ell_0$ to the procedure $g$ with an initial abstract store $\hat{\rho}_0$.

Dataflow Equations

Definition 1 (Dataflow Equations) An inductive program invariant $\hat{\Sigma}$ is a solution to the set of dataflow equations for program $g$ with an entry location $\ell_0$ and initial abstract store $\hat{\rho}_0$: \[ \begin{array}{rrll} \hat{\Sigma}( \ell_0 ) & = & \hat{\rho}_0 \\ \hat{\Sigma}( \ell_i ) & = & \bigsqcup_{ \ell_j \mathrel{\mathord{-}\mkern-4mu[c]\mkern-4mu\mathord{\rightarrow}} \ell_i \in g} \{ \hat{\rho}' \mid \hat{\Sigma}(\ell_j) \vdash c \Downarrow\hat{\rho}' \} & \text{for $i \neq 0$} \end{array} \]

We solve a dataflow analysis by finding the least fixed point of the set of transfer functions (i.e., one for each program location $\ell_i$ where $i \neq 0$).

Exercise: Chaotic Iteration

\[ \begin{array}{rrll} \hat{\Sigma}( \ell_0 ) & = & \hat{\rho}_0 \\ \hat{\Sigma}( \ell_i ) & = & \bigsqcup_{ \ell_j \mathrel{\mathord{-}\mkern-4mu[c]\mkern-4mu\mathord{\rightarrow}} \ell_i \in g} \{ \hat{\rho}' \mid \hat{\Sigma}(\ell_j) \vdash c \Downarrow\hat{\rho}' \} & \text{for $i \neq 0$} \end{array} \]

The chaotic iteration algorithm computes the least fixed-point invariant $\hat{\Sigma}_\omega$ by iterating at each location $\ell_i$ until convergence.

r = 1;
while
  (n > 0) {
    r = r * x;
    n = n - 1;
  }

Fill in the following table where each $\hat{\Sigma}_i$ is the $i$th iterate using the sign abstract domain. Cell $\hat{\Sigma}_0(\ell_0)$ is $\hat{\rho}_0$, which consider to be $\top$.

	$\hat{\Sigma}_0$	$\hat{\Sigma}_1$	$\hat{\Sigma}_2$	$\hat{\Sigma}_3$	$\hat{\Sigma}_4$	$\hat{\Sigma}_5$	$\hat{\Sigma}_6$	$\hat{\Sigma}_7$	$\hat{\Sigma}_8$	$\hat{\Sigma}_9$	$\hat{\Sigma}_{10}$	$\hat{\Sigma}_\omega$
$\ell_0$	$\top$
$\ell_1$	$\bot$
$\ell_2$	$\bot$
$\ell_3$	$\bot$
$\ell_4$	$\bot$
$\ell_5$	$\bot$
$\ell_6$	$\bot$

Chaotic Iteration

Let us use the convention that empty cells mean that the abstract store at location is unchanged from the previous iterate and $\cdot$ means we have detected a fixed point at that location.

	$\hat{\Sigma}_0$	$\hat{\Sigma}_1$	$\hat{\Sigma}_2$	$\hat{\Sigma}_3$	$\hat{\Sigma}_4$	$\hat{\Sigma}_5$	$\hat{\Sigma}_6$	$\hat{\Sigma}_7$	$\hat{\Sigma}_8$	$\hat{\Sigma}_9$	$\hat{\Sigma}_{10}$	$\hat{\Sigma}_{\omega}$
$\ell_0$	$\top$
$\ell_1$	$\bot$	$\texttt{r} \mapsto\mathsf{+}$
$\ell_2$	$\bot$		$\texttt{r} \mapsto\mathsf{+}$				$\top$				$\cdot$
$\ell_3$	$\bot$			$\texttt{r} \mapsto\mathsf{+}$				$\top$
$\ell_4$	$\bot$				$\top$				$\cdot$
$\ell_5$	$\bot$					$\top$				$\cdot$
$\ell_6$	$\bot$											$\top$

Exercise: Reflection: Chaotic Iteration

What is the worst-case complexity of chaotic iteration?

For efficiency, chaotic iteration is typically done by following the reverse post-order of the weak topological order of the strongly-connected components. What does this mean?

How could we generalize chaotic interation to infinite height domains?

Reflection: Chaotic Iteration

What is the worst-case complexity of chaotic iteration?

For a lattice with height $h$ and procedure with $n$ program locations, chaotic iteration is $O(h \cdot n)$ in the worst case.

For efficiency, chaotic iteration is typically done by following the reverse post-order of the weak topological order of the strongly-connected components. What does this mean?

Intuitively, find the fixed points of inner loops before outer loops.

How could we generalize chaotic interation to infinite height domains?

Intuitively, apply widening $\mathbin{\nabla}$ at some program location within each loop.

Exercise: Widening

i = 0;
while
  (i < n) {
    i = i + 1;
  }

Fill in the following table where each $\hat{\Sigma}_i$ is the $i$th iterate using the interval abstract domain with widening at the loop head $\ell_2$. Cell $\hat{\Sigma}_0(\ell_0)$ is $\hat{\rho}_0$, which consider to be $\top$.

	$\hat{\Sigma}_0$	$\hat{\Sigma}_1$	$\hat{\Sigma}_2$	$\hat{\Sigma}_3$	$\hat{\Sigma}_4$	$\hat{\Sigma}_5$	$\hat{\Sigma}_6$	$\hat{\Sigma}_7$	$\hat{\Sigma}_8$	$\hat{\Sigma}_9$	$\hat{\Sigma}_{10}$	$\hat{\Sigma}_\omega$
$\ell_0$	$\top$
$\ell_1$	$\bot$
$\ell_2$	$\bot$
$\ell_3$	$\bot$
$\ell_4$	$\bot$
$\ell_5$	$\bot$

Widening

	$\hat{\Sigma}_0$	$\hat{\Sigma}_1$	$\hat{\Sigma}_2$	$\hat{\Sigma}_3$	$\hat{\Sigma}_4$	$\hat{\Sigma}_5$	$\hat{\Sigma}_6$	$\hat{\Sigma}_7$	$\hat{\Sigma}_8$	$\hat{\Sigma}_\omega$
$\ell_0$	$\top$
$\ell_1$	$\bot$	$\texttt{i} \mapsto[0, 0]$
$\ell_2$	$\bot$		$\texttt{i} \mapsto[0, 0]$			$\texttt{i} \mapsto[0, \infty)$			$\cdot$
$\ell_3$	$\bot$			$\texttt{i} \mapsto[0, 0]$			$\texttt{i} \mapsto[0, \infty)$
$\ell_4$	$\bot$				$\texttt{i} \mapsto[1, 1]$			$\texttt{i} \mapsto[1, \infty)$
$\ell_5$	$\bot$									$\texttt{i} \mapsto[0, \infty)$

Summary: An Abstract Interpretation Template

Syntax

expressions $\quad e$

statements $\quad s$

Concrete Semantic Domains

values $\quad v$

states $\quad \sigma$

Concrete Semantics

$\fbox{$\sigma \vdash e \Downarrow v$}$

$\fbox{$\sigma \vdash s \Downarrow\sigma'$}$

Forward-Reachable Collecting Semantics

$\begin{array}{rrrl} \text{value properties} & V& \mathrel{::=}& \circ\mid V,v \end{array}$

$\begin{array}{rrrl} \text{state properties} & \Sigma& \mathrel{::=}& \circ\mid\Sigma,\sigma \end{array}$

$\fbox{$\lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace = \lambda \Sigma.V$}$

$\fbox{$\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda \Sigma.\Sigma'$}$

$\lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace\,\Sigma = \{ v \mid \text{$\sigma \vdash e \Downarrow v$ and $\sigma\in \Sigma$} \}$

$\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace\,\Sigma = \{ \sigma' \mid \text{$\sigma \vdash s \Downarrow\sigma'$ and $\sigma\in \Sigma$} \}$

Abstract Domains

$\begin{array}{rrrl} \text{abstract values} & \hat{v} \end{array}$

$\begin{array}{rrrl} \text{abstract states} & \hat{\sigma} \end{array}$

$\fbox{$\gamma(\hat{v}) = V$}$

$\fbox{$\gamma(\hat{\sigma}) = \Sigma$}$

$\fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{v}$}$

$\fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack^\sharp = \lambda \hat{\sigma}.\hat{\sigma}'$}$

$\gamma( \lbrack\!\lbrack e \rbrack\!\rbrack^\sharp\,\hat{\sigma} ) \supseteq \lbrace\!\lbrack\!\lbrack e \rbrack\!\rbrack\!\rbrace\, \gamma(\hat{\sigma}) \quad $for all $\hat{\sigma}$

$\gamma( \lbrack\!\lbrack s \rbrack\!\rbrack^\sharp\,\hat{\sigma} ) \supseteq \lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace\, \gamma(\hat{\sigma}) \quad $for all $\hat{\sigma}$

	\(\hat{\Sigma}_0\)	\(\hat{\Sigma}_1\)	\(\hat{\Sigma}_2\)	\(\hat{\Sigma}_3\)	\(\hat{\Sigma}_4\)	\(\hat{\Sigma}_5\)	\(\hat{\Sigma}_6\)	\(\hat{\Sigma}_7\)	\(\hat{\Sigma}_8\)	\(\hat{\Sigma}_9\)	\(\hat{\Sigma}_{10}\)	\(\hat{\Sigma}_\omega\)
\(\ell_0\)	\(\top\)
\(\ell_1\)	\(\bot\)
\(\ell_2\)	\(\bot\)
\(\ell_3\)	\(\bot\)
\(\ell_4\)	\(\bot\)
\(\ell_5\)	\(\bot\)
\(\ell_6\)	\(\bot\)

	\(\hat{\Sigma}_0\)	\(\hat{\Sigma}_1\)	\(\hat{\Sigma}_2\)	\(\hat{\Sigma}_3\)	\(\hat{\Sigma}_4\)	\(\hat{\Sigma}_5\)	\(\hat{\Sigma}_6\)	\(\hat{\Sigma}_7\)	\(\hat{\Sigma}_8\)	\(\hat{\Sigma}_9\)	\(\hat{\Sigma}_{10}\)	\(\hat{\Sigma}_{\omega}\)
\(\ell_0\)	\(\top\)
\(\ell_1\)	\(\bot\)	\(\texttt{r} \mapsto\mathsf{+}\)
\(\ell_2\)	\(\bot\)		\(\texttt{r} \mapsto\mathsf{+}\)				\(\top\)				\(\cdot\)
\(\ell_3\)	\(\bot\)			\(\texttt{r} \mapsto\mathsf{+}\)				\(\top\)
\(\ell_4\)	\(\bot\)				\(\top\)				\(\cdot\)
\(\ell_5\)	\(\bot\)					\(\top\)				\(\cdot\)
\(\ell_6\)	\(\bot\)											\(\top\)

	\(\hat{\Sigma}_0\)	\(\hat{\Sigma}_1\)	\(\hat{\Sigma}_2\)	\(\hat{\Sigma}_3\)	\(\hat{\Sigma}_4\)	\(\hat{\Sigma}_5\)	\(\hat{\Sigma}_6\)	\(\hat{\Sigma}_7\)	\(\hat{\Sigma}_8\)	\(\hat{\Sigma}_9\)	\(\hat{\Sigma}_{10}\)	\(\hat{\Sigma}_\omega\)
\(\ell_0\)	\(\top\)
\(\ell_1\)	\(\bot\)
\(\ell_2\)	\(\bot\)
\(\ell_3\)	\(\bot\)
\(\ell_4\)	\(\bot\)
\(\ell_5\)	\(\bot\)

	\(\hat{\Sigma}_0\)	\(\hat{\Sigma}_1\)	\(\hat{\Sigma}_2\)	\(\hat{\Sigma}_3\)	\(\hat{\Sigma}_4\)	\(\hat{\Sigma}_5\)	\(\hat{\Sigma}_6\)	\(\hat{\Sigma}_7\)	\(\hat{\Sigma}_8\)	\(\hat{\Sigma}_\omega\)
\(\ell_0\)	\(\top\)
\(\ell_1\)	\(\bot\)	\(\texttt{i} \mapsto[0, 0]\)
\(\ell_2\)	\(\bot\)		\(\texttt{i} \mapsto[0, 0]\)			\(\texttt{i} \mapsto[0, \infty)\)			\(\cdot\)
\(\ell_3\)	\(\bot\)			\(\texttt{i} \mapsto[0, 0]\)			\(\texttt{i} \mapsto[0, \infty)\)
\(\ell_4\)	\(\bot\)				\(\texttt{i} \mapsto[1, 1]\)			\(\texttt{i} \mapsto[1, \infty)\)
\(\ell_5\)	\(\bot\)									\(\texttt{i} \mapsto[0, \infty)\)