0%

s11 — Fast Tier: Schedule + Register Allocation + Symbolic Checker

Goal

The production fast-tier allocator: schedule pass, liveness, greedy linear scan over per-arch masks with spill/reload, block-param-native — and the symbolic checker that PROVES each allocation, landing in the same section as the allocator (never after).

Implementation Sketch

  • Schedule pass: topological intra-block ordering ahead of allocation (Go precedent: regalloc quality collapses without it); deterministic (RPO blocks, stable in-block order).
  • Liveness: backward per-block live-sets over BIR/MIR with block params (no phi insertion — params ARE the merge points; regalloc2 proves block-param-native allocation works).
  • Allocator: single implementation parameterized by ArchConfig masks (u64 covers all 5: SysV 16+16, AAPCS64 31+32, RV64 32+32 incl. fa, s390x 16+16, wasm virtual 16+32); greedy scan with farthest-next-use (Belady-like) spill choice; caller/callee-saved handling per ABI; parallel-move resolver for block-param edge moves (cycle-breaking with one scratch).
  • Spill/reload: frame-slot assignment, per-target addressing (s390x displacement limits, riscv64 imm12 ranges respected).
  • OnWasmStack: wasm values consumed exactly-once-next get the stack flag; emitter skips local.get/set (Go trick).
  • Symbolic checker (regalloc2 checker model): independent pass over post-alloc MIR proving every use reads the location holding the right value along EVERY path (dataflow over locations); runs under ORI_VERIFY_ARC=1 in tests and always in CI; checker failures are hard errors.

Test Strategy

  • Matrix: register-pressure shapes {no-spill, spill-heavy, call-heavy (caller-saved churn), loop-carried, block-param cycles (swap shape), wasm-stack} x all 5 targets — parity-asserted execution.
  • Semantic pin: the parallel-move cycle fixture (a,b = b,a across an edge) pins correct swap resolution per target.
  • Negative pin: a deliberately corrupted allocation (test-only hook) is REJECTED by the symbolic checker — the checker negative pin is mandatory before this section closes.
  • Property tests: random pressure programs; checker green over the corpus; debug+release.

Work Items

  • Schedule pass (deterministic topo order) + tests.
  • Liveness + greedy linear-scan allocator over ArchConfig masks with Belady spill heuristic; block-param parallel-move resolver with cycle breaking.
  • Spill/reload with per-target addressing-range correctness (s390x/riscv64 displacement limits).
  • OnWasmStack assignment + emitter collapse.
  • Symbolic allocation checker (independent location-dataflow proof) wired into tests + CI, with the corrupted-allocation negative pin.
  • Pressure-shape matrix x 5 targets green with parity; property corpus checker-clean; debug+release green.