Repository navigation
microVM wet lifecycle controller: MainPID realization + srv1 REDs - #11809
gunbai-bot[bot] wants to merge 21 commits into
Conversation
… store I/O Not yet typechecked. Carries: - extdeps.linux.cgroup_v2: cgroup.procs as its own interface file, a single-file decoder and a whole-subtree decoder over one tree read - extdeps.tools.grep: every-line-of-one-file-name-under-a-tree, as an ArgvCommand - extdeps.systemd: KillSignal, SendSIGKILL and TimeoutStopSec properties; a Kill operation on systemctl; SystemctlKill on gunbc.host_operation_exec - extdeps.tools.coreutils_stat: PathMode, zero-padded to the four digits extdeps.access.posix file_mode_octal already serializes - product.fabric.sanitation: admit_sanitation_fact, the inverse of the label - gunbc.runner_microvm_lifecycle: StopOutcomeUnobserved, so a stop whose readback failed is not reported as a stop - gunbc.runner_microvm_lifecycle_realize: the subtree readback, the resource absence readbacks, the bounded stop, and the teardown settlement - gunbc.runner_microvm_cell_readiness_store: the record codec and the store I/O Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…clauses - extdeps.linux.cgroup_v2: cgroup.freeze as its own interface file and a subtree decoder, so anything that freezes a cgroup can read back that nothing under a slice is still frozen - gunbc.runner_microvm_lifecycle_realize: read_slice_freeze_state, stating plainly that it cannot make a thaw unconditional and what it does instead - the wet witness sweeps for BOTH a live process and a frozen cgroup - gunbc.ci.ci_layer_roots: the wet file is OfflineLocalRecipe, so the floor can never select a claim that starts systemd units - dropped the uses clauses: gunbc.host_operation_exec and gunbc.scm.init invoke the same operations and resource methods without them Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…port gunbc.runner_observed_version_check observe_captured_console is the closest production analogue and declares it; the resource-method sites (gunbc.scm.init, gunbc.host_operation_exec) do not, and neither does the wet witness in dag/test/claim/spark. So the clause goes on the production chain that reaches run_shell_command_observe and nowhere else. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ent_supply Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…y name A resource is proven absent by a listing of its directory that does not name it, so the reader needs the NAME, not the rendered path. It was spelling "jail" and "jit.img" itself, which is a second authority for a composition runner_microvm_attempt performs; the four names are rows there now and both sides read them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… still owed admit_next_incarnation and settle_and_record_attempt_teardown are the store's production consumers: the admission reads the records the host holds and the terminal path performs the write the settlement already decided on, rather than composing a second one. record_attempt_started is the in-flight half. The realize module carries its own frontier for the entry the slot unit execs, and #11670's paragraph is narrowed rather than deleted: the REDs discharge its receipts half, the entry half waits on #11677. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ts edge TWO DEFECTS FOUND BY TRYING TO EXECUTE THE TEARDOWN RATHER THAN BY READING IT. The jail root and the credential drive live inside the attempt directory, so their absence is established by listing THAT directory -- which after a teardown that did its job does not exist. Listing a directory that is gone establishes nothing, so reading the three subjects independently made the CLEAN outcome unobservable: every successful teardown would have quarantined its own cell on two facts it could not read, and the cell would never be released. An established absence of the container now answers for what is under it; only an attempt directory still THERE is listed. And the readbacks had no dependency edge to the stop. In a pure dependency graph that is not an ordering at all -- a reading with no edge may be evaluated on either side of the thing it is supposed to follow, and a cgroup read before the stop answers about a cell that was still running. The stop is bound first and handed to each readback, which is how a graph says 'after'. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… supplied READING BLANK AS DOUBT DEADLOCKS THE CELL. systemd removes a slice's cgroup as soon as the last unit in it exits, which is the state a SUCCESSFUL teardown leaves -- so a readback that called that unobservable could never release a cell, and gunbc.runner_microvm_cell_readiness's own rule that the first incarnation needs a readback establishing the empty cell could never be satisfied by any cell. systemctl show exiting 0 with no value is the manager affirming it holds no control group under a name derived from THIS cell, which is the same shape as a listing that does not name an entry. A manager that could not ANSWER stays its own arm. RED 4 is restated with the split stated: a genuine cgroup read failure cannot be produced on a serving host without breaking it, so the unreadable reading is supplied at its own boundary and assembled through the production constructor; the never-released half -- the write, the refused release, and the read back off disk -- executes for real. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
readback_ordered_only_by_statement_position: writing an observation after an effect says nothing in a dependency graph; what orders them is an edge. absence_proof_whose_premise_the_success_destroys: an absence established through a container, where the success being proven deletes the container -- so the CLEAN case is the one case the proof cannot observe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
systemctl stop exits nonzero when the job fails, which is exactly what a unit whose child ignores SIGTERM under SendSIGKILL=no produces -- the central case this controller exists for -- and also what an unknown unit produces. Folding both into a refusal reported the ignoring child as an UNOBSERVED stop and never forced it, which is the arm that leaks a VMM. The distinction drawn is the one the transport can make: whether the command reached the manager. What happened to the processes is the cgroup's answer, read next -- and reading it inside the match arm is what puts it after the stop in the graph. Same treatment for the kill, whose exit is the manager's status and not the signalled process's. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A process that moved itself into a sibling scope under the same slice is accounted to the cell, invisible to a kill aimed at the unit, and survives a force that only signals the unit -- which is the escapee RED's whole subject, and it would have made the successful-job RED quarantine for residue the controller could not remove. So the graceful stop stays the ATTEMPT's (its own unit, SendSIGKILL=no, nothing escalating behind the controller) and the force becomes the CELL's: a write of 1 to the slice cgroup's cgroup.kill, which the kernel documents as killing the cgroup and all its descendants, atomically with respect to forking. A frozen task still survives it, which is correct: the task is there, the readback finds it, the cell quarantines. systemd.Systemctl.Kill and its host_operation_exec variant are deleted rather than left standing -- nothing consumes them now, and a modeled operation with no consumer is the dangling modeling DESIGN 3c refuses. The wet witness stops the service itself for the escapee read, because there the subject is the READ and the stop is the world it is taken in; and the escapee REDs wait for the scope to register before observing, since a read taken the instant the service starts can find a slice that is legitimately still empty and would report a test that never ran as a pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The two operations sat between Kill and MaskNow, and removing Kill removed the range up to MaskNow -- taking both with it and leaving their annotation standing over nothing. srv1's typecheck caught it at the two call sites as 'receiver type Primitive(systemd.Systemctl) establishes no method surface', which is the resource boundary refusing a method whose declaration is gone. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s an edge The claims are start, act, observe, sweep -- and they were independent lets with no edges between them, which in a dependency graph is not a sequence. A sweep evaluated before the controller's stop would kill the adversary first and the stop would report StoppedGracefully: a green for a controller that did nothing. Every world-changing step now takes a Bool derived from the step it must not precede. Same class as the production defect filed as readback_ordered_only_by_statement_position, in the file that was supposed to catch it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…serted Slot indices 90-95 were safe because I said a fleet host carries tens. Now gunbc.runner_slot_allocation runner_slot_membership answers it: a unit cannot be started on an identity that authority calls a committed member, whatever this file's indices are edited to and whatever the width becomes. The width is a minimum over the host's CPU, memory and disk axes, so a fleet that grew past ninety would refuse rather than collide. The control runs per PR in the hermetic witness, where a width that outgrew the indices goes red BEFORE anyone runs the wet file -- with the other direction asserted too, since a predicate that answered disjoint for everything would establish nothing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t is not true The file said every claim starts a transient unit and ends with the host as it found it. RED 4 starts no unit -- its subject is a reading no host can be asked to produce safely -- and it wrote two durable records and left them. It now deletes the record and reads back that the cell holds none, which is the same standard the teardown claims are held to: a deletion nobody checked is a teardown nobody read back. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… is eager I wrote that a readback with no edge to its effect 'may be evaluated on either side of it', which overstates what is true today. v1_interpreter eval_call evaluates every argument before the call, unconditionally and in order, so position DOES order these under the seed and no wrong reading has been observed. The defect is that the ordering rested on the executor's strategy rather than on the graph -- invisible while that strategy holds, and silently changed by a second realization or by a demand engine that defers what nothing asks for. The row and both annotations now say that, including that the parameter is not evidence of a caught bug. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… in-flight record controller_start had no production consumer -- begin_attempt is it. The ground is no longer a supplied value: it is a listing of the attempt root that does not name this attempt, read the same way the teardown reads it, with the UNREADABLE arm answering OCCUPIED because a ground nobody could read is not a clear one and the cost of that direction is a launch rather than a leak. The cell is derived from the identity's own slot rather than supplied beside it, so the admission asked for and the binding performed cannot disagree. The write performed is the one the decision's arm carries, never one composed here; recovery writes nothing, because what is owed there is the terminal path for the attempt that never settled. This is the part of the brief that does not need #11677. What still waits on it is the stage-and-launch step between these two halves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
contained_read_plan is the whole content of the rule -- inherit an established absence downward, enumerate a container that is still there, and leave the contents of a container nobody could read unreadable -- and it now has three hermetic claims including the one that matters: an unreadable container must NOT inherit absence, which is one keystroke from the fail-open that releases a cell on a directory nobody could list. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…elper is imported Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Closing: this duplicates #11803, which owns the same two modules ( The work is not lost. Three findings are on #11803 as review comments — a unit-scoped force that a sibling scope under the same slice survives, an unreadable subtree becoming |
The wet half of the microVM slot lifecycle controller: the host readings the decisions in
gunbc.runner_microvm_lifecycle(#11670) have never been taken from, the host-localCellReadinessstore as bytes, and the six REDs executed against real processes.What this is
gunbc.runner_microvm_lifecyclecarries the controller's DECISIONS and takes every observation asa supplied value. Nothing in that lane had run against a process. This adds the module those values
come from —
gunbc.runner_microvm_lifecycle_realize— plusgunbc.runner_microvm_cell_readiness_store, which is the record codec and the store I/O.The split inside the realize module is pure fold beside wet performer: every classification takes
supplied readings and is witnessed hermetically, and every function that touches the host does
nothing but obtain those readings and hand them to a fold.
The six REDs
They are wet
.dagclaims, not a shell script, because a shell reimplementation of stop-then-forcewould establish nothing about the modeled controller. Each one starts its own TRANSIENT unit
through
gunbc.systemd_run_transientwith the PRODUCTION stop properties, drives the productionfold against it, and sweeps its own slice before returning.
trap '' TERMunderSendSIGKILL=noStoppedByForce, never gracefulsystemd-run --scopesibling in the cell sliceForceStopBoundExceeded, and the cell quarantinesNo live slot is touched. Every unit, slice and path is derived by the PRODUCTION functions from
slot indices 90-95. A fleet host allocates slots from
01upward and carries tens of them, notninety, so the derivation collides with nothing serving; the premise is checkable with
systemctl list-units 'actions-runner@*'on any fleet host.On the freezer, and why not a genuinely wedged task. A task the kernel will not reap cannot be
created safely on a serving host and cannot be cleaned up afterwards. A frozen cgroup is a real
survivor of SIGKILL — the signal is not delivered until the cgroup is thawed — and it is reversed
by its own inverse verb. It is also the one residue this run can leave that looks like nothing, so
read_slice_freeze_statereads back that no cgroup under the slice is frozen, and every claim'ssweep asserts it. The reversal cannot be made unconditional inside the substrate — there is no
finalizer and a killed process runs nothing — so the unconditional thaw is an operator command
outside the run, stated on the function rather than implied.
Four things the wet lane found before a host ran it
Derived by walking the success path rather than by a compiler. Three of them would have made a RED
read the wrong way round; the fourth had not yet produced a wrong answer and says so:
attempt directory, whose deletion is what a successful teardown is — so their absence
listings were listings of a directory that is gone, and every successful teardown would have
quarantined its own cell. Absence is now inherited from an established absence of the
container. Filed as
absence_proof_whose_premise_the_success_destroys.the program put them after the effect they describe — and the fields of a record have no order
at all. Stated precisely, because it is the one of the four that had not yet produced a wrong
answer: the seed interpreter is eager, so field order happens to hold today, and the fix moves
the ordering out of the executor's evaluation strategy and into the graph. The stop is bound
first and handed to each readback; the parameter is the word "after". Filed as
readback_ordered_only_by_statement_position, which says the same thing.slice is accounted to the cell and survives a kill aimed at the unit. The graceful stop stays
the attempt's; the force is now a write to the slice cgroup's
cgroup.kill, which the kernelkills the whole subtree with, atomically against forking. A frozen task still survives it,
which is the point of RED 3.
A fourth, smaller: a blank
ControlGroupis the manager affirming it holds no cgroup under thatname, not a doubt — reading it as doubt made a cell whose slice systemd had garbage-collected
unreleasable, which is exactly what a successful teardown leaves behind.
What is supplied rather than executed
Two things, and both are named on the claims that supply them.
The slot NETWORK readback.
gunbc.runner_microvm_networkderives it from seven host readings joinedagainst a
ConvergedSlotNetworkreceipt, and a synthetic slot has no converged network to read;producing one would mean converging a tap and an nft ruleset on a serving host. That boundary's real
execution belongs to that module. Everything else is executed: real units, real stops, real reads of
/sys/fs/cgroup, real listings, real files under the store root.The UNREADABLE CGROUP reading in RED 4. Producing a genuine cgroup read failure on a serving host
means breaking the host — the manager would have to stop answering, or the unified hierarchy would
have to become unreadable to root. So that reading is supplied at its own boundary and assembled
through the production constructor, while the half the brief calls "never released" runs for real:
the quarantine is written to the store as bytes, a Ready settlement at the same generation is
offered and refused, and the store is read back off disk.
What is NOT here
The launch half — jailer/Firecracker bring-up and the #11677 join (a VMM may start only when THIS
attempt's
JitDeviceStagedand the same plan's workspace readiness both hold).attempt_staging_verdictexists only on #11677's branch, and consuming it before that lands would fork it. It is the next
change in this lane, and all six REDs live in the half that is here.
Conformance (DESIGN §3b), for the domains this touches
product.fabric.sanitationCellReadiness, the across-incarnation meaning staysgunbc.runner_microvm_cell_readiness, and this change adds no second verdict: every fold hereproduces a carrier one of those modules already declares. The force targets the CELL because the
cell is what is released.
against the attempt by
attempt_teardown_readback's constructor before any of them can reach averdict. Absence comes from
extdeps.filesystem.filesystem_io's established-absence fold andnever from a failed read; the kernel's own
cgroup.procs,cgroup.freezeandcgroup.killinterfaces are modeled in
extdeps.linux.cgroup_v2beside the ones already there.owes an inverse:
parse ∘ renderis the round trip, the escape covers exactly the threecharacters the two grammars rest on, and every way a record can fail to be a record is one typed
arm. Writes go through
apply_cell_readiness_write— this module asks it and performs only theone file its answer authorises.
extdeps.access.posixposix_root_uid, the required store mode is aFileModerendered byfile_mode_octal(which is whystat -c %04aand not%a), the attempt's entry names becamerows rather than being spelled twice, and the disjointness of the wet slot indices is
runner_slot_membership's answer rather than a sentence.Where every run happened
(Filled in from the srv1 runs. The required CI check executes no
.dagwitness, and the wet file isOfflineLocalRecipeingunbc.ci.ci_layer_rootsso the floor can never select a claim that startssystemd units.)