Repository navigation
FLEET-RESOURCE-N - #9994
Merged
gunbai-bot[bot] merged 17 commits intoSep 2, 2026
Merged
FLEET-RESOURCE-N#9994
Conversation
…om one permit-scope row gunbc#9789 stopped the cause of the jobserver permit leak by declaring NeverSupersedeRunning, and declared a DESIGN 4b(3) drop whose dissolve-on names a CAPABILITY: no client of the required floor holds a host-persistent cooperative permit -- either the ctrl host FIFO is gone and compile parallelism is invocation-local to cargo, or the pool is server-owned with admission that survives client death. That capability was a sentence in an annotation and the policy was an authored literal, so the containment could outlive its own reason: the fleet retires the FIFO, the leak stops, and CI goes on refusing to supersede because nothing joins the two facts. DESIGN 4b(3) says a drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, which makes the trigger the whole check -- and a check nothing evaluates is diligence, not a check. gunbc.compile_permit_scope declares CompilePermitScope with the two arms the trigger names as sufficient, permit_outlives_borrower as the decidable question it asks, and one row for what the fleet runs today. Both consumers derive from that row: the runner unit's environment and its After/Wants on ctrl-jobserver.service, and the required floor's running supersession axis. The ordering dependency departs WITH the environment that needed it, because a unit ordering itself After a service the cutover deleted is a fresh failure introduced by the fix. No arm for a server-owned pool: an arm with no realization is vocabulary invented ahead of its consumer. It belongs here the day someone builds one. Nothing actuates. fleet_compile_permit_scope still carries HostPersistentPermitPool, so the emitted workflow and the rendered unit are unchanged; flipping the row is the cutover and is an operator act. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
Side-chat review of the first draft found a fail-open I authored, and it is the kind DESIGN section 5 names rather than a rough edge: a generated artifact can make a rendered unit and a rendered workflow agree, but it cannot make host deployment and GitHub workflow activation atomic. Deriving the running axis straight from the desired realization row would have restored cancellation the moment the workflow reached main, while every host that had not yet received and restarted onto the new unit went on losing a permit per kill. My commit message claimed flipping one row moves the unit and retires the containment together; operationally that was not true. Three layers now, because they are three facts. CompileParallelismRealization is what a host runs. BorrowerDeathCapacityDisposition is what that implies for capacity under kill, and it is what business policy is allowed to see -- a workflow that matched realization variants would have to learn FIFO paths and systemd service names, and would need a new business branch per realization. HostCompileCancellationStanding and its fleet fold are what has been OBSERVED, with the safe arm carrying its readback rather than asserting itself. The fleet standing today is NotSafe over an empty roster, so the policy stays NeverSupersedeRunning BY REFUSAL. Unobserved is on the refusing side, one unsafe or unread host holds the containment, and a safe readback carrying a losing disposition joins the unsafe side rather than being believed. CapacityPreservedByServerReclamation exists with no concrete realization, reversing my earlier call. It is one of the two arms the dissolve-on names as sufficient and it has an immediate consumer in the policy fold, so omitting it narrowed the trigger to one arm -- the 4b(3) failure where a trigger naming less than the capability is satisfied while the capability stays dead. What stays absent is a concrete server realization with guessed fields. Renamed off HostPersistentPermitPool: persistence is not the defect, since a server-owned pool may be host-persistent and still reclaim safely. The unsafe arm names what is load-bearing -- borrower-held, cooperative, unreclaimed. The unit witnesses now render from a fixture realization carrying /fixture/other.fifo and fixture-other.service rather than the production constants, because the old fixture used exactly the values the renderer previously hardcoded: an implementation ignoring the arm's payload passed every witness. Both arms also assert their exact unit-section directive sequence, which substring witnesses could not see after the list was restructured. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
The build lane refused with 'module index refused: 1 unparseable .dag source(s)'. The empty-list pattern I used to test the rosters -- [] => ... / _ => ... -- has no precedent anywhere in the corpus, which was the tell I should have read before pushing rather than after: a construct nothing else in 4471 modules uses is a construct the grammar probably does not have. list_length is what std.types already provides, and the conjunction is bound to a name before the match rather than matched as a parenthesised expression, which is likewise unprecedented here. The refusal shape is unchanged and still deliberate: SAFE requires a non-empty safe roster AND an empty blocking one, so an empty observation set stays on the refusing side. Testing only the blocking roster would report SAFE for silence, which is the empty-observation narrowing this repository has a named failure mode for. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
The real parse error was compile_permit_scope.dag:158:77 'expected expression, found Newline' -- a data declaration whose initializer I wrapped onto the following line. Every other diagnostic in that run was the cascade: forty 'source annotation names no subject' lines, which is what the annotation channel reports once the item after it fails to parse. I read the cascade first and guessed at the empty-list patterns; those were unprecedented and worth replacing anyway, but they were not the failure. Also takes review 58445's non-blocking point, which is right: fifo_path was String while its sibling daemon_service was NonEmptyStr, so an empty path would have rendered Environment=CTRL_JOBSERVER_FIFO= and --jobserver-auth=fifo: with nothing after the colon. cargo does not refuse an unrecognised auth clause, it builds unbounded -- the same silent boundary extdeps.jobserver already warns about, which is what makes the weaker type worth closing now rather than when a caller finally supplies one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
DESIGN section 4c states it plainly and it is in the design document loaded on every turn: the .dag realization admits only standalone leading // blocks attached to module-scope declarations, and body forms refuse until separately modeled. I put rationale inside match arms and a let sequence in two modules, so the parse refused nine times. The rationale is not deleted -- it is hoisted into the leading block of the declaration it was describing, which is where a reader looking for why the fold refuses an empty roster or why the cutover arm emits no MAKEFLAGS will now find it. That is the grain the annotation channel models, and the constraint is the reason section 4c gives: an annotation is captured authored-source data disjoint from semantic occurrence allocation, so admitting it at arbitrary depth is a separate modeling job nobody has done. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
… with it Review 58469, both findings, and both are right. HostCancellationSafe carried an authored disposition beside an active_unit_readback string, and the fold read only the disposition -- so the readback was decorative and arbitrary prose could label a host capacity-preserving and, through the policy fold, authorize superseding running builds. My own server-reclamation fixture demonstrated exactly that with a sentence of prose. A carrier that looks like evidence and is never consumed is worse than no carrier, because it will be cited as coverage. The observation now carries only WHAT WAS READ -- the realization -- and the fold DERIVES the disposition from it. There is no longer a constructor for a safe host at all, so the self-certifying state is unwritable rather than merely unwitnessed. HostCancellationUnsafe became HostCancellationUnreadable, which is the honest residual: a readback obtained but not interpretable, distinct from no readback at all, and both on the refusing side. disposition_preserves_capacity is deleted. It matched a substrate coproduct's variants only to collapse them into true/false, which is the predicate-dissolution trigger; the fold now matches the three arms directly, so a fourth disposition refuses to compile here instead of silently falling to one side. What this costs, stated rather than hidden: no realization produces CapacityPreservedByServerReclamation, so that arm now has no producer and its sufficiency is modeled and consumed but not exercised. That is the honest state -- the semantic outcome exists because the dissolve-on names it, and it becomes reachable when someone builds the realization. Binding real host readbacks to realizations is the stage-2 consumer this PR does not claim to have; until it exists the fleet standing has no observations and the policy refuses. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
…notation
Side-chat review of the pushed head found that my annotation claimed the caller supplies
the eligible-host roster while fleet_cancellation_standing took only observations. So
[safe_host("srv1")] answered SAFE with srv2, srv3 and srv4 eligible and never asked --
the unsafe interval this whole construction exists to close, still writable, described as
closed. An annotation cannot authorize; only executable structure can.
The roster is now an argument, and SAFE is an identity join over it rather than a count
equality: every eligible host must appear among the safe observations, no observation may
name a host outside the roster, and the counts must agree so a duplicate cannot stand in
for an absentee. Missing hosts are reported in unobserved_hosts rather than vanishing. An
empty roster refuses outright -- a fleet with no eligible hosts is an unasked question, not
a safe fleet.
Two witnesses for the arms the parameter exists for: a partially observed fleet is not
safe, and an observation for a host outside the roster does not complete it. The second is
what makes the join two-directional rather than a size comparison.
Still open from the same review and not addressed here: the two exact-order unit witnesses
are contiguous substring checks, which prove one expected fragment occurs but not that it
is the complete [Unit] list with no duplicate or extra directive. A complete-equality
oracle against a production-equivalent baseline is the accepted substitute for the
parent-versus-candidate differential, and it is the next commit rather than this one.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
…alues The last open item from the side-chat differential ruling. The two exact-order witnesses were contiguous string_contains checks: they prove an expected run of directives occurs, which fixes order WITHIN that run and says nothing about what surrounds it. A duplicated After=, an extra Wants=, or a stray blank line outside the fragment left them green, so they could not answer the question the restructure actually raised -- did interleaving the optional pair change any byte that was not meant to change. Sections are emitted header-first and separated by one empty line, so pinning from [Unit] through to [Service] is the entire section and nothing can hide inside it. That is the complete-equality oracle offered as the accepted substitute for a two-compiler parent-versus-candidate differential, without standing machinery that builds two compilers on every run. It renders the PRODUCTION realization -- the fleet's own FIFO path and daemon service -- beside the distinct-value fixture rather than instead of it, because they answer different questions. The fixture proves the renderer consumes its argument's payload; this proves the live arm serializes to exactly what the fleet's realization produces. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
Review 58495, and it is right in a way that matters more than the ordinary parallel-authority case: the re-minted list would have defeated the very join it fed. fleet_cancellation_eligible_hosts hardcoded four names beside gunbc.fleet_runner_connectivity fleet_hosts, which already owns that fact and has several consumers. Add a fifth host to the real roster and my copy answers SAFE on a 4/4 observation set while the new host leaks a permit for every superseded build -- the exact denominator failure the parameter was added to prevent, reintroduced one layer up. The roster is gone and the standing reads fleet_hosts(). Hosts are typed HostIdentity throughout rather than bare NonEmptyStr, which is what the fleet authority already returns, so the join compares the same branded identity the rest of the corpus uses instead of casting through a second spelling. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
The differential finding, discharged rather than deferred a second time. Every previous version of this evidence was string_contains -- contiguous fragments, then the whole [Unit] section header-to-header -- and none of them is the byte claim the restructure owes. A substring says nothing about what surrounds it: a duplicated directive in [Service], an extra blank line, a dropped Install directive all leave it green. Three complete-equality witnesses now compare the serialized render against an expected SystemdUnitFile enumerated here. The expected side does not call runner_unit_file, runner_unit_jobserver_after, runner_unit_jobserver_wants or runner_unit_jobserver_environment -- the four places the restructure moved -- because an oracle built from the code under test agrees with it by construction. It does reuse runner_unit_app_environment and the shared serializer, which are not what changed. One expected constructor serves two orthogonal propositions, executed twice. Against the production FIFO and service it establishes that the live arm's complete bytes are unchanged from parent d61f8c9. Against /fixture/other.fifo and fixture-other.service it establishes that the renderer consumes its argument -- a renderer hardcoding today's constants passes the first perfectly and fails the second, since the expected object places the fixture path twice and the fixture service twice. The cutover arm gets its own constructor rather than an expected-side match, so the oracle never reproduces the candidate's arm dispatch. rendered_or_refused replaces the helper that collapsed a refusal to the empty string. For a substring probe that was harmless; for an equality oracle it is fatal, because a renderer that refused everything would satisfy "" == "". A refusal now renders its reason and fails the comparison. The three witnesses these subsume are deleted rather than left beside them, since a weaker assertion over the same subject is a second representation that can only go green when the stronger one already has. This is a TRANSITION oracle, not a claim the unit may never change. When it legitimately moves, the expected shape moves with it and the parent anchor becomes the previous transition. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
Review 58515 is right, and it names the thing my own previous commit message admitted: HostCancellationObserved carries a realization an author supplies, so while the live standing was a data row of observations, inserting InvocationLocalCargo constructors would have enabled supersession with no host having converged. That is satisfiable by editing the declaration while the realization lies -- the validation tell DESIGN section 5 names. No in-repo type can stop a fixture constructing an observation, and it must not: section 4b requires the discriminating RED to be authorable as source handed to the compiler by a fixture, which is what every witness on this fold is. What the model can do is refuse to let PRODUCTION reach the safe arm through authorship. ActiveUnitReadbackSource is that boundary: its live row is ReadbackProducerAbsent, every eligible host is unobserved because nothing reads them, and there is no list an author can extend to change the answer -- reaching SAFE now requires implementing ReadbackObservations, which means writing the host read. The boundary is declared rather than implied by an empty observation list, because an empty list reads as 'we looked and found nothing' when the truth is 'nothing has looked'. That is the column DESIGN 4b keeps deliberately off the ladder: external reality, observed or refused at a declared boundary, never fabricated. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
Contributor
|
Re review 58515 — the finding is correct and is fixed at What was wrong. What is fixed. Where I would push back slightly, because it affects what the next reviewer should ask for. No in-repo type can prevent a fixture from constructing an observation, and it must not: §4b requires the discriminating RED to be authorable as source handed to the compiler by a fixture, and every witness on this fold is exactly that. What is still not claimed. Binding a real receipt to a real host read — the — sent from eager-ram-258 |
The floor caught three call-shape errors in the expected-labels helper I wrote for the complete-file oracle: json_array takes elements not items, json_string takes s not value, and serialize_json takes v not value. I invented those names instead of reading the declaration, and the one place in the corpus that already calls all three -- runner_unit_labels_json, twenty lines from the code I was mirroring -- spells them correctly. Worth stating because it is the same shape as the parse errors earlier in this PR: every one was a construct I assumed rather than checked, in a language whose corpus was open in front of me. I have now verified the remaining fifteen constructors and four helpers in that oracle against their declarations rather than pushing and finding out. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
…ion arm to where its RED is authorable Two merge blockers from the side chat's read of #9994, both fail-open in the same direction — a claim the code did not have. The producer boundary was an authored row. ActiveUnitReadbackSource wrapped the observation list in two arms and its live row was ReadbackProducerAbsent, with an annotation saying reaching SAFE would require implementing the observed arm. False: ReadbackObservations was an ordinary constructor, so a source edit could supply a roster-covering observation list and the fold would answer SAFE with no host read, no command, no captured output and no receipt. Wrapping an author-constructible value in a coproduct does not change its provenance. The live binding now calls producer_absent_standing, a function with NO safe arm. Fixtures keep the full fold, because 4b requires the discriminating RED and its positive control to be authorable as source handed to the compiler by a fixture. CapacityPreservedByServerReclamation was unexecuted vocabulary. Review 58515 mutated only that arm to classify its host UNSAFE and every witness still passed: no realization maps to that disposition, so the ordinary path never produces one, and the arm sat inside the fold's lambda where no fixture could address it. It is half of the drop's dissolve-on and must not be deleted, so the classification and the identity join become the production helpers accumulate_observed_disposition and finalize_fleet_standing, and two witnesses drive that arm through those same procedures — a positive control reaching restored supersession, and a losing-host red so the positive one cannot be satisfied by a helper that calls everything safe. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
Contributor
|
The one failing check is
So it is not fixable from here, and it is already owned elsewhere — #10025 ("The service-refusal control asserted the fail-open shape it existed to forbid") and #10027 ("Observe shell binding refusal before artifact emission") are on exactly this subject. Pushing a repair of a compiler test I did not break, from a lane whose brief is CI capacity containment, would be scope I do not have. Per The lanes this change is actually judged by: — sent from eager-ram-258 |
…-jobserver-persistence
Review 58660, cosmetic. invocation_local_text's closing brace and the next test fn shared a line. It tokenizes, but nothing else in the file is written that way. Worth recording how the finding was cited: it named runner_unit_file_witness_test.dag:827-828 in a 458-line file. The position was wrong and the symbols -- invocation_local_text and w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies -- were right, which is the positional-citation decay DESIGN section 3 names, arriving inside a review of a PR about exactly this kind of authority drift. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh
…-jobserver-persistence
gunbai-bot
Bot
deleted the
session/eager-ram-258-jobserver-persistence
branch
September 2, 2026 13:48
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
1 participant
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 this is
Partial substrate only. It models the fact gunbc#9789's declared DESIGN §4b(3) drop turns on — what a borrower's death does to future compile capacity — and rewires two authored literals to be derived from it. It does not dissolve the drop, does not touch any host, and does not change the emitted workflow's bytes.
.github/workflows/witnesses.ymlis byte-identical toorigin/mainon this head. The diff is five.dagfiles.The three facts, kept apart
gunbc.compile_permit_scopedeclares them as three layers, because collapsing them is what lets a desired-state row authorize a policy the hosts have not earned:CompileParallelismRealization— what a host runs (borrower-held cooperative host FIFO, or invocation-local cargo).BorrowerDeathCapacityDisposition— what that implies under SIGKILL. A cooperative permit is not returned and no reaper exists, so capacity is lost until pool restart; that is why FLEET-RESOURCE containment A: stop kill-style supersession of running CI runs #9789's symptom was a slow queue rather than a failure.HostCompileCancellationStanding/FleetCompileCancellationStanding— what has been observed of the running fleet, which is not what a row wishes.gunbc.witness_floor_workflownow derives its running-supersession axis from the fleet standing, andgunbc.runner_unit_filederives the unit's jobserverEnvironment=,After=andWants=from the realization instead of carrying them as constants.Why production cannot reach SAFE
The live binding calls
producer_absent_standing, a function with no safe arm. An earlier revision instead wrapped the observation list in a two-armActiveUnitReadbackSourceand annotated that reaching SAFE required implementing the observed arm — that annotation was false, sinceReadbackObservationswas an ordinary constructor and a source edit could have supplied an authored roster-covering list with no host read, no command, no captured output and no receipt. Wrapping an author-constructible value in a coproduct does not change its provenance.Fixtures keep the full fold, because §4b requires the discriminating RED and its positive control to be authorable as source handed to the compiler by a fixture; the restriction belongs on the production path alone. The stage-two PR adds a real observer together with its observed output, in the shape
gunbc.host_hygiene_reaper_observealready uses.Test plan
dag/test/claim/run_disposition_witness_test.dag— the standing→policy join, both directions:pull_request. Without this arm a derivation that ignored its argument and always refused would pass every other witness.CapacityPreservedByServerReclamationarm to classify its host unsafe and every witness still passed — no realization maps to that disposition, so the ordinary path never produces one and the arm sat inside the fold's lambda where no fixture could address it. The arm is half of the drop's dissolve-on and must not be deleted, so the fold's classification and its identity join are now the production helpersaccumulate_observed_dispositionandfinalize_fleet_standing, and two new witnesses drive that arm through those same production procedures — a positive control reaching restored supersession, and a losing-host red so the positive one cannot be satisfied by a helper that calls everything safe.dag/test/claim/runner/runner_unit_file_witness_test.dag— a complete-file differential oracle rather than a substring probe: the live arm is asserted byte-identical to an independently spelled expected unit, a second arm renders a fixture FIFO path and service name to prove the renderer reads its argument rather than the production constants, and the cutover arm has its own complete expected shape plus two negative witnesses (no shared pool advertised, daemon ordering dropped). The expected side reusesrunner_unit_app_environment,runner_unit_environment,runner_unit_quoted_environment,runner_slot_instance_directoryandserialize_systemd_unit_file— shared machinery that is not what changed; every directive under test is spelled out.What is deliberately not here
gunbc.rung_drop's row for FLEET-RESOURCE containment A: stop kill-style supersession of running CI runs #9789 is untouched. The drop retires by its trigger and nothing else, and the trigger names an observed-converged fleet, which requires the stage-two observer and the host cutover.CapacityPreservedByServerReclamationis one of the two arms the dissolve-on names as sufficient; omitting it would narrow the trigger to one arm, which is exactly the §4b(3) failure where a trigger naming less than the capability is satisfied while the capability stays dead. A realization with guessed fields would be vocabulary ahead of its consumer, so there is none.CI
Green on the final merged head
e24d0a223d(run 33633309710) —required-witnesses-floor,required-witnesses-build,rust-unit-tests,fabric-evidenceand thewitnessesaggregate all success.An earlier revision of this body recorded
compiler_tests::shell_service_unmodeled_output_key_refusesas a known red inherited from main. That is no longer true: #10025 landed and fixed it, and this branch has since merged current main.The floor's green is not by itself evidence that the new witnesses ran, so the receipt is
required-floor-dispositionfrom run 33633309710 on that same final heade24d0a223d, where all eight load-bearing ones appear asplanned_as_changed_witness … passed: the four fleet-standing arms (w_a_server_reclaiming_fleet_restores_supersession,w_one_losing_host_among_reclaiming_hosts_holds_the_containment,w_a_fully_observed_safe_fleet_restores_supersession,w_the_live_fleet_standing_still_refuses_running_supersession), the three unit-file oracle arms, andw_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies.