VCR-DEC-001: graph-colouring allocator across if/else joins — measured, flag-off (#242) - #891
Merged
Merged
Conversation
…ns (#242) Widen the flag-off SYNTH_GRAPH_ALLOC spike past whole-straight-line functions to colour a whole BRANCHY function at once. - liveness.rs: validate_cfg_rewrite — the CFG-lifted translation validator. The straight-line Rideau/Leroy pairwise trace-equality check lifted to a backward MUST-fixpoint over the CFG (union at joins, least fixpoint from the exit seeds, back edges included). Control-flow instructions must be byte-identical on both sides, so flag equality at a Bcc follows from its Cmp's use equations. - liveness.rs: cfg_exit_observable — ONE definition of the exit contract, consumed by both the validator (as its seed) and the pass (as sink live-out). Deliberately not derived from 'registers either side writes': that makes the seed depend on the rewrite, which is how a pass shrinks its own acceptance test. The v0.50 attempt failed exactly there. - graph_alloc::joins — label-form CFG (pop{..,pc} IS a return sink, the #888 class), cross-block webs via a reaching-def fixpoint, web interference from CFG liveness (dead defs interfere with live-after too), Push/Pop register lists identity-pinned (#888), #677 absent- colour blockers, Chaitin/Briggs colouring, independent edge re-check, then validate_cfg_rewrite as the acceptance gate. Flag stays OFF: frozen anchors 10/10 unchanged. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…r bias (#242) The lane's DELIVERABLE: vcr_dec_001_join_alloc_measure.py compares the join-aware colourer against the shipping greedy/segment allocator over the whole ARM repro corpus — .text bytes from the ELF SYMTAB (never disasm text, #850) and SOUND per-function cycle BOUNDS from --emit-wcet. Two defects the measurement found and this commit fixes: 1. edge-recheck declined 16 corpus functions on '1(R1)~16(R1) -> R1/R1': two PINNED webs of one register. A pinned web's register is not a colourer choice, so that is the original's own behaviour, not a conflict. The edge exists only because the conservative exit contract makes a register live at the return with no unifying use. Skip edges whose both endpoints are pinned (the shipping pass exempts the same pair class). 2. chaitin_core's lowest-free-colour select repacked whole functions into R0/R1, and on loop_param_bound_663::sum_const that landed the loop's compare result on the register a later forward_stack_reloads was forwarding through: two movs became two ldrs INSIDE the loop, +2 bytes and +22 CYCLES. A whole-function allocator that ignores what the rest of the pipeline is about to do is not automatically better than a greedy one. color_webs_biased prefers (1) the web's own register when already caller-saved, (2) the lowest free caller-saved colour — the actual objective, evacuating R4-R8 so the prologue can shrink, (3) its own register, (4) lowest free. chaitin_core is deliberately NOT changed: it is shared with the shipping pass, so a different select order there would move the frozen bytes. Measured (relocatable / label-form, 617 functions, 275 applied): bytes 40822 -> 40776 -46 (-0.11%) 8 shrank, 1 grew wcet 13866 -> 13841 -25 (-0.18%) 7 shrank, 0 grew Before the bias the same corpus was -22 bytes / +4 CYCLES. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Increment 1 could claim execution correctness TRANSITIVELY (flag-on bytes were identical to shipping BY CONSTRUCTION). Increment 2 diverges, so that claim is retired and replaced by real gates. - scripts/repro/vcr_dec_001_join_alloc_execution_differential.py (NEW, WIRED into ci.yml in this commit): unicorn runs the flag-ON image and compares return value + linear-memory window against wasmtime over every join shape the allocator reaches. Per function it first asserts ENGAGEMENT (applied AND flag-on bytes actually differ) so it can never pass by re-testing the shipping compiler, and it asserts RA-003 Consistent from SYNTH_RA003_VERBOSE rather than from the exit code. 38/38 checks, 13 engaged functions. PROVEN non-vacuous by MUTATION, and the mutation is the lane's point: emptying cfg_exit_observable -- the exit contract the pass and its own CFG validator SHARE -- while removing the churn bias that masks it emits code leaving the return value in the wrong register. validate_cfg_rewrite AND VCR-RA-003 both ACCEPT it; only this gate catches it (16 wrong results). #872 made concrete: a validator that shares its pass's dataflow is necessary, not sufficient. - vcr_dec_001_graph_alloc_differential.py: property (3) 'flag-on == flag-off corpus-wide' is now FALSE and is replaced by (3a) a fixture the allocator did NOT apply to must stay byte-identical, (3b) an applied one must not GROW, (3c) >=2 fixtures must diverge or increment 2's reach regressed. - ci.yml wiring uses and an awk assertion on the machine-readable summary requiring passed == total, total > 0 AND engaged > 0. Verified red-first against 0/0, 30/38 and ENGAGED=0. - 6 new unit gates incl. the cross-arm colouring (asserts a NON-identity rewrite), a RED one-armed rename across a join that the straight-line validator structurally cannot see, a rewritten-branch reject, an exit-observable clobber reject, and the #888 mid-stream pop{..,pc} return-sink shape. cargo fmt --check / clippy --workspace --all-targets -D warnings / test --workspace: all exit 0. Frozen anchors 10/10. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…#242) The measurement IS the deliverable, so the numbers and the verdict are in the entry: -46 bytes / -25 worst-case cycles over 617 corpus functions (275 applied), 8 shrank / 1 grew / 0 cycle regressions -- and the honest read is 'not yet' for a v0.54 flip, with the limiting factor named (reach, not soundness) and the decline histogram that makes the next increment schedulable. claim_check: 34/34 hold. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…#242) The early return was `orig.is_empty() || blocks.is_empty()` -> Ok. An EMPTY CFG for a NON-empty stream therefore validated every rewrite vacuously -- the same class of failure as the v0.50 join attempt's two `entry_seed` hacks. Drop the `blocks.is_empty()` disjunct so the case falls through to the structural tiling check, which rejects it, and add a regression test covering both the empty CFG and a CFG that leaves instructions unwalked. Also refresh the module header, which still described increment 2 as 'NAMED, NOT in this spike' -- the doc-honesty class a cold review caught in v0.51 (shipped features still described as not yet done). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.53 lane L5, the North Star allocator lane. Flag-off (
SYNTH_GRAPH_ALLOC); frozen anchors 10/10; nothing runs unless the flag is set.The deliverable: measured delta vs greedy
617 corpus functions, 275 applied. Bytes from the ELF symtab; cycles are synth's own sound
--emit-wcetbounds (identical modelling assumptions, not hardware):.textbytesVerdict for a v0.54 flip: not yet — and the limiting factor is REACH, not soundness. Declines are now a named histogram rather than one bucket: 164 unmodeled i64/FP op, 68 call/call-indirect, 73 single-block, 10 unreachable-block, 9 numeric-branch. Calls and numeric branches are the two schedulable next increments.
Two defects found while building it
chaitin_core's lowest-free-colour select repacked into R0/R1 and landed a loop compare result on a registerforward_stack_reloadswas forwarding through — twomovs became twoldrs inside the loop, +22 cycles. Before the fix the corpus measured −22 B / +4 cycles.color_webs_biasednow prefers a web's own register when already caller-saved.chaitin_coreis untouched (shared with the shipping pass).The oracle finding worth reading
validate_cfg_rewritelifts the trace-equality validator to a backward must-fixpoint over the CFG and computes its own exit contract, so the pass cannot hand it a weakened seed (the v0.50 failure mode).Proven non-vacuous by mutation — and the result matters beyond this lane: emptying the shared exit contract emits code that leaves the return value in the wrong register, and
validate_cfg_rewriteAND VCR-RA-003 both ACCEPT it. Only execution catches it (16 wrong results). Two independent validators, one shared blind spot — the #872 lesson generalising. Hence the CI-wired execution differential (unicorn vs wasmtime, 38/38 checks, 13 engaged functions).Also:
Push/Poplists identity-pinned, mid-streampop {…,pc}treated as a return sink, and a vacuity hole (empty CFG →Ok) closed with a test.RA-003
Corpus sweep both paths: 0 violations, 431/447
Consistent— the sweep distinguishes "no violation" from "not checked".Refs #242.