docs(vcr-ra): map the register-exhaustion recovery ladder (#242)#476
Merged
Conversation
Roadmap artifact, no codegen change. The north star (#242) replaces synth's single-pass register allocator with a verified one; the clearest spec of what that allocator must do is the failure-recovery ladder the current allocator has accreted (arm_backend.rs select_direct): base attempt -> optimized-decline (#120) -> spill-on-exhaustion (#242 3b-lite) -> param frame-backing (#204) -> promotion-off fallback (#474/#475). Each rung is reached only after a recoverable register exhaustion, so the base-attempt corpus is untouched (frozen gate green). Maps each rung to the issue that added it and the failure it catches, ties fixtures to rungs (only rung 4 / promotion_exhaustion_fallback is confirmed load-bearing; the rest are by design intent pending a per-rung counter), and states the VCR-RA acceptance implication: a correct-by-construction allocator with spilling collapses rungs 2-4 into "allocation succeeds" — the ladder then survives only as a never-firing defense-in-depth assertion. Refs #242, #474 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 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.
Roadmap artifact, no codegen change (frozen gate green).
The north star (#242) replaces synth's single-pass register allocator with a verified one. The clearest spec of what that allocator must do is the failure-recovery ladder the current allocator has accreted in
arm_backend.rs::select_direct:Each rung is reached only after a recoverable
register exhaustion, so the base-attempt corpus is untouched (that's why each was bit-identical when it landed, and why the frozen gate stays green).Why it matters for #242: rung 4 existing at all is a direct symptom of the single-pass allocator — local promotion is an optimization that can turn a working compile into a failure, "fixed" by a retry that drops the optimization. A correct-by-construction allocator with spilling collapses rungs 2-4 into "allocation succeeds": no exhaustion Err, no ladder. So the VCR-RA acceptance bar is that every function needing rungs 2-4 today allocates on the first pass under the verified allocator, the ladder surviving only as a never-firing assertion.
Honest scoping: only rung 4 is confirmed load-bearing here (its fixture fails without the rung); the other fixture→rung mappings are design-intent pending a per-rung counter (noted as the natural next measurement, env-gated/frozen-safe).
Refs #242, #474
🤖 Generated with Claude Code