feat(worker): run provider mutations outside the fleet lock under per-slot leases (C2 3 of 3) - #261
Merged
Merged
Conversation
…-slot leases (C2 3 of 3) The fleet lock now covers only short read-validate-claim and apply sections. Every provider mutation goes through provider_mutate under a non-blocking per-slot flock lease (provider_call refuses 'mutate' outright), claimed durably by claim_pending before the provider is touched and applied by apply_pending against a FRESH load, never the caller's pre-call object. Mutations for different slots run concurrently; an execute no longer blocks status, dry reconcile, requests, or withdrawals for its whole guest run. Reconcile fetches inventory unlocked, plans and claims in one short hold, mutates unlocked, applies in a fresh hold, and records refusals on a CLEAN load. The drain of stranded claims runs AFTER convergence with strict=False, skipping any slot whose lease a live process holds, so a wedged or hours-long replay cannot stop the fleet converging; the planner and the classification refresh skip claimed slots, whose durable records are deliberately not yet the truth. resume drains only its own slot, strictly. claim_pending refuses a different key on a claimed slot, closing the blind overwrite that silently discarded the first claim's replay obligation and ran the guest twice. The sanctioned exit that overwrite used to provide is now explicit: abandon-claim takes the lease, replays the mutation itself, requires the provider result to bind the exact idempotency key (the mutation is provably complete and its result final under key-idempotency), records the refusal verbatim with the result digest in cleanup_refusals, and only then clears the claim. The capacity commands keep their single holds deliberately: merged_specialized_reservations ignores non-reserved locals, so a split would let two concurrent reserves each admit against a budget that fits one. The two-writer proof parks two creates INSIDE the provider on a real FIFO rendezvous and asserts a two-entry pending_actions map with two distinct assignment generations - a shape structurally unsatisfiable under the old fleet-lock discipline, with a one-child positive control that must fail the two-arrival wait. The fixture provider gains an flock around its read-modify-write so a lost update cannot masquerade as a controller bug.
…e refusal, close abandon's race The review proved the LOCK_NB discipline had no behavioral pin (a blocking lease survived the suite; the static marker was satisfied by a docstring): the concurrent unit now probes slot 1's lease from a bounded subprocess while the parked child owns it, requiring an immediate SlotBusy. abandon- claim gains the drain's under-lease re-read before re-sending, so a claim a concurrent drain applied is never mutated again without a durable claim naming it. The strict drain mode is pinned against the wedged claim (resume depends on it). The abandon docstring and help now say the proof is obtained BY submitting and what a refused create leaves behind; dead loop and stale execute_action comments removed.
…w path the ban exposes fm-azure-pilot's bound probe called provider_call with 'mutate' directly, which the lock discipline now refuses; the timeout bound under test lives on _provider_call_raw, which every mutation reaches through provider_mutate. The probe now asserts the ban fires AND the raw path carries the bound.
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
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.
What
C2's final change, per C2-DESIGN.md section 3, shipped as ONE PR as the design requires: a half-serialized controller in which some commands hold the fleet lock across provider calls and others do not is worse than either end state.
Verification
18 units green. New proofs:
Mutations against the committed tree, each red: claim different-key refusal dropped; apply_pending claim re-check dropped (survived the first sweep, pinned by the stale-apply probe); drain dropping refused claims; planner claimed-slot skip dropped (survived the first sweep, pinned by the released-worker plan probe); mutate ban dropped; lease slot binding dropped; abandon-claim key match dropped.
bin/fm-lint.sh clean; fm-behavior-shards.sh --check 8 clean (file duration re-budgeted 8000->12000ms).