Deferred Allocation/Deletion Formal Modeling and Bug Fixes

[lightsighter]

This PR adds a TLA+ model of Realm's deferred instance allocation/deletion logic (LocalManagedMemory), uses it to find and adjudicate several long-standing bugs — including the event-loop deadlock suspected in the original design talk — and fixes them with a design that was model-checked before being ported to C++. The fixes ship with API-level regression tests that provably detect the old bugs: run against main, they reproduce the deadlock and the exact debug assertion the model predicted.

The model (tla/allocation/)

DeferredAlloc.tla models the allocator's three heap states (current/future/release), the pending_allocs/pending_releases queues with their seqid ordering, release reordering (attempt_release_reordering), poisoned-precondition cleanup (remove_pending_release), and event preconditions — transcribed branch-by-branch from mem_impl.cc with line citations (DESIGN.md records the correspondence). The first-fit range allocator is abstracted to a tag→interval map proven equivalent to BasicRangeAllocator's address-ordered first fit. Clients are constrained by the documented contract: topologically sorted requests (no back edges), destroy preconditions incorporating the created event. C++ asserts are modeled as checkable invariants rather than assumptions, so assert-reachable states are found, not pruned. Instance redistricting is deferred to a v2 model (FUTURE-VERIFICATION.md).

./tla/allocation/run.sh runs the local config matrix in seconds-to-minutes and is the standing regression oracle for future mem_impl.cc changes.

Bugs found and fixed (details in tla/allocation/bugs/)

• BUG-1 — event-loop deadlock from trigger-time ordering (bugs/BUG-1.md). A deferred create is inserted into the release/alloc total order when its precondition triggers, but its e_created was handed out at request time. A release requested in between may legally depend on that e_created; the future-state rebuild counts its space anyway, so Realm funds the allocation from a release that can only happen after the allocation completes — a permanent, silent hang, after the mapper was told InstanceAllocResult{success=true}. Minimal witness: 2 instances + 1 user event (7-state TLC trace).
  Fix: snapshot cur_release_seqid at request time (DeferredCreate::release_seqid_cap); at trigger, admit only against releases at-or-below the cap (canonical-order replay) with a monotone-cap queue guard; a capped miss returns an honest ALLOC_INSTANT_FAILURE instead of hanging.

• BUG-6 — stranded ready release; assert(!it->is_ready) at mem_impl.cc:772 reachable (bugs/BUG-6.md). A reordering-failure pushback can leave a ready release queued behind a non-ready one; the oldest-entry drain then empties pending_allocs, and both cleanup paths are skipped precisely because the queue just emptied. Debug builds abort on the next deferral-needing allocation; release builds silently break the documented release = current + ready releases invariant. A composite of this state with a later reordering swap permanently leaks the stranded range while firing its dealloc notify (the instance-recycling double-tracking class from Fix Instance ID Reuse #442) — no poison involved. TLC witnesses: 9 steps / 3 instances, and 12 steps / 5 instances for the leak.
  Fix: a shared sweep applies remaining ready releases (redistrict-aware) to current_allocator at every pending_allocs→empty transition, restoring the invariant — the cc:772 assert is now genuinely true.

• BUG-5 — trailing allocations dropped by poisoned-release cleanup (bugs/BUG-5.md). remove_pending_release's rebuild replay never revisits pending allocs whose seqid watermark exceeds every surviving release — they are neither failed nor re-funded. Composed with the BUG-1 fix (which makes poisoned releases routine), this strands an admitted allocation forever; TLC found the deadlock the moment the cap fix was modeled without it.
  Fix: after the replay walk, continue the same loop over the remaining allocs — re-place into the rebuilt future state or fail them cleanly. The three fixes are intentionally one change: the cap must not land without the trailing replay.

Behavior change

Allocations that previously "succeeded" by being funded from a not-yet-requested-at-create-time deletion now fail honestly at trigger time. Those successes were unsound promises (the hang above); mappers already handle allocation failure. Unconditioned (NO_EVENT) creates — the dominant case — are bit-identical to the old behavior (verified instruction-level in review).

Verification

• Fix design validated in the model first: full state-space exhaustion at small bounds (e.g. 23.5M distinct states with the complete invariant battery), targeted witnesses for each bug flipping red→green, and a GC-ripple client confirming the deferred-create-funded-by-later-GC pattern still succeeds.
• Scale runs (Slurm, sapling_tlc.sbatch): fixed model violation-free through 7.52B distinct states (depth 11 complete, deep into 12); poison paths clean through 1.9B.
• C++ reviewed against the verified spec function-by-function (two independent passes, zero blocking findings); full test suite green; 4 new regression tests in tests/deferred_allocs.cc — against main they catch the BUG-1 hang, the BUG-6 abort (Assertion failed: (!it->is_ready), mem_impl.cc:772 — exactly the modeled witness), and the inversion hang. This PR also re-wires tests/deferred_allocs.cc into CMake (it had been orphaned), reviving its 16 pre-existing directed tests.

Not in this PR

• BUG-7 (bugs/BUG-7.md): a pre-existing mixed redistrict/plain drain bug in reuse_storage_immediate found during review (memory-safety severity) — fixed separately on mbauer-bug7-reuse-drain.
• Known scope limits, documented in-tree: the request-time snapshot is airtight for owner-node creates (remote-create ordering is a recorded v2 gap), and redistricting/duplicate-release modeling is the v2 campaign (FUTURE-VERIFICATION.md).

[codecov]

Codecov Report

❌ Patch coverage is 29.11392% with 56 lines in your changes missing coverage. Please review.
✅ Project coverage is 30.42%. Comparing base (15b3e9b) to head (ae7ba5f).
✅ All tests successful. No failed tests found.

Files with missing lines	Patch %	Lines
src/realm/mem_impl.cc	29.87%	50 Missing and 4 partials ⚠️
src/realm/inst_impl.cc	0.00%	1 Missing ⚠️
src/realm/inst_impl.h	0.00%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #474      +/-   ##
==========================================
+ Coverage   30.41%   30.42%   +0.01%     
==========================================
  Files         199      199              
  Lines       41282    41337      +55     
  Branches    14779    14982     +203     
==========================================
+ Hits        12554    12575      +21     
- Misses      27488    28305     +817     
+ Partials     1240      457     -783     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.