How to Compute the Fixed Point on a DataFlow Lattice

Question

Wondering the general overview of how to compute the fixed point on a program's dataflow lattice.

A fixed point of a function $f(x)$ is one where the output of the function equals the input, so:

$$f(x) = x$$

Given $f$ is an order preserving (monotonic) function $x ⊑ y \Rightarrow f(x) ⊑ f(y)$, in this presentation, they have $x_\bot$ be the least fixed point of $f: L \to L$, so $f(x_\bot) = x_\bot$, where $L$ is a program lattice. Then they say:

Now, let $x_0 = \bot$ [the end of the lattice] and $x_i = f(x_{i−1})$

• By induction, $x_i ⊑ x_\bot$.
• Also, the chain $x_i$ is an ascending chain.
• If $L$ has no infinite ascending chains, sooner or later $x_i = x_{i+1} = x_\bot$

I'm wondering what this means. What happens algorithmically (the high-level steps) when we are iterating toward a fixed point. In the presentation they say "Do computation by simulating execution of program until reach fixed point".

This doc says "In this situation [data flow], the mathematical function is the flow function [so $f$], and the fixed point is a tuple of the dataflow analysis values at each point in the program (up to and including the loop)". They define flow function as a map from the dataflow info immediately before to after the program point / instruction.

So essentially, we divide the program into nodes or points where each point is an instruction/statement. We create a function showing the change of values from before and after each point (in and out, the flow function). We then iterate on the values somehow, that's where I'm unclear about. Wondering if we are iterating through the program points, calling $f$ for each point, or if we stay at one point and iterate on it with some sort of input until we reach a fixed point. Then wondering how that works. Not sure how the iteration works, or how $x_\bot$ works (if its part of some subset of the program points $L$ for each point (kind of like a neighborhood) or what.

Answer 1

You don't compute the least fixpoint of a lattice; you compute the least fixpoint of a function $f$. The standard method is to use a method called chaotic iteration, which is exactly the iterative algorithm described in your quote: set $x_0 := \bot$, $x_1 := f(x_0)$, $x_2 := f(x_1)$, etc., and keep iterating until you reach $i$ such that $x_i = x_{i+1}$; the resulting $x_i$ is the least fixpoint of $f$.

In some cases it is possible to speed this up for a particular function $f$, but don't worry about this at this stage.

It's possible to view the process above as in some sense simulating the execution of the program, but I find it likely that this viewpoint is going to lead to confusion, so I'm not sure I would recommend trying to understand it that way. Iteratively evaluating $f$ is not the same as iterating through the program points of the program.

Talk about splitting the program up is largely irrelevant to your question about how to compute a least fixpoint. There are two steps: convert the program to a function $f$; find the least fixpoint of $f$. The business about dividing up the program is relevant to how you convert the program to $f$, but not relevant to how you compute the fixpoint of $f$ (at least, not at the basic level).