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.