Record the microVM, floor and per-VM-memory state at wind-down

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(),

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

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

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<Sys
 //
 // Taking the intent as an argument is what lets a witness render the fleet's CURRENT teardown --
 // `ExitType=main` implied by its absence, `KillMode=process` -- and show that the same renderer
-// produces a unit whose property `lifecycle_intent_cannot_orphan` REFUSES. Fixing the pair here as a
+// produces a unit whose property `lifecycle_intent_stops_finished_incarnation` REFUSES. Fixing the pair here as a
 // constant would leave the discriminating case unauthorable, which §4b calls a check that cannot go
 // red.
 fn runner_unit_teardown_directives(intent: RunnerUnitLifecycleIntent) -> List<SystemdServiceDirective> {