Skip to content

feat: graph colouring — VCR-RA-001 allocation decision (#242) - #270

Merged
avrabe merged 1 commit into
mainfrom
feat/vcr-ra-graph-coloring
Jun 5, 2026
Merged

avrabe merged 1 commit into
mainfrom
feat/vcr-ra-graph-coloring

Conversation

@avrabe

@avrabe avrabe commented Jun 5, 2026

Copy link
Copy Markdown
Contributor

North-star increment — VCR-RA-001 (side-by-side, unwired)

Completes the analysis → decision core of the register allocator, on top of the merged interference graph (#269). No codegen path touched.

What

liveness::color_graph(graph, k) -> ColorResult — Chaitin/Briggs graph colouring with optimistic spill:

  1. Simplify — repeatedly remove a node of degree < k onto a stack (it can always be coloured after its neighbours, which use ≤ k−1 colours).
  2. Spill — if every remaining node has degree ≥ k, optimistically push the highest-degree one (Briggs: often still colourable in practice).
  3. Select — pop in reverse, assign the lowest colour no neighbour uses; a node that finds no free colour in 0..k is an actual spill.

Returns Colored(BTreeMap<Reg, colour>) or Spilled(BTreeSet<Reg>).

Why it matters

This is precisely the decision synth's single-pass allocator cannot make — it hard-fails on register exhaustion instead of spilling, which is what forces the reciprocal-mult cost-gate (#209/v0.11.20). With the colour/spill decision in hand, the eventual wiring can spill under pressure instead of bailing.

Soundness

Pure algorithm over the graph, zero non-test callers, no emitted-byte path touched ⇒ every frozen differential fixture (control_step 0x00210a55, flight_algo 0x07FDF307, divseam) is bit-identical by construction.

Tests

  • 5 colouring units: empty graph; 2-colour a path; K4 spills at k=3; K4 colours at k=4 (all-distinct); k=0 spills.
  • Extended the real-selector-output test: actual codegen is colourable within the R0–R8 pool (k=9) and the returned colouring is valid (adjacent nodes differ) — the current allocator already fits it, so a principled colouring must too.

Verification

cargo test -p synth-synthesis (302 lib + suites) green · clippy clean · fmt clean.

Remaining for VCR-RA-001: spill-code insertion → precolouring reserved regs → ABI-exit-liveness union → virtual-reg selector output → oracle-gated wiring.

🤖 Generated with Claude Code

…on (#242)

Complete the analysis→decision core of the allocator on top of the merged
interference graph (#269): color_graph(graph, k) -> ColorResult via
Chaitin/Briggs with optimistic spill.

  1. SIMPLIFY — repeatedly remove a node of degree < k onto a stack (it can
     always be coloured after its neighbours, which use ≤ k−1 colours).
  2. SPILL    — if every remaining node has degree ≥ k, optimistically push
     the highest-degree one (Briggs: often still colourable in practice).
  3. SELECT   — pop in reverse, assign the lowest colour no neighbour uses;
     a node that finds no free colour in 0..k is an actual spill.

Returns Colored(BTreeMap<Reg,colour>) on success or Spilled(BTreeSet<Reg>)
with the nodes a real allocator would rewrite to stack slots and retry.
This is precisely the decision synth's single-pass allocator CANNOT make —
it hard-fails on register exhaustion instead of spilling, which is what
forces the reciprocal-mult cost-gate (#209/v0.11.20).

Soundness: pure algorithm over the graph, zero non-test callers, no codegen
path touched => every frozen differential fixture (control_step 0x00210a55,
flight_algo 0x07FDF307, divseam) is bit-identical BY CONSTRUCTION.

Tests: 5 colouring units (empty, 2-colour a path, K4 spills at k=3, K4
colours at k=4, k=0 spills). Extended the real-selector-output test to
assert actual codegen is colourable within the R0–R8 pool (k=9) and the
returned colouring is valid (adjacent nodes differ).

Remaining for VCR-RA-001: spill-code insertion -> precolouring reserved
regs -> ABI-exit-liveness union -> virtual-reg selector output ->
oracle-gated wiring (the step that finally removes the hard-fail).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@avrabe
avrabe merged commit d358603 into main Jun 5, 2026
13 checks passed
@avrabe
avrabe deleted the feat/vcr-ra-graph-coloring branch June 5, 2026 08:35
@codecov

codecov Bot commented Jun 5, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 94.94949% with 5 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/liveness.rs 96.66% 3 Missing ⚠️
crates/synth-synthesis/src/instruction_selector.rs 77.77% 2 Missing ⚠️

📢 Thoughts on this report? Let us know!

avrabe added a commit that referenced this pull request Jun 5, 2026
…it (#242) (#272)

The register-allocator analysis+decision layer is merged and unwired
(reg_effect → cfg_liveness #268 → interference_graph #269 → color_graph
#270 → color_graph_precolored #271), all bit-identical-by-construction
because nothing calls them.

The wiring is categorically different: it makes the allocator drive codegen,
so it CHANGES emitted bytes and needs the full differential oracle gate. This
design note sequences that crossing before any of it is written:

 - identifies the hard-fail sites the wiring replaces (instruction_selector.rs
   ~362/388/609/4699/4765 — the exhaustion errors that force the cost-gates),
 - the frozen-behaviour invariant (control_step 0x00210A55 / flight_algo
   0x07FDF307 / divseam bit-identical at every sub-step; flag default-off),
 - 5 oracle-gated sub-steps (verify_allocation oracle → spill-cost ranking →
   virtual-reg selector output flag-gated → spill-code insertion → wire-in +
   per-function flip where the differential proves no-regression),
 - the per-step oracle gate, and the non-goals (coalescing/splitting deferred).

Design leads code: the next bounded, safe piece is step 1 (verify_allocation,
still unwired); the rest is the planned consequential effort.

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant