Scalable Barriers (Again)

[lightsighter]

Rewrites Realm's barrier internals around two tree-structured protocols designed to scale to thousands of nodes, replacing the all-ranks-message-the-owner scheme. Both protocols were designed and formally verified in TLA+ before implementation; the specs, model-checking scenarios, and design documents ship in tla/barrier/ as the normative record.

Design

• Arrival (BarrierArrive.tla, ARRIVAL_PROTOCOL.md): the owner learns an arrival plan from observed traffic and pushes it out; nodes aggregate cumulative counts up the plan tree, staying O(radix) per node in steady state. Deviations (over-arrival, arrivals at unplanned nodes, run-ahead into future generations) trigger per-generation eager flush so no arrival is ever silently stranded; plan changes use an invalidate/new-plan pair with local deferral to resolve their race. Entirely feed-forward: no timers, no polling, no background work.
• Notification (BarrierNotify.tla, NOTIFICATION_PROTOCOL.md): the owner keeps a subscriber set (no learned tree — the multicast layer plans fan-out per send), publishes version-gated membership, and sends trigger notifications as gap-checked deltas; a node that can't apply a delta pulls. Includes departure hysteresis (K=8, adaptive) so the set tracks waiting patterns without timers.

Verification

Every protocol rule (10 arrival + 8 notification) is backed by a mutation battery: disable the rule, and a model-checking scenario chosen for exactly that failure catches it (tla/barrier/battery.py, 26 rows, ~20 min). The models found real bugs before the code did — including a double-count safety bug where re-parenting a node mid-generation counted its arrivals twice, and several liveness strands in plan-switch races — and drove the fixes (pinned report edges, dead-plan install guards, retroactive outsider signaling). They also surfaced one pre-existing bug: alter_arrival_count is documented as persistent across generations but was applied to a single generation; this PR fixes it to match the documented contract (note: behavioral change, and the API previously had zero test coverage anywhere).

Implementation notes

• Barrier migration is removed; reduction barriers keep the existing eager path unchanged.
• One mutex per BarrierImpl; every spec action is one critical section (documented per-action in STATE_AND_LOCKING.md); has_triggered stays lock-free.
• Deviation-path instrumentation counters dump at destroy_barrier — a run's coverage is checkable, not assumed.

Testing

• tests/barrier_scale_test: a 9-phase deviation driver (over-arrival, outsiders, run-ahead, per-generation plan churn, alters, disjoint waiters, poison, seeded chaos) with counter-based exercise proofs; green at 1/2/4 ranks over MPI, TSAN-clean, full suite 839/839.
• New -ll:barrier_plan_radix (default 8, unchanged behavior) lets small-rank runs form deep plan trees, making the plan-switch race windows reachable on a workstation; with radix 2, the deferral and stale-edge paths execute and pass at 4–6 ranks.
• Remaining scale work (2→128 node ladder, two race-window cases that need ≥8 ranks) is specified in tla/barrier/SCALE_TEST_PLAN.md.

[codecov]

Codecov Report

❌ Patch coverage is 0% with 18 lines in your changes missing coverage. Please review.
✅ Project coverage is 33.81%. Comparing base (0b6d486) to head (1a62a12).
✅ All tests successful. No failed tests found.

Files with missing lines	Patch %	Lines
src/realm/barrier_impl.h	0.00%	15 Missing ⚠️
src/realm/runtime_impl.cc	0.00%	3 Missing ⚠️

Additional details and impacted files

@@                   Coverage Diff                    @@
##           mbauer-fix-multicast     #467      +/-   ##
========================================================
- Coverage                 34.94%   33.81%   -1.14%     
========================================================
  Files                       202      202              
  Lines                     44162    45648    +1486     
  Branches                  15266    16012     +746     
========================================================
+ Hits                      15433    15434       +1     
- Misses                    27383    29031    +1648     
+ Partials                   1346     1183     -163     

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

[elliottslaughter]

alter_arrival_count is documented as persistent across generations but was applied to a single generation; this PR fixes it to match the documented contract

I think the documentation is wrong and the behavior as previously written is intentional. Every barrier generation lives as an independent entity and arrival count adjustments don't flow forward.

I don't know that we care: SCR is dead and we don't maintain any active manual CR codes. I just mention it because there may well be applications that rely on the implemented behavior and I personally never found it unintuitive.

[elliottslaughter]

Barrier migration is removed

Again, maybe we don't care, but SCR did rely on this and perhaps manual CR codes would too.

[elliottslaughter]

I'd be curious what the strategy is for keeping the TLA in sync with the C++ (or for that matter, verifying that the ever matched). As far as I know it's a manual process and the formal verification is only as good as your ability to line up the two implementations.

[eddy16112]

What is the difference between this PR and Artem's old scalable barrier implementation?

[lightsighter]

alter_arrival_count is documented as persistent across generations but was applied to a single generation; this PR fixes it to match the documented contract

I think the documentation is wrong and the behavior as previously written is intentional. Every barrier generation lives as an independent entity and arrival count adjustments don't flow forward.

I don't know that we care: SCR is dead and we don't maintain any active manual CR codes.

Note, this pull request does not change the documented semantics. The prior implementation was not faithfully implementing the described semantics. All we're doing here is ensure that the runtime matches the documentation, which in my opinion, is the better semantics for how alter_arrival_count should behave.

I just mention it because there may well be applications that rely on the implemented behavior and I personally never found it unintuitive.

If there was anyone (and I doubt it), they should have reported it as a bug for not matching the documentation. ;)

[lightsighter]

I'd be curious what the strategy is for keeping the TLA in sync with the C++ (or for that matter, verifying that the ever matched). As far as I know it's a manual process and the formal verification is only as good as your ability to line up the two implementations.

If you know of one you let me know. ;) The only one I've got is: ask the LLM to check that the implementation matches the TLA spec. In this case all the code has actually been synthesized from the spec itself (not the other way around) so it's guaranteed to match. We can say something like: always change the spec and then ask an LLM to generate code from it, but there's no way to enforce that.

[lightsighter]

What is the difference between this PR and Artem's old scalable barrier implementation?

I would say that the main way it is different is that it is less buggy. ;) Artem's previous version is still disabled because no one ever went back and fixed all the bugs we were observing with it. This version is getting robustly tested at scale and is passing complex tests with lots of state transitions that exercise all the different states in the TLA+ model, so I have a lot more confidence that it is correct and we'll actually be able to deploy it in practice. Looking at the complexity of the TLA+ models (for both arrivals and notifications) I think it is safe to say that Artem's prior implementation didn't handle all the necessary cases.

[elliottslaughter]

In this case all the code has actually been synthesized from the spec itself (not the other way around) so it's guaranteed to match.

I want to be careful with this claim. This is not a "correctness by construction" argument because the LLM is not a deterministic function. (Neither is a human, for that matter.) There is no guarantee, even if the LLM really does start with the TLA+ code and then derive the C++ from that, that the code is ever going to match. We have at most an empirical argument that this is the case (if we run the code and see no hangs), but the assurance only goes one direction: if we do see a hang, we know the C++ code doesn't match (or the TLA+ doesn't describe what we think it describes), but if we don't see a hang, we'll never know if they really match 100% or if we're just waiting to discover some corner case.

I still think it's better than before, and TLA+ is better than no TLA+, but I'd be more comfortable if we had a human actually read the new code, because who knows what's hiding in there.

[lightsighter]

In this case all the code has actually been synthesized from the spec itself (not the other way around) so it's guaranteed to match.

I want to be careful with this claim. This is not a "correctness by construction" argument because the LLM is not a deterministic function. (Neither is a human, for that matter.) There is no guarantee, even if the LLM really does start with the TLA+ code and then derive the C++ from that, that the code is ever going to match. We have at most an empirical argument that this is the case (if we run the code and see no hangs), but the assurance only goes one direction: if we do see a hang, we know the C++ code doesn't match (or the TLA+ doesn't describe what we think it describes), but if we don't see a hang, we'll never know if they really match 100% or if we're just waiting to discover some corner case.

That may be true in principle, but I gave the LLM extremely strict instructions to ensure a 1-to-1 translation and then had it launch multiple validation agents to confirm the invariant, followed by me asking an entirely different LLM to also perform an audit to confirm the invariant. It's as close to true as it is going to be.

I still think it's better than before, and TLA+ is better than no TLA+, but I'd be more comfortable if we had a human actually read the new code, because who knows what's hiding in there.

I don't think that's reasonable. There's about 5K lines of code changes and the complexity of the state machines are monstrous. Checking something like 7 nodes with 5 barrier generations and 3 different arrival patterns across those generations requires checking more than 100+M states and required a 24 hour TLC run to verify soundness. You're never going to be able to check it just by looking at the C++ code. I think the only way you can verify this is by running the code. I've done aggressive testing up to 128 nodes (512 ranks with 8 processes/node) on Eos and so far no bugs. Ask your favorite LLM to concoct the most aggressive test that you want and I'll even run it for you. No way is anyone going to find any bugs staring at this C++ code though.

[lightsighter]

Here is some performance data showing performance of the main branch barriers against these barriers at scale. There are two different patterns: one that is an all-to-all and one that is half-to-half (where half the nodes arrive and the other half subscribe). We can see the new barriers are competitive with the old ones at small node counts and significantly better at scale.

[lightsighter]

Here is some data for arguing that the default radix for the protocols used in internally should be 8 and that the worst case scenarios are much better for the new barriers.

[lightsighter]

Made another important optimization here which ensures that nodes do not forward on their arrivals in the "expected" case until after they've seen their local arrivals and all their expected child arrivals. Model checked comprehensively with multiple generations and arrival patterns up to 4 nodes, and partial up to 5 nodes. Validated correctness on tests at full scale.