Lab 14 · Round-robin vs worklists vs sparse, and liveness in Datalog¶

Chapter: 14 · Dataflow Analysis & Abstract Interpretation · Lessons: 14.4 (solver orders), 14.6 (sparse liveness, Algorithm 14.6.4), 14.8 (Datalog, Algorithms 14.8.3–14.8.4) · Time: 4–6 hours after E1 and E2 · Tests: ./course test 14 (labels ch14, lab)

Goal¶

Solve the same analyses in several ways and measure the difference. Part A compares the five solver strategies of your E1 solver (round-robin in RPO and in postorder, FIFO, LIFO and priority worklists) on random gen/kill problems and on a pathological loop chain, and then dense bit-vector liveness (your E2) against a sparse per-value liveness you write here (L1). Part B writes liveness a third way: as four Datalog rules (L4), evaluated by a small bottom-up Datalog engine you write in Python (L3), naively and semi-naively. Every implementation is checked against the others; the provided drivers print the numbers you then explain with Lessons 14.4, 14.6 and 14.8.

Requirements¶

L1. Sparse liveness. Implement lab14::computeLivenessSparse (contract below) with the path-exploration algorithm of Lesson 14.6 (Algorithm 14.6.4): for every use of a value, walk backwards from the using block (for a phi use: from the end of the incoming block) through predecessors, marking the value live-in / live-out, and stop at the defining block or at a block where the value is already marked. The result must equal pebble::dataflow::computeLiveness(F) as sets on every block of every function, reachable or not (the conventions of Liveness.h: phi results are not live-in to their block; a phi's incoming value is live-out of that predecessor). Count one SparseStats::Marks each time a value is newly added to some block's live-in set (so at the end Marks equals the total size of all live-in sets). Complexity: $O(\sum_v \lvert \text{blocks where } v \text{ is live} \rvert + \text{uses})$, no per-block iteration over all values. No recursion per block (the bench uses 5 000-block functions).
L2. Measurement. Run both drivers (below) and fill in the table under Milestones. Explain each row with the lesson results it illustrates: the $d(G) + 2$ bound (Theorem 14.4.6) and the loop chain (Proposition 14.4.10) for Part 1–2, Proposition 14.6.11 for Part 3, Proposition 14.8.11 for Datalog.
L3. A Datalog engine. Implement evaluate in datalog/datalog.py (standard library only) with naive (Algorithm 14.8.3) and semi-naive (Algorithm 14.8.4) bottom-up evaluation and stratified negation. The syntax, the error cases and the two counters are specified exactly below, because the tests compare them.
L4. Liveness as rules. Write datalog/liveness.dl: rules defining live_in(V, B) and live_out(V, B) from the facts edge, def, use, phiuse (below), equal to Definition 14.3.9 — the tests compare your relations with the output of the C++ analysis on every tests/ch14/Inputs/*.facts, with both methods.

The contract¶

L1 (C++), in include/lab14/SparseLiveness.h; your code goes anywhere under src/:

namespace lab14 {
struct SparseStats { std::uint64_t Marks = 0; };
pebble::dataflow::LivenessResult
computeLivenessSparse(const llvm::Function &F, SparseStats *Stats = nullptr);
}

L3 (Python), in datalog/datalog.py — the tests use only these three names:

class DatalogError(Exception): ...
@dataclass
class Result:
    relations: dict[str, set[tuple[str, ...]]]   # every relation, EDB and IDB
    iterations: int                               # rounds (see below)
    derivations: int                              # rule firings (see below)
def evaluate(program: str, facts: str | dict | None = None, *, method: str = "semi-naive") -> Result

facts is extra input: either text in the same syntax (facts only; a rule there is an error) or a dict mapping a relation name to a set of tuples (elements converted with str).

Datalog syntax¶

A program is a sequence of clauses, each ending in .: a fact edge(a, "b c"). (no variables) or a rule head(X, Y) :- atom, atom, ... .. Comments run from // or # to the end of the line.
An atom is name(arg, ..., arg) with at least one argument; a body atom may be negated with a leading !. Heads are never negated.
An argument is a variable (an identifier starting with an upper-case letter or _), or a constant: a lower-case identifier (a, entry), an integer (-3), or a double-quoted string with backslash escapes ("f:%x.0"). Constants are strings: a, "a" denote the same constant.
Raise DatalogError for: a syntax error; a fact with a variable; a relation used with two different arities (in facts or rules); an unsafe rule (a variable of the head or of a negated atom that occurs in no positive body atom); a program that is not stratifiable (a relation depends negatively on itself through recursion); an unknown method.

Evaluation, rounds and derivations¶

Strata. Relations defined by rules (IDB) get the least stratum numbers such that stratum(head) ≥ stratum(positive body relation) and stratum(head) > stratum(negated body relation); EDB relations are fixed input. Strata are evaluated in increasing order, each to its fixed point; a negated atom only ever refers to a relation of a lower stratum or the EDB, which is complete by then.
Naive (per stratum): one round fires every rule of the stratum on the whole current database; the new tuples are added after the round; stop after a round that produces no new tuple.
Semi-naive (per stratum): round 1 fires every rule on the whole database (everything is new); in every later round, a rule with $k$ positive body atoms over relations of the current stratum is fired $k$ times, the $j$-th time with atom $j$ ranging over the previous round's delta (the tuples first derived in that round) and every other atom over the full relation. Rules without such atoms fire only in round 1. Stop after a round with no new tuple.
iterations = the number of rounds, summed over strata, including each stratum's final round that derives nothing.
derivations = the number of successful body instantiations (one per satisfying assignment of the body's variables, per firing), including duplicates and tuples already known.

Example (the tests): transitive closure path(X, Y) :- edge(X, Y). path(X, Z) :- path(X, Y), edge(Y, Z). on a 10-node chain derives 45 paths in 10 rounds with both methods; on a 30-node chain semi-naive makes exactly 435 derivations (each path once), naive more than five times as many.

Liveness facts (L4)¶

opt -load-pass-plugin=<PebblePasses> -passes='print<pebble-datalog-facts>' -disable-output f.ll prints, per function, these facts (names are "<function>:<name>", so several functions can share one database):

Fact	Meaning
`edge(B, S)`	a CFG edge $B \to S$
`def(V, B)`	value $V$ is defined in block $B$ (phis included; arguments in the entry block)
`use(V, B)`	a non-phi instruction of $B$ uses $V$ and $V$ is not defined earlier in $B$ (upward exposed)
`phiuse(V, P, B)`	a phi of $B$ uses $V$ on the edge $P \to B$

Input and output formats¶

usage: ch14-solverbench [--quick] [--seed N]
uv run python labs/ch14-dataflow/datalog/compare.py FACTS [FACTS ...] [--rules liveness.dl]
uv run python labs/ch14-dataflow/datalog/compare.py --chain N

ch14-solverbench prints three Markdown tables and a verdict, and exits with status 1 if any two strategies (or dense and sparse liveness) disagree. With --quick (the ctest smoke run) the inputs are small; the output of the reference solution starts:

## Part 1: solver strategies on random gen/kill problems (256 facts)

| CFG nodes | direction | strategy | evaluations | evals / node | passes | time (ms) |
|---:|---|---|---:|---:|---:|---:|
| 50 | forward | round-robin RPO | 200 | 4.00 | 4 | 0.06 |
...
## Part 3: dense vs sparse liveness on random SSA functions

| blocks | values | dense (ms) | sparse (ms) | sparse marks | agree |
|---:|---:|---:|---:|---:|---|
| 20 | 61 | 0.05 | 0.02 | 65 | yes |
...
OK: every strategy and both liveness algorithms agree

compare.py evaluates the rules with both methods and prints rounds, derivations and time per input:

### transitive closure of a 20-node chain

| method | rounds | derivations | time (ms) |
|---|---:|---:|---:|
| naive | 20 | 2660 | 27.3 |
| semi-naive | 20 | 190 | 2.3 |

naive and semi-naive agree: yes

Provided infrastructure¶

File	What it gives you
`bench/SolverBench.cpp`	the C++ driver: random CFGs and gen/kill problems (Part 1), the loop chain (Part 2), random SSA functions for dense vs sparse liveness (Part 3), cross-checks
`include/lab14/RandomIR.h`, `provided/RandomIR.cpp`	random CFGs and random SSA functions (also used by the unit tests)
`datalog/compare.py`	the Datalog measurement driver; `PEBBLE_DATALOG_DIR` selects another engine directory
`pebble/lib/Passes/Dataflow/Ch14Passes.cpp`	`print<pebble-liveness>` and `print<pebble-datalog-facts>`
`tests/ch14/Inputs/.facts`, `.liveness`	facts and the matching C++ liveness for the test corpus

What the tests check¶

Test	Checks
`ch14.SparseLiveness.Corpus`	L1 equals an independent path-search liveness oracle (the one that checks E2) on every function of `tests/ch14/Inputs/*.ssa.ll`, and `Marks` equals the number of (value, block) live-in pairs — each pair is discovered exactly once
`ch14.SparseLiveness.RandomSSAFunctions`	the same on 150 random SSA functions of 3–16 blocks with up to 4 back edges
`ch14.lab.bench-smoke`	`ch14-solverbench --quick` exits 0
`ch14.datalog` → `EngineTest.*`	L3: transitive closure (relations, 10 rounds), 435 semi-naive derivations on a 30-chain and naive > 5×, facts and constants in the program text, stratified negation, the five error cases
`ch14.datalog` → `LivenessRulesTest.*`	L4 (with your L3): `live_in` / `live_out` equal the C++ liveness on every `.facts` input, naive and semi-naive

Milestones¶

E1 and E2 pass (ctest --preset linux -L '^ch14$' -R 'DataflowSolver|Liveness').
L1: ch14.SparseLiveness.* and ch14.lab.bench-smoke pass.
L3, then L4: ch14.datalog passes (ctest --preset linux -R ch14.datalog --output-on-failure).
Measure and fill in:

cmake --build build/linux --target ch14-solverbench
build/linux/bin/ch14-solverbench
uv run python labs/ch14-dataflow/datalog/compare.py tests/ch14/Inputs/*.facts
uv run python labs/ch14-dataflow/datalog/compare.py --chain 60

Input	Your numbers	Reference (Lessons 14.4, 14.6, 14.8)
Part 1, 10 000 nodes forward: RPO / postorder / FIFO evaluations		60 000 / 690 000 / 46 448
Part 2, loop chain $n = 1024$: RPO / postorder evaluations		3 072 / 1 049 600
Part 3, 5 000 blocks: dense / sparse ms		228 / 14.6 (timings: one run on the course container; expect different numbers, the same ratio)
Datalog, chain 60: naive / semi-naive derivations		71 980 / 1 770

For each row, name the result that predicts it and check the prediction (for example: why is postorder round-robin exactly $n + 1$ passes on the loop chain? why do naive and semi-naive need the same number of rounds?).

Hints¶

Hint 1 — where to start

For L1, first collect, for every value, its uses as (block, is-phi-use, incoming block) triples; then run the backward walk per value with an explicit stack. For L3, write the parser first and test it on the examples above; evaluation is a nested-loop join over the body atoms from left to right.

Hint 2 — the key idea

L1: a value is live-in at a block iff some use is reachable backwards from it without passing the definition, so "stop when already marked" makes each (value, block) pair cost O(1) amortized. A phi use makes the value live-out of the incoming block, not live-in of the phi's block. L3: semi-naive evaluation is correct because every new derivation must use at least one tuple that was new in the previous round (Theorem 14.8.5); firing a rule once per recursive atom with that atom restricted to the delta covers exactly those.

Hint 3 — a design sketch

L1: DenseMap<const BasicBlock *, unsigned> block numbers, one BitVector or SmallPtrSet per block for live-in and live-out, and a worklist of blocks per value. The common bug the random tests catch: values used in unreachable blocks (walk them too) and a value used by a phi in its own block (a loop-carried phi). L3: keep relations as sets of tuples, represent a variable binding as a dict, and count a derivation every time the body matches — before checking whether the head tuple is new. The common bug: a negated atom whose relation is in the current stratum (must be rejected), and forgetting the final, empty round in iterations.

Stretch goals ★¶

Add an SCC-ordered worklist (Bourdoncle's weak topological order, Lesson 14.4 §6) to your solver as a sixth strategy in a local copy of the bench, and compare its evaluation counts with priority-by-RPO on Part 1.
Run liveness.dl in Soufflé (Lesson 14.8's real-world box) on the same .facts files and compare its time with your engine's.
Write reaching definitions or definite initialization as Datalog rules (definite initialization needs negation: "not initialized on some path").

Fact	Meaning
`edge(B, S)`	a CFG edge \(B \to S\)
`def(V, B)`	value \(V\) is defined in block \(B\) (phis included; arguments in the entry block)
`use(V, B)`	a non-phi instruction of \(B\) uses \(V\) and \(V\) is not defined earlier in \(B\) (upward exposed)
`phiuse(V, P, B)`	a phi of \(B\) uses \(V\) on the edge \(P \to B\)

Input	Your numbers	Reference (Lessons 14.4, 14.6, 14.8)
Part 1, 10 000 nodes forward: RPO / postorder / FIFO evaluations		60 000 / 690 000 / 46 448
Part 2, loop chain \(n = 1024\): RPO / postorder evaluations		3 072 / 1 049 600
Part 3, 5 000 blocks: dense / sparse ms		228 / 14.6 (timings: one run on the course container; expect different numbers, the same ratio)
Datalog, chain 60: naive / semi-naive derivations		71 980 / 1 770