Flashcards — Chapter 13¶
105 cards. Review them with spaced repetition in the terminal (./course flash 13) or export them to Anki (./course flash export 13). Here, click a card to reveal its back.
scopes¶
What are the optimization scopes, from smallest to largest?
Local (one basic block), superlocal (an extended basic block path), regional (the dominator-tree path), global (all paths, merged at joins), interprocedural (Definition 13.1.2).
What is an extended basic block?
A maximal tree of blocks: a root that is the entry or has ≠ 1 predecessor, and members that each have exactly one predecessor, inside the set (Definition 13.1.1). Each root-to-node path is straight-line code.
Why is a superlocal scope sound for value numbering?
Every execution entering block B_j of an EBB path has just executed B_1 … B_{j-1} in order (Proposition 13.1.3), so facts from the path hold; a scoped table pops facts when leaving a subtree (Lemma 13.1.10).
Cost of superlocal / dominator-based value numbering?
O(n) expected with a scoped hash table (one push/pop per block); regional adds building the dominator tree.
constant-folding¶
What must a constant folder model exactly?
The IR semantics at the IR's width: two's-complement wrapping, poison for violated flags and oversized shifts, immediate UB (division by zero, INT_MIN / -1), and IEEE 754 round-to-nearest for FP (Definition 13.1.6).
Why doesn't pebble-constfold fold udiv i32 7, 0?
It is immediate UB. Replacing it would be a refinement, but it would silently remove a trap the program may rely on; E1 leaves UB in place (E1-R3).
Name three floating-point folding pitfalls.
x + 0.0 ≠ x for x = −0; x × 0.0 is NaN for NaN/∞ and −0 for x < 0; (1 + 1e16) − 1e16 = 0 but 1 + (1e16 − 1e16) = 1 (no reassociation); host x87 double rounding (Proposition 13.1.14).
Complexity of worklist constant folding?
O(n + u) folds and re-examinations for n instructions and u uses: each instruction is folded at most once and re-queued at most once per operand change (Theorem 13.1.13).
hand-written-combiner¶
What is the InstSimplify/InstCombine contract?
A simplifier returns an existing value (operand, dominating instruction or constant) and never creates instructions; a combiner may create instructions, must not grow the instruction count (except replacing expensive ops) and must emit canonical forms (Definition 13.2.3).
Worklist invariant of a peephole engine with depth-2 patterns?
Every instruction to which a rule might apply is on the worklist; after a rewrite push the new instruction, its users and the users' users (Algorithm 13.2.4).
Cost of a sequential hand-written combiner?
O(s · m · ℓ) for s worklist pops, m rules tried per opcode, pattern size ℓ; compiled and hand-ordered, so fast in practice.
Why does a correct peephole engine produce a refinement?
Each rule is valid (its result refines its pattern), refinement is a congruence for SSA replacement, and it is transitive, so each step and the whole sequence refine the input (Theorem 13.2.7).
pattern-matcher¶
What does m_Deferred(X) do in LLVM's PatternMatch?
Matches the value that X was bound to earlier in the same pattern, at match time: m_Add(m_Value(X), m_Deferred(X)) is "X + X".
Soundness and completeness of recursive pattern matching?
Match(L, v) returns σ iff L matches v under σ, else fail (Lemma 13.2.8); first occurrence of a variable binds, later ones compare.
Cost of one embedded pattern match?
O(ℓ) for pattern size ℓ; O(2^c ℓ) with c commutative (m_c_*) nodes; usually the root opcode test fails first, O(1).
Why embed patterns in C++ (PatternMatch) instead of writing if/dyn_cast chains?
Rules read like the math and are compiled to the same code; but preconditions and flags remain ad hoc C++, so rules cannot be listed or verified as data.
pattern-dsl¶
Examples of external pattern DSLs in production compilers?
GCC match.pd compiled by genmatch; Cranelift ISLE (mid-end rules and lowering); LLVM GlobalISel combiner rules in TableGen.
What does compiling a rule set into a decision tree preserve?
Rule priority: for every input the tree returns the first rule (in priority order) that matches and whose precondition holds (Theorem 13.2.9).
Cost of matching with a decision tree?
O(d): each position is tested once on the way down (d = tree depth ≤ largest pattern), independent of the number of rules; tree size ≤ sum of pattern sizes.
Main advantage of rules as data?
They can be verified (Alive, Crocus for ISLE), listed and counted; adding a rule needs no new C++. Cost: infrastructure, and an interpreted DSL is slower (lab: 75–95 vs 25–40 ms).
enumerative-superopt¶
What does an enumerative superoptimizer (Massalin) do?
Enumerates programs over an instruction set I and constants K by increasing length, filters with test vectors, and fully verifies survivors; the first verified one is a shortest (Algorithm 13.3.3, Theorem 13.3.9).
Why must a superoptimizer verify after test vectors?
Tests only sample inputs; Massalin's and GSO's results were checked by simulation and "might be incorrect with a very small probability". A full check (enumeration or SMT) makes the result sound.
Cost of enumerative superoptimization?
Exponential in the length L: ∏_{j<L} |I| (a + k + j)² programs for a arguments and k constants; practical up to L ≈ 4–5.
What did Bansal and Aiken add to superoptimization?
A peephole superoptimizer: enumerate short windows from training programs, look up cheaper equivalents by fingerprint in a database, prove them with a SAT solver, and store them as a rewrite table (Algorithm 13.3.4).
stochastic-superopt¶
What is STOKE's cost function?
c(R) = eq(R; T) + perf(R): eq counts differing output bits over the tests (Hamming distance), perf estimates latency (Algorithm 13.3.5).
STOKE's acceptance probability for a proposal with cost change Δ?
min(1, e^(−βΔ)) (Metropolis–Hastings); the chain's stationary distribution is ∝ e^(−β c) if proposals are symmetric (Theorem 13.3.10).
Why accept worse proposals in STOKE?
To escape local minima: with probability e^(−βΔ) the chain climbs, so it can reach distant low-cost programs; improvements are always accepted.
Guarantees and cost of STOKE?
Verified results but no optimality; an unbounded random walk (minutes to hours), able to reach long sequences enumeration cannot.
synthesis¶
What is CEGIS?
Counterexample-guided inductive synthesis: alternate Synth(E) (find holes consistent with examples E) and Verify (find an input where the candidate fails, add it to E) until Verify finds none (Algorithm 13.3.6).
Termination and soundness of CEGIS?
Sound: a result passed full verification. On a finite domain D it terminates within |D| iterations, since each adds a new input (Theorem 13.3.11).
What does Souper do?
Extracts integer dataflow fragments from LLVM IR and asks an SMT solver for a cheaper refinement (a constant, an existing value, or a small synthesized expression); used offline to find missing InstCombine rules.
What constant does CEGIS find for udiv i16 x, 515, and where else does it appear?
trunc((zext32(x) · 65155) >> 25): the Granlund–Montgomery magic number with ℓ = 9 (Lesson 13.7).
learned-rules¶
What is the weakest precondition of a generalized rule?
The set of constant values and widths for which every instance is a refinement; a precondition P is sound if P ⇒ WP and weakest if P ⇔ WP (Definition 13.3.7).
How does Alive-Infer / Hydra turn a concrete rule into a compiler rule?
Replace literals by symbolic constants, find expressions for derived constants, learn a predicate separating positive from negative examples, then verify for all widths (Algorithm 13.3.8).
What does verification catch in learned rules?
Over-generalization: e.g. (x << y) >>s y → x fails at i2 (x = −2, y = 1); a verified sound precondition makes every allowed instance valid (Proposition 13.3.12).
Cost of generalizing and verifying a rule?
Dominated by verification per width (up to 64 widths, SMT per width): seconds to minutes per rule.
canonical-forms¶
What is a canonical form in a peephole optimizer?
One chosen spelling per class of equivalent instructions: constants on the right, operands by complexity, strict predicates against constants, sub C as add −C (Definition 13.4.2).
What does InstCombine's getComplexity return?
0 for undef/poison, 1 for other constants, 2 for casts, neg, not and fneg, 3 for arguments and other instructions; commutative operands are sorted by it.
Why canonicalize before other rules?
Each rule has to match one form instead of all syntactic variants (half the patterns for one commutative node), and value numbering sees equal things as equal (Proposition 13.4.6).
Cost of canonical operand ordering?
O(1) per instruction, O(n) per pass (Algorithm 13.4.4).
rewriting¶
Newman's lemma?
A terminating rewrite system is confluent iff it is locally confluent (Theorem 13.4.7).
What is a critical pair?
An overlap of two rules' left sides (one unifies with a non-variable subterm of the other); the two one-step results form the pair. All joinable ⇒ locally confluent (Theorem 13.4.8).
How do you prove a rule set terminates?
Give a well-founded measure that every rule strictly decreases, e.g. μ = (I, S, A, M) lexicographically for R1–R17 (Theorem 13.4.9).
What does Knuth–Bendix completion do, and what does it cost?
Orients non-joinable critical pairs into new rules until all pairs join; checking pairs is O(m²ℓ²) unifications, completion may diverge (Algorithm 13.4.5).
Is R1–R17 confluent?
Not once flags count: R2 and R9 on add (add nsw y, 5), 0 give add nsw y, 5 vs add y, 5; both refine the source, E2's priority makes the result deterministic.
lvn¶
What is the key of an instruction in LVN?
(opcode, type or predicate, value numbers of the operands), with commutative operands sorted; flags are not part of it (Definition 13.5.2).
LVN invariant?
Every numbered value, when not poison, equals the denotation of the key recorded for its number (Lemma 13.5.11).
Why must LVN intersect flags on a hit?
Replacing a flag-free add x, y by an earlier add nsw x, y makes overflowing inputs poison; keeping only the common flags (andIRFlags) makes the replacement a refinement (Theorem 13.5.12).
Cost of local value numbering?
O(n) expected per block with hash tables (O(n log n) with ordered maps).
memory-vn¶
What is a memory version in LVN?
A counter bumped by every store and every instruction that may write memory; loads are keyed by (type, VN(ptr), version) (Definition 13.5.4).
How does store-to-load forwarding work with memory versions?
A store of v to p enters v under the key a load of p would have after the store; a later load of the same type from the same address number finds it (Algorithm 13.5.5).
Why are memory versions sound without alias analysis?
Any possible write bumps the version, so a load key can only hit an entry from the same version, where no write happened in between (Theorem 13.5.13).
Cost of memory in LVN, and its LLVM counterpart?
O(1) per memory operation (one counter); EarlyCSE's CurrentGeneration, refined with MemorySSA.
dag¶
What is the DAG of a basic block?
Leaves for initial values and constants, one interior node per distinct (op, children), labels for the variables currently holding each node (Definition 13.5.6).
What does DAG construction find, and what does reassembly add?
Common subexpressions (same as LVN) plus, for non-SSA code, dead nodes (no live label) and freedom to reorder; reassembly emits needed nodes children-first (Algorithms 13.5.7–13.5.8).
Cost of building a block DAG?
O(n) expected with a hash (memo) table; choosing the best evaluation order for registers is NP-hard in general (with common subexpressions).
Where does LLVM build block DAGs?
SelectionDAG: one DAG per block, CSE through the FoldingSet CSEMap in getNode.
dce¶
When is an instruction trivially dead?
No uses, not a terminator or EH pad, no side effects (no memory writes, cannot unwind) and guaranteed to return (Definition 13.5.9).
Why does worklist DCE miss dead cycles?
A phi and an add that only use each other each have a use, so neither is trivially dead; aggressive DCE marks from effects and sweeps the rest.
Cost of worklist DCE?
O(n + u): each instruction is deleted once and each operand edge re-queues at most one instruction (Theorem 13.5.15).
Why may DCE delete an unused sdiv that might divide by zero?
Removing UB is a refinement (Definition 13.8.2); the deleted instruction had no other effect.
reassociation¶
Briggs–Cooper rank of a value?
Constants 0, arguments 1, opaque instructions (phi, load, call) R(B), the 1-based RPO number of their block, other expressions the max of their operands' ranks (Definition 13.6.2).
What does rank-based reassociation build?
For each add/mul/and/or/xor tree (internal nodes: same opcode, single use, same block), a left-deep chain over the leaves sorted by (rank, position), constants folded into one last operand (Algorithm 13.6.3).
Which flags survive reassociation?
None, except add nuw if every node had nuw and or disjoint if every node had disjoint; nsw never survives (Theorem 13.6.8).
Why sort by rank?
Low-rank (loop-invariant) operands combine first at the bottom of the chain, exposing invariant subexpressions to LICM and constants to folding (Theorem 13.6.9).
Cost of rank-based reassociation?
O(n + Σ_T k_T log k_T) for ranks plus sorting each tree's k_T leaves.
tree-height¶
Completion time of a tree with arrival times?
T = max_j (a_j + d_j), where d_j is the depth of leaf j and each operation takes one unit (Definition 13.6.4).
Greedy tree-height reduction?
Repeatedly combine the two earliest-ready values (Huffman-style); the result has minimal completion time (Algorithm 13.6.5, Theorem 13.6.10).
Minimal height of an add tree over n leaves at time 0?
⌈log₂ n⌉, versus n − 1 for the left-deep chain (Corollary 13.6.11).
Cost and trade-off of tree-height reduction?
O(k log k) per tree with a priority queue; balanced trees keep more values live, so it runs late (MachineCombiner) with real latencies.
mul-const¶
What is the non-adjacent form (NAF) of a constant?
The signed-digit representation with digits in {−1, 0, 1} and no two adjacent non-zeros; it has minimal weight among signed-digit forms (Proposition 13.7.8).
How many add/subtract operations does multiplication by C via the NAF need?
weight(NAF(C)) − 1, e.g. 119 = 2⁷ − 2³ − 1 needs 2 (binary would need 5).
Cost of computing a NAF chain?
O(b) for a b-bit constant; production compilers compare it with factoring (45 = 9 × 5 → two x86 lea) and a single mul under a cost model.
div-const¶
Magic multiplier for unsigned division by d at width N?
m = ⌈2^(N+ℓ) / d⌉ with error e = m·d − 2^(N+ℓ); q = ⌊m·x / 2^(N+ℓ)⌋ (Definition 13.7.3).
Exact criterion for a magic multiplier?
⌊m x / 2^(N+ℓ)⌋ = ⌊x/d⌋ for all x < 2^N iff e · n_c < 2^(N+ℓ), n_c = 2^N − 1 − (2^N mod d) (Theorem 13.7.6); Granlund–Montgomery's e ≤ 2^ℓ is the sufficient special case.
When is the add fix-up needed?
When the smallest valid m needs N + 1 bits: multiply by m − 2^N, then q = ((x − h) >> 1 + h) >> (ℓ − 1) with h the high product (Theorem 13.7.9; LLVM's IsAdd).
Cost of division by a constant?
O(N) to compute the magic number at compile time; at run time 1 multiply-high plus a few shifts/adds instead of a 20–90-cycle divide.
refinement¶
Definition of refinement for straight-line functions?
t refines s if for every input, every behavior of t is in the closure of s's behaviors: anything if s may have UB; a value v if s may return v or poison; poison only if s may return poison (Definitions 13.8.2, 13.8.4).
Why is refinement a preorder, and why does that matter?
It is reflexive and transitive (Theorem 13.8.3), so a pipeline of refining passes refines its input.
Why may an optimizer replace one use of an SSA value by a more defined one?
Every instruction is monotone in definedness (Lemma 13.8.10), so refinement is a congruence for SSA replacement (Theorem 13.8.11).
Cost of deciding refinement?
NP-hard in general for fixed widths (SMT); by enumeration, exponential in the total input bits (Lesson 13.9).
ub-poison¶
Poison vs immediate UB?
Poison is a value that propagates through operations and becomes UB only when it reaches a side effect or a branch; immediate UB (division by zero, branch on poison) is undefined at once.
What does freeze do, and why must it not be duplicated?
freeze poison yields an arbitrary but fixed value; two freezes may choose differently, so replacing one freeze used twice by two freezes can produce new values.
Why can't select be turned into a branch without freeze?
select with a poison condition is poison, but br on poison is immediate UB; branching on freeze(c) is a refinement.
Order of poison, undef and freeze in definedness?
poison ⊒ undef ⊒ freeze ⊒ any concrete value: each may be refined by the ones to its right (Proposition 13.8.12).
flags¶
Which LLVM flags generate poison?
nsw, nuw (add sub mul shl trunc), exact (udiv sdiv lshr ashr), disjoint (or), samesign (icmp), nneg (zext, uitofp): the result is poison when the promised property fails.
How do you decide whether a rewrite keeps a flag?
Write both results as exact integer expressions of the inputs; the flag survives iff the target's condition follows from the source's flags for every input (Algorithm 13.8.7).
Flags of R9 (x + C1) + C2 → x + (C1 + C2)?
A flag survives iff both adds have it and C1 + C2 does not overflow in its sense (Theorem 13.8.14).
Flags of R10 mul x, 2^k → shl x, k?
nuw kept; nsw kept iff k < N − 1 (at k = N − 1, 2^k is negative as a signed constant) (Theorem 13.8.13).
fast-math¶
What does nsz license?
The sign of a zero operand or result may be flipped, so fadd x, +0.0 → x becomes valid (it fails for x = −0 otherwise) (Definition 13.8.8).
Which FP identities hold without any flags?
x + (−0.0) = x and x − (+0.0) = x, for every x including −0 and NaN (Proposition 13.8.16 (a)).
Value-based vs rewrite-based fast-math flags?
nnan, ninf, nsz change the value semantics (poison / sign choice); reassoc, arcp, contract, afn license rewrites that change rounding, and only if every instruction of the rewritten expression carries the flag (Definition 13.8.8, Theorem 13.8.17).
What does clang's default -ffp-contract=on do to a * b + c?
Emits llvm.fmuladd: the back end may fuse into one rounding (FMA) or keep two.
smt¶
What is Alive2's refinement query?
∃ inputs, poison masks, target choices ∀ source choices: ¬ub_s ∧ (ub_t ∨ (¬poison_s ∧ (poison_t ∨ val_s ≠ val_t))); unsat means valid (Definition 13.9.2, Theorem 13.9.9).
In which order does Alive check a rule, and why split it?
UB, then poison, then value: each is a separate SMT query, so a counterexample names the failing check (Algorithm 13.9.3).
Cost and limits of SMT-based verification?
NP-hard; seconds per rule at fixed widths, timeouts on wide mul/div; complete only for the widths checked (every width up to 64 in Alive).
What does Alive-FP add?
Encodings of IEEE formats and fast-math flags, so FP peephole rules can be verified; proofs do not transfer between FP formats.
bounded¶
What is bounded exhaustive checking?
Run source and target on every input of small widths (all bit patterns plus poison, all freeze choices) and compare behavior sets (Definition 13.9.5, Algorithm 13.9.6).
Why is a bounded check not a proof for all widths?
Rules can depend on N: and x, 255 → x holds for N ≤ 8 and fails at 9; R11 fails only at i1 (Proposition 13.9.11).
Which rules are bitwidth independent?
Rules built only from and/or/xor with constants 0 and −1 and no flags: valid at all N iff valid at N = 1 (Proposition 13.9.11 (a)).
Cost of bounded exhaustive checking?
Exponential in total input bits: ∏ (2^w + 1) inputs (+ poison), e.g. 66 049 for two i8 arguments; instant at 8 bits.
translation-validation¶
Translation validation vs verified compiler?
TV checks each compilation after the fact and may say unknown (Pnueli 1998, Necula 2000, Alive2's opt plugin); a verified compiler (CompCert) proves every compilation correct once, with fewer optimizations.
What does CompCert's main theorem state?
If compilation succeeds, every behavior of the assembly is a behavior of the C source (backward simulation), for sources without UB (Theorem 13.9.12 (b)).
Cost of translation validation?
One refinement check per pass per function per compilation (SMT: seconds, timeouts possible), versus a one-time proof effort for a verified compiler.
What did Csmith find about CompCert?
Wrong-code bugs in its unverified parts (front end) but none in the verified middle end (Yang et al. 2011).