diff --git a/dag/gunbc/runner/runner_microvm.dag b/dag/gunbc/runner/runner_microvm.dag index b22664cf35c..bc1bcf348bd 100644 --- a/dag/gunbc/runner/runner_microvm.dag +++ b/dag/gunbc/runner/runner_microvm.dag @@ -35,8 +35,8 @@ import gunbc.runner_slot_allocation { import gunbc.runner_unit { RunnerUnitLifecycleIntent, gunbc_runner_lifecycle_intent, - lifecycle_intent_cannot_orphan, - gunbc_runner_listener_is_main_process, + lifecycle_intent_stops_finished_incarnation, + gunbc_runner_main_exits_when_incarnation_ends, } import extdeps.github.actions_runner { ActionsRunnerRelease, actions_runner_release_2_337_0 } import extdeps.virtualization.firecracker { @@ -425,10 +425,18 @@ type VmmProcessTopology = VmmIsMainProcess | VmmUnderLifecycleController // its guest alive holding the same credential. "Everything inside the VM dies together" is true and // does not help when the VM is what survived. // -// gunbc.runner_unit already owns the deciding predicate and the measured input (the listener is a -// GRANDCHILD of MainPID because GitHub's stock run.sh does not exec), so this consumes that -// authority rather than re-deriving it. Stating the dependency in prose would have left it -// satisfiable by an author who never read the paragraph. +// gunbc.runner_unit already owns the deciding predicate and the measured input (whether the tracked +// main process exits when the incarnation ends), so this consumes that authority rather than +// re-deriving it. Stating the dependency in prose would have left it satisfiable by an author who +// never read the paragraph. +// +// THIS IS A NECESSARY GATE, NOT A SUFFICIENT ONE, and the gap is a declared frontier. The predicate +// is static: it says a finished incarnation makes systemd issue a stop that reaches the cgroup. It +// cannot say the VMM is gone afterwards -- a task in uninterruptible sleep survives SIGKILL, and a +// main process that outlives its incarnation issues no stop at all -- nor that the cell is safe to +// reuse. That is gunbc.product.fabric.sanitation's CellReadiness, established by a terminalizer's +// readback, which this admission will consume once the terminalizer lands. Until then an Admitted +// verdict here is not sufficient grounds to run customer work. type RunnerMicroVmAdmission = RunnerMicroVmAdmitted | RunnerMicroVmRefusedOrphanableUnit { reason: String } @@ -452,7 +460,7 @@ type RunnerMicroVmAdmission fn runner_microvm_admission( topology: VmmProcessTopology, intent: RunnerUnitLifecycleIntent, - listener_is_main_process: Bool, + main_exits_when_incarnation_ends: Bool, transport: JitCredentialTransport, config: FirecrackerVmConfig, reserve: RealizationReserve, @@ -461,11 +469,11 @@ fn runner_microvm_admission( VmmIsMainProcess => runner_microvm_admission_after_topology(transport: transport, config: config, reserve: reserve) VmmUnderLifecycleController => - if lifecycle_intent_cannot_orphan(intent: intent, listener_is_main_process: listener_is_main_process) { + if lifecycle_intent_stops_finished_incarnation(intent: intent, main_exits_when_incarnation_ends: main_exits_when_incarnation_ends) { runner_microvm_admission_after_topology(transport: transport, config: config, reserve: reserve) } else { RunnerMicroVmRefusedOrphanableUnit { - reason: "this topology keeps a lifecycle controller above the VMM, and the unit's teardown can leave a live process behind, so an orphaned VMM would keep its guest and its credential alive -- the microVM relocates the orphan rather than removing it. Deploy the cgroup-reaching intent, or exec the VMM directly as MainPID", + reason: "this topology keeps a lifecycle controller above the VMM, and the unit's teardown can leave a live process behind, so an orphaned VMM would keep its guest and its credential alive -- the microVM relocates the orphan rather than removing it. Deploy the declared intent (ExitType=main with KillMode=control-group), or exec the VMM directly as MainPID", } } } @@ -631,7 +639,7 @@ fn gunbc_runner_microvm_admission( runner_microvm_admission( topology: topology, intent: gunbc_runner_lifecycle_intent, - listener_is_main_process: gunbc_runner_listener_is_main_process, + main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends, transport: gunbc_runner_jit_transport, config: config, reserve: gunbc_runner_microvm_realization_reserve(), diff --git a/dag/gunbc/runner/runner_slot_retirement.dag b/dag/gunbc/runner/runner_slot_retirement.dag index e1b2d4f97f3..7fea4efb531 100644 --- a/dag/gunbc/runner/runner_slot_retirement.dag +++ b/dag/gunbc/runner/runner_slot_retirement.dag @@ -45,7 +45,7 @@ import gunbc.systemctl_show_read { // 3. OBSERVE IT GONE, and observe the CGROUP EMPTY -- two facts, not one. // // WHY THE CGROUP IS A SEPARATE OBSERVATION FROM THE UNIT. `gunbc.runner_unit`'s teardown intent -// (ExitType=cgroup, KillMode=control-group) exists precisely because a runner unit could report +// (ExitType=main, KillMode=control-group) exists precisely because a runner unit could report // stopped while its Runner.Worker, claim_executor and gunbc children kept running -- the orphan // class that motivated that drop-in. A unit reported gone whose cgroup still holds processes is // exactly that state, and it still holds memory. Charging capacity against the unit's disposition diff --git a/dag/gunbc/runner/runner_unit.dag b/dag/gunbc/runner/runner_unit.dag index 607a16a301c..63382f8fd86 100644 --- a/dag/gunbc/runner/runner_unit.dag +++ b/dag/gunbc/runner/runner_unit.dag @@ -162,42 +162,64 @@ type RunnerUnitLifecycleIntent { kill_mode: SystemdKillMode } -// THE ONE PROPERTY THE INTENT EXISTS TO GUARANTEE, STATED AS A PREDICATE OVER THE PAIR RATHER THAN -// AS A CHOSEN CONSTANT. +// THE ONE PROPERTY THE INTENT EXISTS TO GUARANTEE: WHEN AN INCARNATION ENDS, SYSTEMD ISSUES A STOP, +// AND THAT STOP REACHES EVERY PROCESS IN THE CGROUP. // -// A slot cannot leave a live process behind at teardown unless BOTH hold: the stop must reach every -// process in the cgroup (kill_mode), and systemd must not consider the service finished while -// processes remain (exit_type). Either one alone is insufficient, and that is the trap the brief -// names -- KillMode=control-group with ExitType=main still lets the manager decide the service -// ended when a wrapper exits, so the teardown that would have reached the cgroup is never issued -// for the survivors. +// Two questions, and each half answers exactly one. kill_mode answers whether an ISSUED stop +// reaches the whole cgroup. exit_type answers whether a stop is ISSUED AT ALL when the incarnation +// ends -- and that second question is the one an earlier revision of this predicate answered +// backwards. // -// THE PARAMETER IS WHETHER THE LISTENER IS THE MAIN PROCESS, NOT WHETHER A WRAPPER EXECS, AND THE -// DIFFERENCE IS THE WHOLE MEASUREMENT. An earlier revision asked the second question, on the -// reasoning that a wrapper which execs leaves the listener as the tracked process. That reasoning -// is wrong here for a reason no amount of reading the wrapper would have shown: jit-runner.sh DOES -// exec, and the listener is still not the main process, because what it execs into is GitHub's -// stock run.sh, which does not exec. Measured process tree, srv1 2026-08-25 -- run.sh at pid -// 702572 with ppid 1 as MainPID, its run-helper.sh child at 702921, and Runner.Listener at 702930. -// The listener is a GRANDCHILD of the process systemd supervises. +// THE RETRACTED ARMS, AND THE INCIDENT THAT FALSIFIED THEM. The earlier predicate read +// `ExitTypeCgroup => true` and `ExitTypeMain => listener_is_main_process`, on the reasoning that +// ExitType=cgroup makes systemd wait for the whole cgroup and so cannot call the service finished +// while a process remains. The waiting is real; what it implies is the opposite of what that +// revision concluded. Under ExitType=cgroup, a populated cgroup keeps the unit RUNNING after +// MainPID exits, so no stop transaction begins, KillMode never executes and TimeoutStopSec never +// starts. srv2-02, 2026-09-16: GitHub cancelled a job at its 180-minute cap, the cancel reached the +// step's shell but not its claim_executor child, run.sh exited, and the unit sat `active` with +// MainPID=0 for 2.7 days holding 16 GB. The census of 2026-09-18 found srv1-03 and srv1-07 in the +// same state for 16 days, held by background processes a SUCCESSFUL job had left behind -- so the +// hang is not a property of cancellation, it is a property of any survivor. // -// So the predicate takes the fact that decides the outcome rather than a proxy for it. A proxy that -// happens to be true while the thing it stands for is false is worse than no parameter at all. -fn lifecycle_intent_cannot_orphan(intent: RunnerUnitLifecycleIntent, listener_is_main_process: Bool) -> Bool { +// THE CORRECTED ARMS ARE MEASURED, NOT READ. srv1, systemd 255, 2026-09-18, a transient unit with +// KillMode=control-group, SendSIGKILL=yes, TimeoutStopSec=4s, whose main process forks a child and +// exits zero: under ExitType=main the child was reaped whether it honored SIGTERM or ignored it (the +// second after the SIGKILL escalation); under ExitType=cgroup the unit stayed `active running` with +// MainPID=0 and the child alive in both cases; an explicit `systemctl stop` under ExitType=cgroup +// reaped the ignoring child in 4s. So ExitType decides whether a stop is issued, KillMode decides +// whether an issued stop reaches the cgroup, and ExitType is irrelevant once a stop is requested. +// +// THE PARAMETER IS WHETHER THE TRACKED MAIN PROCESS EXITS WHEN THE INCARNATION ENDS, and it +// replaces `listener_is_main_process`, which was the wrong question. The listener being a +// grandchild of MainPID does not matter: run.sh's exit is what makes systemd issue the stop, and +// KillMode=control-group then collects the grandchildren. What would defeat ExitType=main is a main +// process that OUTLIVES the incarnation -- which is exactly run.sh's return-code-2 relaunch loop. +// +// WHAT THIS PREDICATE DOES NOT PROVE, stated so it is not cited for more. It is a static property +// of unit configuration: it says a stop is issued and reaches the cgroup. It does not say the +// processes are gone afterwards (a task in uninterruptible sleep survives a pending SIGKILL), it +// does not cover a main process that stays alive across the incarnation's end, and it does not say +// the cell is safe to reuse. Those are runtime facts, owned by a terminalizer's readback and by +// gunbc.product.fabric.sanitation's CellReadiness, and no Bool over two directives can stand for +// them. +fn lifecycle_intent_stops_finished_incarnation(intent: RunnerUnitLifecycleIntent, main_exits_when_incarnation_ends: Bool) -> Bool { systemd_kill_mode_reaches_whole_cgroup(mode: intent.kill_mode) && match intent.exit_type { - ExitTypeCgroup => true - ExitTypeMain => listener_is_main_process + ExitTypeMain => main_exits_when_incarnation_ends + ExitTypeCgroup => false } } -// THE DECLARED RESTING FORM, AND IT IS FORCED BY MEASUREMENT RATHER THAN CHOSEN. +// THE DECLARED RESTING FORM: ExitType=main WITH KillMode=control-group. // -// The preferred form was that the listener become the tracked main process, because then nothing -// has to wait on a cgroup to know the service is over. That form is UNREACHABLE without forking -// run.sh -- vendor code that also carries the return-code-2 relaunch loop and the deprecation exit -// path -- so it is not on the table, and this row records that as the reason rather than presenting -// ExitTypeCgroup as a preference. +// An earlier revision declared ExitType=cgroup, on the reasoning that the listener could not +// become the tracked main process without forking run.sh. The premise holds -- run.sh does not +// exec -- but it was never the deciding fact: the listener does not need to be MainPID for +// ExitType=main to work, because run.sh itself exits when the incarnation ends, and that exit is +// what issues the stop. ExitType=cgroup was the configuration that turned every surviving process +// into a slot held indefinitely (see the predicate above). It is retracted, not kept beside the +// corrected form. // // WHAT THE OTHER HALF FIXES, MEASURED BY EXECUTION ON srv4-04 2026-08-25. An explicit // `systemctl restart` of an idle slot killed the main process and NOTHING ELSE: the outgoing @@ -234,8 +256,8 @@ fn lifecycle_intent_cannot_orphan(intent: RunnerUnitLifecycleIntent, listener_is // drop-in, and a needrestart deferral so the upgrade stops issuing the restart. // // THE DECLARED INTENT DOES NOT DEPEND ON THAT CHAIN, WHICH IS WHY THE RETRACTION DOES NOT MOVE IT. -// ExitTypeCgroup plus KillModeControlGroup is warranted by what a teardown must reach, and by the -// executed fact that today's teardown reaches only the main process. Whether the ordinary path +// KillModeControlGroup is warranted by what a teardown must reach, and by the executed fact that a +// KillMode=process teardown reaches only the main process. Whether the ordinary path // detaches lineages by that route or another, a stop that does not reach the cgroup cannot collect // them. // @@ -246,11 +268,16 @@ fn lifecycle_intent_cannot_orphan(intent: RunnerUnitLifecycleIntent, listener_is // lane -- srv1-01 showed many restarts and no surplus while srv4-03 showed none and several // detached generations, so it is diagnostic metadata and never the subject. data gunbc_runner_lifecycle_intent: RunnerUnitLifecycleIntent = RunnerUnitLifecycleIntent { - exit_type: ExitTypeCgroup, + exit_type: ExitTypeMain, kill_mode: KillModeControlGroup, } -// THE LISTENER IS NOT THE MAIN PROCESS ON THIS FLEET, stated as its own row because it is the input -// the predicate above needs and it is an observation about vendor code rather than a choice. It -// changes only if run.sh changes or is replaced. -data gunbc_runner_listener_is_main_process: Bool = false +// run.sh EXITS WHEN THE INCARNATION ENDS, stated as its own row because it is the input the +// predicate above needs and it is an observation about vendor code rather than a choice. In the +// pinned runner, run-helper.sh returns 0 -- and run.sh exits -- for listener codes 0, 1, 5 and any +// unknown code; it returns 2, and run.sh relaunches in place, for listener codes 2, 3 and 4 (the +// self-update and retryable paths). An ephemeral runner finishing its one job returns 0. The +// relaunch arm is the residual this row does not cover: there the incarnation ends while MainPID +// lives, no stop is issued, and collecting the outgoing incarnation is the terminalizer's +// obligation, not this unit's. This changes only if run.sh changes or is replaced. +data gunbc_runner_main_exits_when_incarnation_ends: Bool = true diff --git a/dag/gunbc/runner/runner_unit_file.dag b/dag/gunbc/runner/runner_unit_file.dag index c7fe7f7c0c9..3bcc1df3a0e 100644 --- a/dag/gunbc/runner/runner_unit_file.dag +++ b/dag/gunbc/runner/runner_unit_file.dag @@ -73,9 +73,9 @@ data gunbc_runner_unit_file_scope_disposition: Disposition = SingleAuthority // THE RUNNER UNIT, MODELLED RATHER THAN COPIED. // // `gunbc.runner_unit` already owns what a runner unit is NAMED and, since #9235, what its teardown -// must GUARANTEE -- `RunnerUnitLifecycleIntent` plus `lifecycle_intent_cannot_orphan`, which proves -// that a stop cannot leave a live process behind only when the kill reaches the whole cgroup AND -// systemd does not call the service finished while processes remain. That intent was declared and +// must GUARANTEE -- `RunnerUnitLifecycleIntent` plus `lifecycle_intent_stops_finished_incarnation`, which holds +// only when a finished incarnation makes systemd ISSUE a stop (the main process exits under +// ExitType=main) AND that stop reaches the whole cgroup (KillMode=control-group). That intent was declared and // UNROUTED: nothing rendered a unit, so the fleet's live template still carries `KillMode=process` // and no `ExitType=` at all, and the property the repository had proved was true of nothing. // @@ -115,8 +115,8 @@ data gunbc_runner_unit_file_scope_disposition: Disposition = SingleAuthority // this shape. Removing it would look like tidying and would stop the fleet under load. // // TimeoutStopSec=5min -- how long a stop is allowed before SIGKILL. It becomes MORE load-bearing -// under the teardown fix below, not less: `ExitType=cgroup` means the stop now waits on the whole -// cgroup, so this is the bound on that wait. +// under the teardown fix below, not less: once the stop reaches the whole cgroup, this is the bound +// after which a survivor that ignores SIGTERM is SIGKILLed (measured on srv1 2026-09-18). // THE ON-HOST APP KEY PATH, WHICH IS THE MATERIALIZATION OF A SECRET THAT ALREADY HAS AN AUTHORITY. // @@ -254,7 +254,7 @@ fn runner_unit_jobserver_wants(scope: CompileParallelismRealization) -> List List { diff --git a/dag/test/claim/runner/runner_host_file_converge_witness_test.dag b/dag/test/claim/runner/runner_host_file_converge_witness_test.dag index 717b183eca2..6628183e8f8 100644 --- a/dag/test/claim/runner/runner_host_file_converge_witness_test.dag +++ b/dag/test/claim/runner/runner_host_file_converge_witness_test.dag @@ -2,7 +2,7 @@ module test.claim.runner_host_file_converge_witness_test import std.types { Bool, String, NonEmptyStr, Int } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } -import extdeps.systemd.unit_file { ExitTypeMain, KillModeProcess, serialize_systemd_drop_in } +import extdeps.systemd.unit_file { ExitTypeMain, ExitTypeCgroup, KillModeControlGroup, KillModeProcess, serialize_systemd_drop_in } import extdeps.needrestart { NeedrestartUnitNamePrefixAdmitted, NeedrestartUnitNamePrefixRefused, @@ -13,8 +13,8 @@ import product.placement_supply { HostIdentity } import gunbc.runner_unit { RunnerUnitLifecycleIntent, gunbc_runner_lifecycle_intent, - gunbc_runner_listener_is_main_process, - lifecycle_intent_cannot_orphan, + gunbc_runner_main_exits_when_incarnation_ends, + lifecycle_intent_stops_finished_incarnation, runner_unit_prefix, runner_unit_name_of_registration, } @@ -132,7 +132,7 @@ fn srv1_desired_population() -> RunnerHostFileDesiredPopulation { // THE ORACLE IS WRITTEN HERE, NOT DERIVED. systemd.unit(5) drop-in grammar: a section header, one // directive per line, a terminating newline. If the renderer and this string ever agree because both // moved, the witness has become a restatement, so the literal stays literal. -data expected_teardown_dropin_text: String = "[Service]\nExitType=cgroup\nKillMode=control-group\n" +data expected_teardown_dropin_text: String = "[Service]\nExitType=main\nKillMode=control-group\n" test fn the_teardown_dropin_carries_the_declared_pair_and_nothing_else() -> Bool { gunbc_runner_unit_teardown_dropin_text() == expected_teardown_dropin_text @@ -144,13 +144,17 @@ test fn the_teardown_dropin_lands_in_the_runner_template_dropin_directory() -> B // THE DISCRIMINATING RED, AS THE LIVE FLEET CARRIES IT. `KillMode=process` with systemd's default // `ExitType=main` is what srv1 reported on 2026-09-11. Rendering that pair through the same function -// must produce different bytes, and the orphan predicate must refuse it, or the drop-in is a -// decoration that would read green whatever the fleet did. +// must produce different bytes, and the predicate must refuse it, or the drop-in is a decoration that +// would read green whatever the fleet did. The ExitType=cgroup drop-in this one replaces is the second +// red: it is what the fleet carries on 2026-09-18, and a revert to it must not read green. test fn the_live_teardown_pair_renders_differently_and_can_orphan() -> Bool { let live = RunnerUnitLifecycleIntent { exit_type: ExitTypeMain, kill_mode: KillModeProcess } + let exittype_cgroup_dropin = RunnerUnitLifecycleIntent { exit_type: ExitTypeCgroup, kill_mode: KillModeControlGroup } serialize_systemd_drop_in(drop_in: runner_unit_teardown_dropin(intent: live)) != expected_teardown_dropin_text - && !lifecycle_intent_cannot_orphan(intent: live, listener_is_main_process: gunbc_runner_listener_is_main_process) - && lifecycle_intent_cannot_orphan(intent: gunbc_runner_lifecycle_intent, listener_is_main_process: gunbc_runner_listener_is_main_process) + && !lifecycle_intent_stops_finished_incarnation(intent: live, main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends) + && !lifecycle_intent_stops_finished_incarnation(intent: exittype_cgroup_dropin, main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends) + && serialize_systemd_drop_in(drop_in: runner_unit_teardown_dropin(intent: exittype_cgroup_dropin)) != expected_teardown_dropin_text + && lifecycle_intent_stops_finished_incarnation(intent: gunbc_runner_lifecycle_intent, main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends) } // The needrestart snippet, against upstream's syntax: an assignment into the override_rc hashref, @@ -405,7 +409,7 @@ fn standing_wire_of(st: RunnerSlotUnitStanding) -> String { } test fn the_declared_pair_on_a_loaded_current_unit_is_effective() -> Bool { - standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "control-group", exit: "cgroup"), intent: gunbc_runner_lifecycle_intent)) == "effective" + standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "control-group", exit: "main"), intent: gunbc_runner_lifecycle_intent)) == "effective" } // THE FALSE-POSITIVE RED. systemctl shows a unit it has not loaded with the manager's DEFAULTS, and the @@ -422,11 +426,12 @@ test fn a_unit_needing_reload_is_pending_whatever_it_reports() -> Bool { && standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "yes", kill: "process", exit: "main"), intent: gunbc_runner_lifecycle_intent)) == "reload-pending" } -// srv1's and srv2's live reading (2026-09-11), and each half alone. +// srv1's and srv2's live reading before the teardown drop-in (2026-09-11), the ExitType=cgroup drop-in +// that replaced it (2026-09-18), and a partial kill mode alone. test fn the_live_reading_and_each_half_alone_are_not_effective() -> Bool { standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "process", exit: "main"), intent: gunbc_runner_lifecycle_intent)) == "not-effective:process:main" - && standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "control-group", exit: "main"), intent: gunbc_runner_lifecycle_intent)) == "not-effective:control-group:main" - && standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "mixed", exit: "cgroup"), intent: gunbc_runner_lifecycle_intent)) == "not-effective:mixed:cgroup" + && standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "control-group", exit: "cgroup"), intent: gunbc_runner_lifecycle_intent)) == "not-effective:control-group:cgroup" + && standing_wire_of(st: classify_runner_slot_unit(reading: reading(load: "loaded", reload: "no", kill: "mixed", exit: "main"), intent: gunbc_runner_lifecycle_intent)) == "not-effective:mixed:main" } // ── The slot population ────────────────────────────────────────────────────────────────────────── @@ -450,7 +455,7 @@ test fn the_population_is_desired_units_then_loaded_extras() -> Bool { ) == ["actions-runner@srv1-01.service", "actions-runner@srv1-03.service", "actions-runner@srv1-02.service", "actions-runner@srv1-38.service"] } -data show_fixture: String = "Id=actions-runner@srv1-01.service\nLoadState=loaded\nNeedDaemonReload=no\nExitType=cgroup\nKillMode=control-group\n\nId=actions-runner@srv1-02.service\nLoadState=loaded\nNeedDaemonReload=no\nExitType=main\nKillMode=process\n\nId=actions-runner@srv1-03.service\nLoadState=not-found\nNeedDaemonReload=no\nExitType=main\nKillMode=control-group" +data show_fixture: String = "Id=actions-runner@srv1-01.service\nLoadState=loaded\nNeedDaemonReload=no\nExitType=main\nKillMode=control-group\n\nId=actions-runner@srv1-02.service\nLoadState=loaded\nNeedDaemonReload=no\nExitType=main\nKillMode=process\n\nId=actions-runner@srv1-03.service\nLoadState=not-found\nNeedDaemonReload=no\nExitType=main\nKillMode=control-group" fn population_wires(units: List) -> List { map( diff --git a/dag/test/claim/runner/runner_local_state_witness_test.dag b/dag/test/claim/runner/runner_local_state_witness_test.dag index 99c10a5969b..f8292bedc96 100644 --- a/dag/test/claim/runner/runner_local_state_witness_test.dag +++ b/dag/test/claim/runner/runner_local_state_witness_test.dag @@ -33,9 +33,9 @@ import gunbc.runner_unit { RunnerUnitInstanceMalformed, RunnerUnitInstance, RunnerUnitLifecycleIntent, - lifecycle_intent_cannot_orphan, + lifecycle_intent_stops_finished_incarnation, gunbc_runner_lifecycle_intent, - gunbc_runner_listener_is_main_process, + gunbc_runner_main_exits_when_incarnation_ends, } import gunbc.runner_local_state { RunnerUnitObservation, @@ -261,49 +261,45 @@ test fn witness_only_cgroup_reaching_kill_modes_reach_the_cgroup() -> Bool { && !systemd_kill_mode_reaches_whole_cgroup(mode: KillModeNone) } -// THE PAIR IS WHAT DECIDES ORPHANING, NOT EITHER HALF. KillMode=control-group with ExitType=main -// under a wrapper that does NOT exec is the trap: the teardown would reach the cgroup, but systemd -// considers the service finished when the wrapper exits, so that teardown is never issued for the -// survivors. This witness goes red if the predicate is weakened to consult kill_mode alone. -// THE FOUR CASES, IN THE ORDER THAT MAKES THE PAIR LOAD-BEARING. ExitTypeMain is sufficient ONLY -// when the listener is the main process -- the unreachable form -- and is exactly the trap when it -// is not, which is this fleet. ExitTypeCgroup is sufficient regardless. A kill mode that leaves -// children behind is never sufficient, whatever the exit type says, so the last two cases go red -// if the predicate is ever weakened to consult exit_type alone. -test fn witness_orphan_freedom_needs_both_halves() -> Bool { +// THE PAIR DECIDES, NOT EITHER HALF, AND THE CASES ARE THE srv1 2026-09-18 MATRIX. ExitType=main +// issues a stop when MainPID exits, and KillMode=control-group carries it to the whole cgroup: that +// pair stops a finished incarnation. ExitType=main with a main process that outlives the incarnation +// (run.sh's return-code-2 relaunch loop) issues no stop. ExitType=cgroup issues no stop while any +// process survives -- the srv2-02 incident -- so it refuses whatever the kill mode. A kill mode that +// leaves children behind refuses whatever the exit type. Weakening the predicate to consult either +// half alone turns one of these arms green. +test fn witness_stopping_a_finished_incarnation_needs_both_halves() -> Bool { let cg_main = RunnerUnitLifecycleIntent { exit_type: ExitTypeMain, kill_mode: KillModeControlGroup } let cg_cgroup = RunnerUnitLifecycleIntent { exit_type: ExitTypeCgroup, kill_mode: KillModeControlGroup } - let proc_cgroup = RunnerUnitLifecycleIntent { exit_type: ExitTypeCgroup, kill_mode: KillModeProcess } - lifecycle_intent_cannot_orphan(intent: cg_main, listener_is_main_process: true) - && !lifecycle_intent_cannot_orphan(intent: cg_main, listener_is_main_process: false) - && lifecycle_intent_cannot_orphan(intent: cg_cgroup, listener_is_main_process: false) - && !lifecycle_intent_cannot_orphan(intent: proc_cgroup, listener_is_main_process: false) - && !lifecycle_intent_cannot_orphan(intent: proc_cgroup, listener_is_main_process: true) -} - -// THE DECLARED INTENT IS ORPHAN-FREE ON THE FLEET AS MEASURED, AND THIS IS THE WITNESS THAT BINDS -// THE TWO ROWS TOGETHER. Declaring a lifecycle intent and separately declaring that the listener is -// not the main process would leave the pair unchecked -- the interesting failure is an intent that -// is sound only under an assumption the fleet does not satisfy. -test fn witness_declared_intent_is_orphan_free_on_this_fleet() -> Bool { - lifecycle_intent_cannot_orphan( + let proc_main = RunnerUnitLifecycleIntent { exit_type: ExitTypeMain, kill_mode: KillModeProcess } + lifecycle_intent_stops_finished_incarnation(intent: cg_main, main_exits_when_incarnation_ends: true) + && !lifecycle_intent_stops_finished_incarnation(intent: cg_main, main_exits_when_incarnation_ends: false) + && !lifecycle_intent_stops_finished_incarnation(intent: cg_cgroup, main_exits_when_incarnation_ends: true) + && !lifecycle_intent_stops_finished_incarnation(intent: proc_main, main_exits_when_incarnation_ends: true) +} + +// THE DECLARED INTENT STOPS A FINISHED INCARNATION ON THE FLEET AS MEASURED, and this binds the two +// rows together: an intent sound only under an input the fleet does not satisfy is the interesting +// failure. +test fn witness_declared_intent_stops_a_finished_incarnation_on_this_fleet() -> Bool { + lifecycle_intent_stops_finished_incarnation( intent: gunbc_runner_lifecycle_intent, - listener_is_main_process: gunbc_runner_listener_is_main_process, + main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends, ) - && !gunbc_runner_listener_is_main_process -} - -// THE MEASURED CURRENT BEHAVIOUR, EXPRESSED AS THE INTENT IT IS INDISTINGUISHABLE FROM. On srv4-04 -// a restart killed the main process and left its own run-helper and listener alive, which is what -// a teardown that does not reach the cgroup does. Whatever directives spell it on that host, the -// contract it BEHAVES as cannot avoid orphaning, and the declared intent above must differ from it -// -- a witness that let the two agree would be green over a change that changed nothing. -test fn witness_the_orphaning_contract_and_the_declared_one_differ() -> Bool { - let as_observed = RunnerUnitLifecycleIntent { exit_type: ExitTypeMain, kill_mode: KillModeProcess } - !lifecycle_intent_cannot_orphan(intent: as_observed, listener_is_main_process: gunbc_runner_listener_is_main_process) - && lifecycle_intent_cannot_orphan( +} + +// BOTH CONTRACTS THE FLEET HAS RUN ARE REFUSED, AND THE DECLARED ONE DIFFERS FROM EACH. KillMode=process +// (srv4-04, 2026-08-25: a restart reaped only MainPID) and the ExitType=cgroup drop-in that replaced +// it (srv2-02 held 2.7 days, srv1-03 and srv1-07 held 16 days) must both read red, or this witness +// would stay green over a revert to either. +test fn witness_both_fleet_contracts_are_refused_and_the_declared_one_is_not() -> Bool { + let killmode_process = RunnerUnitLifecycleIntent { exit_type: ExitTypeMain, kill_mode: KillModeProcess } + let exittype_cgroup = RunnerUnitLifecycleIntent { exit_type: ExitTypeCgroup, kill_mode: KillModeControlGroup } + !lifecycle_intent_stops_finished_incarnation(intent: killmode_process, main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends) + && !lifecycle_intent_stops_finished_incarnation(intent: exittype_cgroup, main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends) + && lifecycle_intent_stops_finished_incarnation( intent: gunbc_runner_lifecycle_intent, - listener_is_main_process: gunbc_runner_listener_is_main_process, + main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends, ) } diff --git a/dag/test/claim/runner/runner_microvm_witness_test.dag b/dag/test/claim/runner/runner_microvm_witness_test.dag index 24978365bf2..b8bd524067c 100644 --- a/dag/test/claim/runner/runner_microvm_witness_test.dag +++ b/dag/test/claim/runner/runner_microvm_witness_test.dag @@ -175,6 +175,15 @@ data deployed_lifecycle_intent: RunnerUnitLifecycleIntent = RunnerUnitLifecycleI } data repaired_lifecycle_intent: RunnerUnitLifecycleIntent = RunnerUnitLifecycleIntent { + exit_type: ExitTypeMain, + kill_mode: KillModeControlGroup, +} + +// THE ExitType=cgroup DROP-IN THE FLEET CARRIES ON 2026-09-18, which an earlier revision of this file +// called the repaired intent. One survivor holds the unit running with no stop issued (srv2-02, 2.7 +// days; srv1-03 and srv1-07, 16 days), so under a lifecycle controller an orphaned VMM would be held +// exactly the same way. +data exittype_cgroup_lifecycle_intent: RunnerUnitLifecycleIntent = RunnerUnitLifecycleIntent { exit_type: ExitTypeCgroup, kill_mode: KillModeControlGroup, } @@ -189,7 +198,22 @@ test fn orphanable_unit_refuses_the_microvm_migration() -> Bool { a: runner_microvm_admission( topology: VmmUnderLifecycleController, intent: deployed_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, + transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, + config: mvp_sized_config(), + reserve: witness_reserve, + ), + ) +} + +// THE INCIDENT FIXTURE AS A RED: the configuration the previous revision admitted must now refuse, +// with the orphan cause, or a revert to it would read green. +test fn exittype_cgroup_unit_refuses_the_microvm_migration() -> Bool { + admission_is_orphan_refusal( + a: runner_microvm_admission( + topology: VmmUnderLifecycleController, + intent: exittype_cgroup_lifecycle_intent, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -197,14 +221,14 @@ test fn orphanable_unit_refuses_the_microvm_migration() -> Bool { ) } -// THE POSITIVE CONTROL. Same VM, same transport, cgroup-reaching teardown: admitted. Without this +// THE POSITIVE CONTROL. Same VM, same transport, the declared intent (ExitType=main, KillMode=control-group): admitted. Without this // arm the refusal above would be satisfied by an admission that refuses everything. -test fn cgroup_teardown_admits_the_same_microvm() -> Bool { +test fn main_exit_teardown_admits_the_same_microvm() -> Bool { admission_is_admitted( a: runner_microvm_admission( topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -221,7 +245,7 @@ test fn shared_slot_directory_credential_is_refused() -> Bool { a: runner_microvm_admission( topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigInSharedSlotDirectory { path: "/opt/actions-runner/srv4-04/.credentials" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -246,7 +270,7 @@ test fn two_root_devices_is_a_malformed_vm() -> Bool { a: runner_microvm_admission( topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: two_root_config(), reserve: witness_reserve, @@ -281,7 +305,7 @@ test fn direct_exec_vmm_is_admitted_under_the_same_orphanable_intent() -> Bool { a: runner_microvm_admission( topology: VmmIsMainProcess, intent: deployed_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -297,7 +321,7 @@ test fn topology_is_what_decides_and_it_decides_both_ways() -> Bool { a: runner_microvm_admission( topology: VmmIsMainProcess, intent: deployed_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -306,7 +330,7 @@ test fn topology_is_what_decides_and_it_decides_both_ways() -> Bool { a: runner_microvm_admission( topology: VmmUnderLifecycleController, intent: deployed_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -321,7 +345,7 @@ test fn direct_exec_still_refuses_the_shared_slot_credential() -> Bool { a: runner_microvm_admission( topology: VmmIsMainProcess, intent: deployed_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigInSharedSlotDirectory { path: "/opt/actions-runner/srv4-04/.credentials" }, config: mvp_sized_config(), reserve: witness_reserve, @@ -400,7 +424,7 @@ test fn the_same_guest_is_refused_under_the_production_reserve() -> Bool { a: runner_microvm_admission( topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: mvp_sized_config(), reserve: witness_unmodeled_reserve, @@ -429,7 +453,7 @@ fn admission_of_machine(vcpus: Int, mib: Int) -> RunnerMicroVmAdmission { runner_microvm_admission( topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, - listener_is_main_process: false, + main_exits_when_incarnation_ends: true, transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, config: config_with_machine(vcpus: vcpus, mib: mib), reserve: witness_reserve, diff --git a/dag/test/claim/runner/runner_slot_retirement_witness_test.dag b/dag/test/claim/runner/runner_slot_retirement_witness_test.dag index f936854b631..7564789549c 100644 --- a/dag/test/claim/runner/runner_slot_retirement_witness_test.dag +++ b/dag/test/claim/runner/runner_slot_retirement_witness_test.dag @@ -108,7 +108,7 @@ test fn a_present_unit_is_pending_rather_than_stopped() -> Bool { } // THE ORPHAN STATE: THE UNIT IS GONE AND ITS CGROUP IS NOT EMPTY. This is the exact class the -// teardown drop-in (ExitType=cgroup, KillMode=control-group) was landed to prevent -- a unit +// teardown drop-in (ExitType=main, KillMode=control-group) was landed to prevent -- a unit // reporting stopped while Runner.Worker, claim_executor and gunbc keep running under it. Capacity // must stay charged, because that work is still holding memory. test fn a_gone_unit_with_a_populated_cgroup_is_not_retired() -> Bool { diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index 98791f0052e..9dbbd0f46b9 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -30,8 +30,8 @@ import gunbc.runner_lifecycle { runner_lifecycle_jit_wrapper_path } import gunbc.runner_unit { RunnerUnitLifecycleIntent, gunbc_runner_lifecycle_intent, - gunbc_runner_listener_is_main_process, - lifecycle_intent_cannot_orphan, + gunbc_runner_main_exits_when_incarnation_ends, + lifecycle_intent_stops_finished_incarnation, } import gunbc.runner_host_deploy { admitted_deploy_for, @@ -114,7 +114,7 @@ fn as_installed_intent() -> RunnerUnitLifecycleIntent { test fn the_rendered_unit_carries_the_declared_teardown_pair() -> Bool { let text = rendered_text(intent: gunbc_runner_lifecycle_intent) - string_contains(s: text, pattern: "\nExitType=cgroup\n") + string_contains(s: text, pattern: "\nExitType=main\n") && string_contains(s: text, pattern: "\nKillMode=control-group\n") } @@ -126,16 +126,17 @@ test fn the_as_installed_teardown_renders_differently_and_cannot_be_mistaken_for } // The property the unit exists to hold, joined to the render rather than asserted beside it: the -// intent this module renders satisfies it on this fleet, and the pair the fleet currently runs does -// not. Both arms are needed -- without the second, an intent that guaranteed nothing would pass. -test fn the_rendered_intent_is_the_one_that_cannot_orphan() -> Bool { - lifecycle_intent_cannot_orphan( +// intent this module renders satisfies it on this fleet, and the pair the fleet ran before any +// teardown drop-in does not. Both arms are needed -- without the second, an intent that guaranteed +// nothing would pass. +test fn the_rendered_intent_is_the_one_that_stops_a_finished_incarnation() -> Bool { + lifecycle_intent_stops_finished_incarnation( intent: gunbc_runner_lifecycle_intent, - listener_is_main_process: gunbc_runner_listener_is_main_process, + main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends, ) - && !lifecycle_intent_cannot_orphan( + && !lifecycle_intent_stops_finished_incarnation( intent: as_installed_intent(), - listener_is_main_process: gunbc_runner_listener_is_main_process, + main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends, ) } diff --git a/docs/plans/microvm-and-floor-wind-down-state.md b/docs/plans/microvm-and-floor-wind-down-state.md new file mode 100644 index 00000000000..7da9b9fa32a --- /dev/null +++ b/docs/plans/microvm-and-floor-wind-down-state.md @@ -0,0 +1,224 @@ +# microVM and floor: wind-down state, 2026-09-21 + +Written on operator instruction to wind down and record remaining items, so that v1 +performance and v2 migration can be prioritised. **This is a state record, not a plan**: it +says what is true on `origin/main`, what is owed, and what is blocked, so that resuming any +lane does not begin by re-deriving it. + +Every claim below was verified against `origin/main` at `7a145ef9ca` or read from the lane +that produced it. Where a claim is **contested**, it is marked, and neither version is +asserted — DESIGN §4d: a bet is typed as a bet, and the reader who consumes it as a fact is +the defect. + +--- + +## 1. The floor reports SUCCESS over its own refusal — the highest-value open item + +`.github/workflows/witnesses.yml:67`: + +``` +if [ "$GUNBC_FLOOR_CLASS" = structural ] && [ "$GUNBC_FLOOR_EXIT" -eq 0 ]; then GUNBC_FLOOR_CLASS='none' +``` + +`claim_executor` **exits 0 over its own typed refusal**, so the class is downgraded to `none` +and the job concludes success. A job can therefore report SUCCESS over a run that executed +**zero witnesses**, with its own log saying `phases_failed=1`. + +**This is not merely a hidden defect — it admitted a new one.** #11731 landed a file that +could not parse *because* the floor was refusing and reporting success. The hollow gate is +upstream of the breakage, not downstream of it (§5: a failure arm must refuse, never widen; +the downgrade is an absorbing fallback executed in YAML). + +**Current standing.** The parse class is **closed**: the indented-annotation census is 0 +corpus-wide and the floor now executes 412 witnesses +(`planned=412 executed=412 not_attempted=0 terminal=412 passed=397 known_red_held=8`). +Closed by #11896, #11897, #11880, #11920, #11842. + +**CONTESTED — do not propagate either reading.** Whether the downgrade swallows failures +*per phase* is disputed by two lanes: + +| reading | source | consequence if true | +|---|---|---| +| per-phase: parse reds the job honestly, declarations passes | `nimble-swift-273` | once parse cleared, a **declarations defect is invisible** | +| no such ordering | four run observations | the discriminator is unknown | + +The four observations: main `0de0b6137c7` 13 parse FAILs → **SUCCESS**; #11803 `70faed05501` +340 → **SUCCESS**; #11842 343 → **FAILURE**; #11884 317 → **FAILURE**. No ordering by count, +and parse failures did **not** always red the job. `eager-swift-412` independently reports +the discriminator as **cannot-tell from the logs**. + +**The discriminating test nobody has run**, and it is cheap: read `$GUNBC_FLOOR_LOG` — a +**file** the floor writes, *not* the job log, where every `class=` line is echoed script — or +the classifier itself, on **one PASS and one FAIL of the same phase shape**. Counting +signature strings in the GHA job log is **not** discriminating: a fired signature sets an env +var rather than printing, so identical counts appear whether the hypothesis holds or not. + +**#11836 and #11829 are competing repairs. Only one should land.** Neither is owned. + +## 2. microVM: the part that decides is built; the part that acts is not + +`gunbc.runner_microvm_lifecycle_realize` **landed** (#11803) and has executed against real +processes on srv1 — launch 18/18, lifecycle 30/30, realize 6/6, store 17/17, wet receipt +10/10 under `--wet`, argv-binding wall 13/13. #11677 closed both launch frontiers, so the +JIT credential mint and jail staging are realized. + +**Five declared frontiers, all live in that one landed module.** Read them from the file, +not from here. + +| # | frontier | status | what is missing | +|---|---|---|---| +| 1 | `controller_main_pid_consumer_frontier` | **dispatchable, start here** | **nothing calls `run_controller`.** Until a slot unit execs it as MainPID the module is a library, not a controller. Every other frontier is worth less until this clears. | +| 2 | `attempt_cleanup_realization_frontier` | dispatchable | no unmount, no delete of credential device / workspace / attempt root, no flush. The **only** host mutation in teardown is the `cgroup.kill` write. | +| 3 | `guest_bring_up_channel_frontier` | dispatchable, spans host+guest | no guest→host readiness channel above `VmmStarted`. Decides only whether a slot is SERVING, never whether a cell is CLEAN. | +| 4 | `slot_network_readings_producer_frontier` | **BLOCKED — security** | no converged slot network on any host; every reading is `Unreadable`, which quarantines. | +| 5 | `workflow_effect_sequencing_frontier` | **not a lane — a design question** | `std` carries **no** effect-sequencing authority. Bigger than microVM: every effect sequence in the corpus rests on the answer. | + +**The consequence that governs planning:** the module states it itself — *"no cell settles +CellReady through this module today."* **A first full run quarantines by construction, and +that is not a bug in the readbacks.** A warm pool is impossible until (4) clears. + +> Do not let anyone "fix" (4) by omitting `SlotNetworkQuiescent` from the required facts. +> That is the empty-observation narrow `product.fabric.sanitation` exists to refuse. + +### Why (4) is blocked, stated so the reason survives + +**The converge principal IS the job principal.** Granting it install+restart over files it +also *stages* is granting root: `install /etc/systemd/system/…` +followed by `systemctl restart` is root-equivalence, however narrowly spelled. So +`microvm_network_granted_operations` deliberately carries **readbacks only**. + +To unblock, an administrator principal must (1) own the staged source so the job user cannot +write what root will install and execute; (2) install the nft loader unit and ruleset and +`daemon-reload` + restart it; (3) set `ip_forward` and create the bridge; (4) create and +destroy per-attempt taps — and be **unimpersonable by the job user**. That last is the whole +point, and is why the frontier trigger names a *capability* rather than an artifact (§4b(3)). + +#11751 (`microvm_network_observe`) is in the merge queue at `cd2041cc69a`. It **installs +nothing**, reads every fact with its own UNREAD arm, and mints `ConvergedNetwork` only when +every fact was actually read. On every host today it will **refuse**, because nothing has +installed a tap or the table — that is honest, not a failure. + +### The floor's own job does not fit a cell + +`runner_microvm_floor_fit_stall` remains rostered: ~26.8 GB held-set peak against +`gunbc_runner_slot_memory_max_bytes = 27917287424` (26 GiB) less a 1 GiB realization reserve. + +**Grounding it is an operator decision with a fleet cost**, not an engineering task: raise +per-slot `MemoryMax` to ~28 GiB, which **lowers each host's memory-admitted width**, or +reduce floor demand. The stall explicitly rules out deleting the allowance, reserve or +receipt, and rules out using a fixture cell. + +### The milestone that would settle the cutover question + +**One cell settling `CellReady` once, on one host, after one real job.** Nothing before that +is evidence. If that cannot be reached, the remaining work is unbounded. + +## 3. Dynamic per-VM memory — two compiling, unreconciled implementations + +Design ruled and approved by the side chat; **build parked**. Six items; item 1 is built +**twice, independently, blind to each other**. + +**Neither branch is uncompiled.** The uncompiled attempts are the two *closed* PRs, #11849 +and #11850. + +| branch | sha | evidence | carries uniquely | +|---|---|---|---| +| `session/bright-ram-63` | `125659f70df` | 16/16 PASS + five mutation controls | the **executed** authority-token wall | +| `session/royal-moth-544` | `80ec5065822` | 14/14 + 4/4 PASS, two mutation controls | `std.measure round_up_to_grain` (resolves the unowned rounder fork), ceiling-as-parameter, permit-in-provenance | + +The same three file paths exist on both with different contents, so **merging them is a +textual conflict on every file, not a union.** Pick one base and port the other's evidence. + +**Both PRs (#11883, #11885) were found NON-DRAFT on 2026-09-21, although both lanes believed +they had left them draft** — so a parked program was consuming CI and reviewer attention on +every push. Both were converted back to draft at wind-down. Keep them draft while parked: +ready buys coverage that was never approved. *The lesson is the gap itself* — "I left it +draft" is a belief about a past action, and the dashboard opens PRs on a lane's behalf, so +it must be re-read rather than remembered. + +**The defect, stated correctly** (it is a bypass, not an absence). All three verified against +`origin/main`: + +- `CellReserved` holds exactly four fields — offer, slot_key, generation, account. **No + requirement, no grant, no envelope.** +- `admit_executor_capacity` takes a whole `ExecutionRequirements` and reads exactly **one** + field, `requirements.capacity_class`. **Cell admission does not consider memory.** +- `unmet_memory_axis` returns `[]` when `needed.envelope.memory` is `Absent`, so **unstated + memory is admitted** by the supply screen rather than refused. + +So memory *is* screened before reservation and the runner *does* read the requirement; what +is missing is that memory is never converted into a **grant**, never **atomically reserved** +against live host use, and never **carried on `CellReservation`**. + +`MemoryGrant` and `HostMemoryLedger` return **zero matches anywhere on main**, so items 3-6 +have no landed symbols to integrate against. The coordination hazard for item 4 (#11625, +static-vs-dynamic `MemoryHigh`/`MemorySwapMax`) is still **open**, but its head has moved to +`8e75da2aa48` — re-read it before item 4 rather than trusting any recorded sha. + +**Topology precondition, a gate rather than an item:** exact per-Work sizing is valid only +where Work is bound **before** the VM boots. A generic prebooted GitHub runner does not know +its eventual job. Do not let a guest discover its Work after boot and call that dynamic +allocation. + +**Amendment worth not re-litigating:** a per-host **CAS-linearized** ledger is required. +Per-cell records cannot conserve a host-wide sum — A and B each read 60 of 100 free, each +reserve 30, both succeed, 120 committed. One CAS commits cell occupancy and memory claim +together. + +## 4. Owed evidence + +**#11845's discriminating RED was never executed.** The repair is real and approved, and it +lands on a green that is hollow for the two reasons in §1. Branch +`verify/11845-red-mutation` (`2499194f4b2`) is pushed and is exactly one hunk off the merge +head: the `test -e` defect put back inside the new classifier. **Both of its blockers have +since cleared**, so the pair is now runnable — expect green at the merge head, red at +`2499194f4b2` on `an_unread_path_reaches_unobservable_and_never_absent`. **If the mutation +passes, the control does not discriminate and the repair needs a better one.** Delete that +branch afterwards; `verify/11845-red-control` is plain main and can go now. + +**Two unowned repairs**, both one-liners, both real: + +- `v2.lens.reference_derived_residency_reading` has zero occurrences of + `construction_justification`, while its siblings import it from `v2.lens.common`. +- `dag/test/claim/machine_intake/jade_first_contact_model_witness_test.dag:3` imports `Nat` + from `std.types`; `Nat` is declared in `dag/std/nat.dag`. + +**`required_gate_prefixes` has no `dag/test/claim/runner/` row**, so that file is never +resolved by CI unless a diff touches it — a symbol deletion can strand it silently, as +#11762 did. Likewise no row matches `test.claim.fabric.`, so the dynamic-memory witnesses are +discovered and declined. + +## 5. The P0 that opened this session is contained but not closed + +srv2 still carries `ExitType=cgroup` in +`/etc/systemd/system/actions-runner@.service.d/70-fleet-teardown.conf` — the configuration +that left PID 56295 orphaned holding 16 GB for 2.7 days. srv1 and srv3 are converged to +`ExitType=main`. + +**Residual risk, precisely.** srv2-01..05 are **masked**, so the P0 cannot recur on them +today. But the drop-in lives in the **template** directory and the template is *not* masked, +so any **new** instance (`actions-runner@srv2-06`) inherits `ExitType=cgroup`. The remedy is +to run the modelled fleet converge on srv2; it has simply never run there. + +srv4 is off the reach chain (container → srv1 → srv2-lan → srv3) and `gunbc.fleet_reach` +carries no row for it. + +## 6. Method findings worth keeping + +- **A suite of controls that invoke a pure decision with supplied values is blind to + everything after the decision** — the cleanup leg, the receipt the withheld arm writes — + and stays blind however many are added. Two post-sign-off findings on #11902 both lived in + that one gap. **38/38 is not route coverage.** +- **A repair of a fail-open is a prime site for the same class one layer down.** #11902's + own (d) repair discarded the located cause on its withheld arm and wrote a constant. Grep + every declaration your repair *adds* for a call site before pushing, and re-read every new + refusal arm for whether it names which fact failed. +- **At any power-of-two grain, a checked-add rounder and a subtraction rounder refuse the + same set**, because 2^63 is a multiple of the grain. A gibibyte-grain mutation control + stayed green under the mutation. Use a non-power-of-two grain (1000). Two authors asserted + the opposite from reasoning alone; both were wrong. +- **A refusal-arm claim tests that the arm fires, not that the right inputs reach it.** That + is how two lanes and a reviewer converged on bounding by the maximum instead of by + representability. +- **`claim_batch` exits 0 over its own refusal.** A `*Refused` line is a **non-answer** — + neither pass nor fail — and exit status must never be read as the verdict.