GH-3959: capacity-aware agent assignment

[mlh758]

Rebased onto current main and narrowed to the capacity work. The node-side reconciliation
sweep this PR originally carried shipped separately in #4404 (hardened in #4408), so nothing
of GH-3987 is left here.

GH-3959: capacity-aware agent assignment

Opt-in via CapacityAwareAssignment, off by default. Each node samples its own load through
INodeLoadMonitor — the default reads memory pressure from Environment.WorkingSet against
the GC budget — and advertises it on every heartbeat. The leader then:

• prefers the least-loaded nodes;
• never places onto a node at or above NodeOverloadThreshold (default 90);
• sheds at most OverloadShedBatchSize agents per scheme per evaluation off overloaded nodes,
  never a pinned one;
• leaves agents unassigned when no node has headroom, rather than piling them onto a survivor
  that cannot start them.

Placement stops a 10-point hysteresis band below the shed line, so the two passes cannot
oscillate around one threshold. A node advertising no load always counts as having headroom,
keeping stores without load persistence on today's behavior.

The advertisement persists in a new wolverine_nodes column provisioned only when the feature
is on, leaving existing schemas and AutoCreate settings untouched. PostgreSQL today; other
stores simply never advertise.

Why

In the GH-3959 incident shape — three nodes collapsing to one — the survivor accepted every
assignment, ran out of memory starting them, and the leader re-decided forever: ~125
AssignmentChanged rows/minute with sustained OutOfMemoryException. Now the survivor holds
at its ceiling, the deficit surfaces as waiting agents, and recovery on scale-out is immediate.

All defaults preserve existing behavior.

[Copilot]

🟡 Changes recommended

The capacity shedding/distribution logic currently allows pinned agents to be detached and there are mismatches with the documented/spec’d topology stability behavior and load-monitor contract that should be corrected before merge.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

This PR hardens Wolverine’s distributed agent assignment during cluster churn (rolling deploys, node overload) by adding stability-gated rebalancing, node-local assigned-vs-running reconciliation, and opt-in capacity-aware placement (via a per-node load_factor heartbeat advertisement, PostgreSQL-only for now). It also reintroduces and expands formal P specs (plus Nix tooling) to model-check the relevant distributed protocols.

Changes:

• Add assignment stability gating and node-local reconciliation to reduce churn and self-heal “assigned but not running” wedges.
• Introduce capacity-aware assignment with load sampling/advertisement, overload shedding, and hysteresis.
• Add formal P model-checker specs + Nix flake tooling and documentation updates describing the protocols.

File summaries

File	Description
src/Wolverine/Runtime/Agents/WolverineNode.cs	Adds nullable per-node LoadFactor to the node state model.
src/Wolverine/Runtime/Agents/NodeAgentController.Reconcile.cs	New: topology stability tracking, load sampling, and local reconcile sweep.
src/Wolverine/Runtime/Agents/NodeAgentController.HeartBeat.cs	Advertises LoadFactor on every heartbeat and invokes reconciliation during health checks.
src/Wolverine/Runtime/Agents/NodeAgentController.EvaluateAssignments.cs	Applies stability gate and overload/acceptance flags into the assignment grid evaluation.
src/Wolverine/Runtime/Agents/INodeLoadMonitor.cs	New: load-monitor abstraction + default memory-pressure implementation.
src/Wolverine/Runtime/Agents/AssignmentGrid.Node.cs	Extends grid node model with load/overload/acceptance flags.
src/Wolverine/Runtime/Agents/AssignmentGrid.Distribution.cs	Updates even distribution with overload shedding, headroom-aware receiving set, and load-aware ordering.
src/Wolverine/Runtime/Agents/AssignmentGrid.cs	Adds OverloadShedBatchSize and carries node LoadFactor into the grid.
src/Wolverine/Runtime/Agents/AssignmentGrid.Agent.cs	Adds SheddedForCapacity marker to exempt urgent capacity moves from stability gating.
src/Wolverine/DurabilitySettings.cs	Adds new durability knobs: stability window, reconciliation threshold, capacity-aware settings, shedding batch size, and monitor hook.
src/Persistence/Wolverine.RDBMS/DatabaseConstants.cs	Adds load_factor column constant (intentionally not in shared NodeColumns).
src/Persistence/Wolverine.Postgresql/PostgresqlNodePersistence.cs	Persists/reads load_factor and updates it as part of the single-statement heartbeat write.
src/Persistence/Wolverine.Postgresql/PostgresqlMessageStore.cs	Adds nullable load_factor column to wolverine_nodes schema.
nix/p.nix	New: packages the P model checker as a Nix .NET global tool.
formal/rolling-deploy/RollingDeployTest.p	New: rolling-deploy/capacity test drivers for the model.
formal/rolling-deploy/RollingDeploySpec.p	New: safety/liveness monitor for rolling-deploy + capacity properties.
formal/rolling-deploy/RollingDeployModel.p	New: executable proposal model combining stability gate + reconcile + capacity ceiling behavior.
formal/rolling-deploy/README.md	New: detailed rationale, results, and mutant ledger for rolling-deploy spec.
formal/README.md	New: overview of formal specs, toolchain, and build isolation approach.
formal/leader-election/README.md	New: leader election spec documentation + results/mutants.
formal/leader-election/LeaderElectionTest.p	New: leader election test drivers.
formal/leader-election/LeaderElectionSpec.p	New: leader election convergence spec.
formal/leader-election/LeaderElectionModel.p	New: leader election model.
formal/Directory.Build.targets	New: MSBuild barrier file for generated P projects.
formal/Directory.Build.props	New: MSBuild barrier + CPM disablement for generated P projects.
formal/agent-assignment/README.md	New: single-agent ownership spec documentation + results/mutants.
formal/agent-assignment/AgentOwnershipTest.p	New: agent ownership test drivers.
formal/agent-assignment/AgentOwnershipSpec.p	New: agent ownership convergence spec.
formal/agent-assignment/AgentOwnershipModel.p	New: agent ownership model.
flake.nix	New: dev shell with .NET 8/9/10 + P + Java/Maven for PEx.
flake.lock	New: Nix flake lockfile pinning nixpkgs.
docs/tutorials/leader-election.md	Updates docs to describe lock-based election and references formal spec.
CLAUDE.md	Documents formal specs, toolchain, and “update model with protocol changes” guidance.
.gitignore	Ignores generated P build/run outputs under formal/**/.
.claude/skills/formal-specs/SKILL.md	New: internal skill doc capturing how to compile/check P specs and common pitfalls.

Review details

Suppressed comments (2)

src/Wolverine/Runtime/Agents/AssignmentGrid.Distribution.cs:116

• The rebalancing detach pass (extras) can also detach pinned agents. Pinned agents should be treated as fixed placement constraints, otherwise an operator pin can be undone by the distributor on the next evaluation.

        foreach (var node in receiving)
        {
            var extras = node.Agents.Where(agentSet.Contains).Skip(maximum).ToArray();
            foreach (var agent in extras)
            {
                agent.Detach();
            }

src/Wolverine/Runtime/Agents/NodeAgentController.Reconcile.cs:20

• Naming: observeTopology is internal, but internal/public members in this repo are expected to use PascalCase. Consider renaming to ObserveTopology (and updating its call site) to match the established accessibility-driven casing convention.

• Files reviewed: 33/35 changed files
• Comments generated: 3
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[mlh758]

I'll address those review comments and rebase so that if you want only the code changes it can still be easy to pull out.

Edit: Fixed

[jeremydmiller]

@mlh758 Hey man, can you please back off a little bit? And your characterization of the leadership election in the docs was off anyway. It's a semi-bully algorithm that always looks for the known node with the lowest node number and uses the advisory lock only as a way of taking the leadership. Really a back up.

One more time, I will not take the "P" thing. I cannot afford to have some kind of unusual alternative testing framework nobody knows that will instantly get out of sync with the code.

I'm not enthusiastic about any of this. What are you trying to do here? Is this for your own work, or @erdtsieck's issues? Anne's usage probably needs to be dealt with in the context of the Marten async daemon rather than through the IAgent mechanics IMO.

[mlh758]

I was just trying to show value for it, I didn't realize I was annoying you that hard. I kept the commit with the actual code change separate figuring you might say no. I just thought that a more interesting issue would show some value for modeling like that. I've rebased and now this PR only has the changes. I won't send anything about P or TLA+ at you again.

I picked those issues because they looked interesting and I knew there was similar work I could reference in Orleans. I'm using these projects so I wanted to contribute back. I also knew a simulator/harness for the issue should be possible to create and verify against.

If you don't want this either that's alright and I can back off. I'm just trying to not be someone who makes requests and never sends anything back.

Edit: tldr, sorry, I got too enthusiastic and I see how that was a pain.

[jeremydmiller]

I'm not 100% opposed to the actual approach, but I think there are some other, much simpler ameliorations for the Kubernetes thing I'd rather try first. Just simply saying "don't bother assigning anything until at least this much time has passed or this many nodes exist" would help a ton.

The async daemon thing for Anne that leads to the 10k agents is unique, and I think I'd rather pay more attention to finding ways of balancing work inside of the daemon layer than fighting that at the Wolverine agent distribution level beyond what we've already done.

The "P" thing? I had asked you not to do that before. And the first thing I'm going to do is have Claude translate that into a large battery of tests that mimic that, but in a way that's idiomatic to the project.

By and large, don't try to introduce all new testing or build automation or GitHub workflows to an OSS project as a first time contributor w/o discussing that first. I've been burned by that before, and it's a personal pet peeve of mine because of past experiences.

And sorry for being grumpy

[mlh758]

The "P" thing? I had asked you not to do that before. And the first thing I'm going to do is have Claude translate that into a large battery of tests that mimic that, but in a way that's idiomatic to the project.

I thought I had picked a bad example with leader election and tried to go for something more meaningful that might actually help out.

By and large, don't try to introduce all new testing or build automation or GitHub workflows to an OSS project as a first time contributor w/o discussing that first.

I've been a programmer for a while, I should have known better. I've been rewatching some old strange loop talks where formal methods were brought up and I though, "well, AI might actually make this feasible to introduce and help out!" and since I was using Wolverine and it wouldn't touch existing code I thought I could try it out.

And sorry for being grumpy

I'm the one who threw a giant PR at you with unknown technology, don't worry about it. I've been on the other end of that and it wasn't fun. I saw you communicating with AI a lot and wrongly assumed it wouldn't cause you much extra burden.

The async daemon thing for Anne that leads to the 10k agents is unique, and I think I'd rather pay more attention to finding ways of balancing work inside of the daemon layer than fighting that at the Wolverine agent distribution level beyond what we've already done.

I'd be interested in talking more about that if you want.

[mlh758]

Rebased this and dropped the changes for AssignmentStabilityWindow since #4367 introduced something similar. Re-ran against the simulator repo to make sure it didn't regress.

[jeremydmiller]

Hey, I think the most likely thing is that we take the reproduction harness but not the fix. There'd have to be more than this anyway because we can't ship breaking database changes w/o doing a major version bump.

And I think the priority needs to be in other areas as I was trying to say earlier.

[mlh758]

I could guard the use of the new column on using the option and document that it requires running a migration to use the feature. I should have done that in the first place to make the PR acceptable. (Edit: there is a guard now so that the column is only used if the feature is enabled).

If it's in the wrong place though then that's not worth doing. Where would you rather see a mitigation added?

Either way, you're welcome to the reproduction code.

[mlh758]

The other thing this PR has is:

Compares this node's durable assignment rows against its actually-registered agents and heals the divergences the leader cannot see

This was another thing mentioned in the source issues where it seemed like pods would come up and not all the agents would start. I've also had runs in the simulator repo where after some rollouts there are duplicate agents. There's probably a deeper fix there but the reconciliation would at least heal it. I could pull that out of this PR and open one separately.

[mlh758]

@jeremydmiller okay I've rebased this PR and cleaned up the title/description. I'll make one more pitch for it and then close it out if you're not satisfied. Here's the highlight from my testing in that sim repo:

The new settle period helps with churn during rollout but doesn't change the behavior of losing nodes. If a cluster is under pressure, losing a node can still cause a cascade since a departed node will immediately trigger re-balancing. A wait period might not help even if it didn't though since it could take a while for a new pod to come up if there are other issues with the cluster like nodes being rotated out for maintenance.

Since Wolverine can host custom agents it seems like the spot that would be best aware of how to allocate them, and there's now a guard to keep the new column from being used unless you opt into the feature. I could also be missing a better spot though.

[jeremydmiller]

Thanks @mlh758 — re-verified today: still MERGEABLE/CLEAN against current main with all checks green.

We're not landing this in the current pass, but it's queued for the next one. Plan when we pick it up is a review of the placement/shed hysteresis logic in AssignmentGrid.Distribution and of the opt-in wolverine_nodes column provisioning, then merge.

Also noting for the record that the GH-3987 half shipped separately in #4404 (hardened in #4408), so despite the branch name this PR is purely GH-3959 — that matches your description, just confirming we read it the same way.

[mlh758]

Sounds good, let me know if there are any changes you want against the branch in the mean time. I tried to make it passive per your previous comment but that's the part I'm most worried about having gotten right.