diff --git a/dag/extdeps/systemd/systemctl.dag b/dag/extdeps/systemd/systemctl.dag index 876ed292fbf..045e1271052 100644 --- a/dag/extdeps/systemd/systemctl.dag +++ b/dag/extdeps/systemd/systemctl.dag @@ -1,5 +1,6 @@ module extdeps.systemd.systemctl +import extdeps.transports.shell { ShellOutcome } import std.types { NonEmptyStr, List, Bool, Int, Unit } import std.string_type { String } import std.algebra { trim } @@ -595,6 +596,7 @@ service systemd.Systemctl { operation ShowUserProperty { input { unit: NonEmptyStr, property: NonEmptyStr } output { + outcome: ShellOutcome value: String from "stdout" success: Bool from "exit_success" } diff --git a/dag/gunbc/ci/ci_layer_roots.dag b/dag/gunbc/ci/ci_layer_roots.dag index 448b54f0df7..e066acfc7ab 100644 --- a/dag/gunbc/ci/ci_layer_roots.dag +++ b/dag/gunbc/ci/ci_layer_roots.dag @@ -327,6 +327,10 @@ data excl_run_verdict_exit_status_dissolve: DissolutionCondition = unbound_disso data excl_shell_spawn_refused_reason: String = "SUBSTANTIATED per-row: the subject of test.claim.shell_spawn_refused_real_execution_witness is whether the host can spawn argv[0], and whether the seed's shell transport turns a failed spawn into ShellSpawnRefused rather than aborting the evaluation. Both are facts about the real spawn, so the file cannot be made hermetic: a mock_response for test.ShellSpawnProbe.Observed would be authored data, and the discriminating red (an absent binary yields ShellSpawnRefused) would pass against a fabricated refusal whether or not the transport realizes one. Its fns are scheduled in v2.workflow.local_repo_wet_terminal local_repo_wet_schedule, which the required floor executes: the only effect is spawning a local program (true, false, an absent name) -- no network, no cargo, no remote host, no writes." +data excl_manager_unaskable_reason: String = "SUBSTANTIATED per-row, and it is its OWN row rather than a second use of excl_shell_spawn_refused_reason because that reason substantiates a DIFFERENT SUBJECT AND A DIFFERENT EFFECT SET (review 69970): it says in terms that the subject of test.claim.shell_spawn_refused_real_execution_witness is whether the host can spawn argv[0], and that its only effect is spawning a local program. The subject here is a SYSTEMD USER MANAGER -- whether gunbc.compute.work_provider_local read_user_unit_property folds a refused spawn of systemctl into a property that was NOT QUERIED, so the two unit readings reach their own unavailable arm instead of the whole evaluation ending as a shell-spawn-refused runtime error with the seat charged and the producer lease held. The effects are the manager probe, systemctl ShowUserProperty for four unit properties, and a cgroup events read: a superset of the neighbour row's one effect, over a different boundary. DESIGN section 3b: a home that resolves but owns only part of the scope a row claims is a scope/ownership mismatch on the row. The negative half that admits it to the same LANE is the one every member shares: no network, no cargo, no remote host, no install media, and nothing written outside what the witness creates." + +data excl_manager_unaskable_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for the manager probe AND for systemd.Systemctl.ShowUserProperty, sufficient for the queried/not-queried fold to be re-checked hermetically against BOTH shell outcomes; then the fn re-enrols as an ordinary hermetic discovery row, drops off local_repo_wet_schedule and off floor_route_gap, and this row deletes. A mock for the probe ALONE does not discharge it: the subject is what the property reader does when the manager cannot be spawned, so a run that reaches ShowUserProperty through a fixture and never exercises the refusal arm re-checks the assertion against authored data rather than against the boundary.") + data excl_shell_spawn_refused_dissolve: DissolutionCondition = unbound_dissolution(description: "the spawn boundary of the shell transport becomes executable under the execution-corpus scope prefix as ExecutionWitnessKind rows in gunbc.commit_workflow, the same terminal excl_bin_wet_dissolve names; then this row and its four schedule rows delete together. Publishing a mock_response for ShellSpawnProbe.Observed does NOT discharge it: a mocked ShellSpawnRefused re-checks the assertions against a fixture, not against the spawn.") // bin-execution witness class re-homed to the falsifier wet cadence (CI floor endgame D6): the @@ -1031,6 +1035,16 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_tempdir_write_reason, dissolution: excl_local_repo_wet_dissolve}, + WitnessExclusionRow { + pattern: "manager_unaskable_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_manager_unaskable_reason, + dissolution: excl_manager_unaskable_dissolve}, + WitnessExclusionRow { + pattern: "attempt_lifecycle_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_local_repo_wet_tempdir_write_reason, + dissolution: excl_local_repo_wet_dissolve}, WitnessExclusionRow { pattern: "review_sheet_legacy_declaration_wet_witness_test.dag", classification: LocalRepoWetLane, diff --git a/dag/gunbc/compute/attempt_lifecycle.dag b/dag/gunbc/compute/attempt_lifecycle.dag new file mode 100644 index 00000000000..d26355f3574 --- /dev/null +++ b/dag/gunbc/compute/attempt_lifecycle.dag @@ -0,0 +1,533 @@ +module gunbc.compute.attempt_lifecycle + +import std.types { String, Bool, Int, NonEmptyStr, EpochSecs, Seconds } +import std.measure { Kibibyte, kibibyte, kibibyte_count } +import std.content_hash { content_hash_of_value } +import std.durable_compare_and_set { + CasAttempt, cas_attempt, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, + CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, + CasSlotObservation, CasObservedReadable, CasObservedUnreadable, + CasReadableSlot, CasReadableAbsent, CasReadablePresent, + CasGeneration, cas_generation_count, cas_unreadable_slot_detail, + CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, +} +import gunbc.durable_cas_file_store { + CasAttemptAdmission, CasAttemptAdmitted, CasAttemptDigestMismatch, CasAttemptDigestIncomparable, + CasAttemptKeyNotSlotAddressable, admit_cas_attempt, file_compare_and_set, DefaultAccessCreateOnly, + observe_cas_slot_state, +} +import gunbc.compute.work_request { WorkEnding, work_ending_wire, work_ending_decode } +import extdeps.languages.json.emit { JsonValue, json_object, json_kv, json_string, json_int, serialize_json } +import extdeps.languages.json.parse { + parse_json_document, JsonDocumentParsed, JsonDocumentUnreadable, json_document_gap_text, + json_object_unique_member, JsonMemberFound, JsonMemberAbsent, JsonMemberDuplicated, JsonMemberNotAnObject, + JsonString, JsonNumber, +} + +// THE ATTEMPT'S OWN RECORD, AND THE ONE PLACE ITS LIFECYCLE IS DECIDED. +// +// gunbc#11962 (PR 1) admits a reservation and releases it when the run ends. What it deliberately +// does NOT have is a way to give a seat back when that release does not land, and it declares that +// absence as gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge rather +// than shipping a recovery whose failure modes would FREE SEATS THAT SHOULD STAY HELD. This module +// is that capability, and every shape in it exists because one of those failure modes is real. +// +// WHY A CAS SLOT AND NOT A FILE, A FLAG OR A RE-LISTING. Recovery and the producer are two +// principals racing over one attempt, and the question "may this attempt still launch" has to be +// answered in the SAME step that answers "is this attempt terminal". A file the producer checks and +// then acts on is two steps with a window between them, and the window is exactly where an unbacked +// launch lives: reserve, recovery sees no unit and releases, producer spawns against memory nobody +// holds. So the state lives in a compare-and-set slot and every transition names the generation it +// expects -- the store decides the winner, and the loser is refused by precondition rather than by +// noticing afterwards. +// +// THE SLOT IS KEYED BY THE RESERVATION REFERENCE, which names ONE HOLD (identity plus the instant +// it was taken). Keying by work identity would make a retry collide with the attempt it is +// retrying -- the defect PR 1 already paid for once with its obligation files. + +// THE UNIT LIFECYCLE, AND IT IS A UNION OF TWO AXES RATHER THAN EITHER ONE OF THEM. +// +// Two lists met here and neither was the answer. PR 1's -- attempt-completed, authoritative-absence, +// populated, unavailable -- is closest to an OBSERVATION axis: what we were able to learn. +// The lifecycle brief's -- terminated-success, terminated-failure, still-running, unknown -- is an +// OUTCOME axis: what happened to the attempt. Making either the carrier and deriving the other +// loses something real (ruling, loyal-swift-608, 2026-09-21): +// +// FOLDING AUTHORITATIVE ABSENCE INTO A FAILURE ARM IS THE LOSS THAT MATTERS. "The manager has no +// record of this unit" and "the attempt failed" are different facts with different evidence, and +// only the FIRST is safe to free a seat on WITHOUT an attempt record to consult -- absence needs +// no record to be conclusive, while a failure verdict is a claim about a run whose record may not +// exist. PR 1 landed that distinction and a derivation must not quietly spend it. +// +// So the union keeps every distinction either list carries, and the count is a consequence rather +// than a target. TerminatedCauseUnknown is PR 1's authoritative absence under the name that says +// what it is: ended, and nothing here knows why. +type UnitLifecycle + = UnitTerminatedSuccess { detail: String } + | UnitTerminatedFailure { detail: String } + | UnitTerminatedCauseUnknown { detail: String } + | UnitStillRunning { detail: String } + | UnitLifecycleUnknown { detail: String } + +// THE THREE ENDED ARMS FREE CAPACITY AND THE TWO UNENDED ONES DO NOT, which is the same predicate +// PR 1 enforced -- every arm it refused on still refuses, and that is asserted ARM BY ARM rather +// than in aggregate, because a derived predicate that is merely green overall is how a refusal +// disappears in a refactor. +fn unit_lifecycle_ended(u: UnitLifecycle) -> Bool { + match u { + UnitTerminatedSuccess { detail: _ } => true + UnitTerminatedFailure { detail: _ } => true + UnitTerminatedCauseUnknown { detail: _ } => true + UnitStillRunning { detail: _ } => false + UnitLifecycleUnknown { detail: _ } => false + } +} + +fn unit_lifecycle_wire(u: UnitLifecycle) -> String { + match u { + UnitTerminatedSuccess { detail: d } => join(["terminated-success (", d, ")"], "") + UnitTerminatedFailure { detail: d } => join(["terminated-failure (", d, ")"], "") + UnitTerminatedCauseUnknown { detail: d } => join(["terminated, cause unknown (", d, ")"], "") + UnitStillRunning { detail: d } => join(["STILL RUNNING (", d, "), so the seat stays charged"], "") + UnitLifecycleUnknown { detail: d } => join(["UNKNOWN (", d, "), so the seat stays charged"], "") + } +} + +// THE LIFECYCLE STATE THE SLOT CARRIES. Reserved is the only state a launch may proceed from and +// the only state recovery may terminate from without observing the unit -- because in Reserved no +// unit exists yet, which is the whole reason the two transitions must exclude each other. +// +// THAT ENTAILMENT IS ENFORCED BY THE ROUTE AND NOT BY AGREEMENT, which is what makes the temporal +// trigger safe to act on. gunbc.compute.work_provider_local reaches compute_spawn_and_collect from +// exactly one place: the AttemptGateReady arm of compute_begin_launch. So a unit exists only if +// Reserved -> Launching was ADMITTED by the store first, and a slot still reading Reserved means +// no unit was ever spawned for that attempt. Recovery terminating a stale Reserved attempt +// therefore cannot be stopping anything, and it does not need to look to know that. If some later +// caller spawned without passing the gate, this entailment would break silently -- which is why +// the gate is one call site rather than a rule. +type AttemptState + = AttemptReserved + | AttemptLaunching + | AttemptTerminal { verdict: AttemptVerdict, detail: String } + +// WHO ENDED THE ATTEMPT AND HOW, AS A CLOSED SET. Two writers reach the terminal generation: the +// producer settling it with the work's own ending, and the recovery door terminating one it found +// dead. Anything else in that position is not a verdict this store ever wrote, so the decode below +// refuses it exactly as it refuses an unknown state word -- review 70244 found it accepting any word +// after "terminal:" while the comment above attempt_record_decode said the opposite. +type AttemptVerdict + = AttemptWorkEnded { ending: WorkEnding } + | AttemptRecovered + +fn attempt_verdict_wire(v: AttemptVerdict) -> String { + match v { + AttemptWorkEnded { ending: e } => work_ending_wire(e: e) + AttemptRecovered => "recovered" + } +} + +fn attempt_verdict_decode(word: String) -> AttemptVerdict? { + if word == attempt_verdict_wire(v: AttemptRecovered) { + Present { value: AttemptRecovered } + } else { + match work_ending_decode(word: word) { + Present { value: e } => Present { value: AttemptWorkEnded { ending: e } } + Absent => none + } + } +} + +fn attempt_state_wire(s: AttemptState) -> String { + match s { + AttemptReserved => "reserved" + AttemptLaunching => "launching" + AttemptTerminal { verdict: v, detail: _ } => join(["terminal:", attempt_verdict_wire(v: v)], "") + } +} + +// THE RECORD RECOVERY READS INSTEAD OF RECONSTRUCTING. The unit name is written here by the attempt +// that owns it; recovery never derives it from the identity, a path spelling or a directory listing. +// That is not tidiness: a derived name is a second authority for the binding, and a recovery acting +// on a name it invented can stop a unit that belongs to a different attempt. +// +// THE QUANTITIES ARE CARRIED AS WHAT THEY ARE. The grant is a Kibibyte (std.measure), not an Int +// with the unit in its field name -- gunbc.compute.work_request's note on the stripped carrier was +// written for exactly that defect, and this record held it anyway from gunbc#12040's first commit +// until review 69915 read it. The two instants are EpochSecs, the same denomination the pool's own +// lease terms and now_epoch_seconds carry, so the comparison recovery makes against the deadline is +// between two values of one type. The unit and the epoch appear as bare numbers only at the JSON +// boundary below, where the wire keeps its spelling (granted_kib) and the decode re-admits them. +type AttemptRecord { + identity: String + reference: String + unit: String + granted: Kibibyte + opened_at: EpochSecs + launch_deadline: EpochSecs + state: AttemptState +} + +fn attempt_record_json(r: AttemptRecord) -> JsonValue { + json_object(members: [ + json_kv(key: "identity", value: json_string(s: r.identity)), + json_kv(key: "reference", value: json_string(s: r.reference)), + json_kv(key: "unit", value: json_string(s: r.unit)), + json_kv(key: "granted_kib", value: json_int(n: kibibyte_count(k: r.granted))), + json_kv(key: "opened_at", value: json_int(n: r.opened_at)), + json_kv(key: "launch_deadline", value: json_int(n: r.launch_deadline)), + json_kv(key: "state", value: json_string(s: attempt_state_wire(s: r.state))), + json_kv(key: "detail", value: json_string(s: match r.state { AttemptTerminal { verdict: _, detail: d } => d AttemptReserved => "" AttemptLaunching => "" })), + ]) +} + +fn attempt_record_wire(r: AttemptRecord) -> String { + serialize_json(v: attempt_record_json(r: r)) +} + +fn attempt_record_with_state(r: AttemptRecord, state: AttemptState) -> AttemptRecord { + AttemptRecord { identity: r.identity, reference: r.reference, unit: r.unit, granted: r.granted, opened_at: r.opened_at, launch_deadline: r.launch_deadline, state: state } +} + +// ── READING THE SLOT, AND UNREADABLE IS NEVER ABSENT ────────────────────────────────────────── +// +// This is the absorbing fallback in its purest form and DESIGN 5 makes it a hard reject: a slot +// that could not be READ and a slot that holds NOTHING are opposite facts with opposite remedies, +// and collapsing them means a recovery creates state on top of one it merely failed to observe, or +// a producer launches because it could not tell it had been terminated. Every arm below is typed +// and none of them widens. +type AttemptSlotReading + = AttemptSlotAbsent + | AttemptSlotHeld { record: AttemptRecord, generation: CasGeneration } + | AttemptSlotUnreadable { detail: String } + +fn attempt_member(doc: JsonValue, key: String) -> String? { + match json_object_unique_member(v: doc, key: key) { + JsonMemberFound { value } => match value { JsonString { value: s } => Present { value: s } _ => none } + JsonMemberAbsent => none + JsonMemberDuplicated => none + JsonMemberNotAnObject => none + } +} + +fn attempt_member_int(doc: JsonValue, key: String) -> Int? { + match json_object_unique_member(v: doc, key: key) { + JsonMemberFound { value } => match value { JsonNumber { lexeme: n } => parse_int(s: n as String) _ => none } + JsonMemberAbsent => none + JsonMemberDuplicated => none + JsonMemberNotAnObject => none + } +} + +// AN INSTANT ON THE WIRE IS RE-ADMITTED, NOT CAST: a negative number is not an epoch second, and a +// record carrying one is unreadable rather than a record whose deadline is before 1970. +fn attempt_member_epoch(doc: JsonValue, key: String) -> EpochSecs? { + match attempt_member_int(doc: doc, key: key) { + Absent => none + Present { value: n } => if n < 0 { none } else { Present { value: n } } + } +} + +fn attempt_member_kibibytes(doc: JsonValue, key: String) -> Kibibyte? { + match attempt_member_int(doc: doc, key: key) { + Absent => none + Present { value: n } => if n < 0 { none } else { Present { value: kibibyte(count: n) } } + } +} + +// A RECORD THAT DOES NOT DECODE IS UNREADABLE, NOT EMPTY, for the same reason the slot is. The +// state word is reconstructed from the same spelling attempt_state_wire emits, and a word this fold +// does not know is unreadable rather than defaulted -- a future state must not read as Reserved, +// because Reserved is the one state a launch may proceed from. +fn attempt_record_decode(text: String) -> AttemptRecord? { + match parse_json_document(s: text) { + JsonDocumentUnreadable { gap: _ } => none + JsonDocumentParsed { value: doc } => + match attempt_member(doc: doc, key: "identity") { + Absent => none + Present { value: identity } => + match attempt_member(doc: doc, key: "reference") { + Absent => none + Present { value: reference } => + match attempt_member(doc: doc, key: "unit") { + Absent => none + Present { value: unit } => + match attempt_member_kibibytes(doc: doc, key: "granted_kib") { + Absent => none + Present { value: granted } => + match attempt_member_epoch(doc: doc, key: "opened_at") { + Absent => none + Present { value: opened } => + match attempt_member_epoch(doc: doc, key: "launch_deadline") { + Absent => none + Present { value: deadline } => + match attempt_member(doc: doc, key: "state") { + Absent => none + Present { value: word } => + match attempt_state_decode(word: word, detail: match attempt_member(doc: doc, key: "detail") { Present { value: d } => d Absent => "" }) { + Absent => none + Present { value: state } => + Present { value: AttemptRecord { identity: identity, reference: reference, unit: unit, granted: granted, opened_at: opened, launch_deadline: deadline, state: state } } + } + } + } + } + } + } + } + } + } +} + +fn attempt_state_decode(word: String, detail: String) -> AttemptState? { + if word == "reserved" { + Present { value: AttemptReserved } + } else if word == "launching" { + Present { value: AttemptLaunching } + } else if starts_with(s: word, prefix: "terminal:") { + match attempt_verdict_decode(word: substring(s: word, start: length("terminal:"), end: length(word))) { + Present { value: v } => Present { value: AttemptTerminal { verdict: v, detail: detail } } + Absent => none + } + } else { + none + } +} + +fn attempt_slot_read(root: NonEmptyStr, reference: NonEmptyStr) -> AttemptSlotReading { + match observe_cas_slot_state(root: root, key: reference) { + CasObservedUnreadable { cause: c } => AttemptSlotUnreadable { detail: join(["the attempt slot could not be read: ", cas_unreadable_slot_detail(cause: c)], "") } + CasObservedReadable { readable: r } => + match r { + CasReadableAbsent => AttemptSlotAbsent + CasReadablePresent { version: v } => + match attempt_record_decode(text: v.value as String) { + Absent => AttemptSlotUnreadable { detail: join(["the attempt slot at generation ", to_string(value: cas_generation_count(g: v.generation)), " holds a record this fold cannot decode"], "") } + Present { value: rec } => AttemptSlotHeld { record: rec, generation: v.generation } + } + } + } +} + +// ── THE TRANSITIONS, EACH NAMING THE GENERATION IT EXPECTS ──────────────────────────────────── +// +// THIS IS WHERE CRITERION 3 LIVES AND IT IS ONE STEP, NOT TWO. A producer that is about to spawn +// advances Reserved -> Launching expecting the generation it read; recovery that wants to end a +// reserved-but-unlaunched attempt advances Reserved -> Terminal expecting the SAME generation. +// The store admits exactly one of them. The loser gets CasPreconditionFailed and, crucially, the +// losing PRODUCER has not spawned anything yet -- the refusal arrives BEFORE the launch, not after +// it, which is the difference between a gate and a regret. +type AttemptTransition + = AttemptAdvanced { state: AttemptState, generation: CasGeneration } + | AttemptLostRace { expected: String, observed: String } + | AttemptTransitionRefused { detail: String } + +fn attempt_commit(root: NonEmptyStr, record: AttemptRecord, expected: CasExpectation) -> AttemptTransition { + let payload = attempt_record_wire(r: record) as NonEmptyStr + match admit_cas_attempt(attempt: cas_attempt( + key: record.reference as NonEmptyStr, + expected: expected, + proposed: payload, + proposed_content: content_hash_of_value(value: payload), + )) { + CasAttemptKeyNotSlotAddressable { key: k } => AttemptTransitionRefused { detail: join(["the reservation reference is not slot-addressable: ", k as String], "") } + CasAttemptDigestMismatch { claimed: _, actual: _ } => AttemptTransitionRefused { detail: "the attempt record's digest did not match its bytes" } + CasAttemptDigestIncomparable { claimed: _, actual: _ } => AttemptTransitionRefused { detail: "the attempt record's digest was incomparable" } + CasAttemptAdmitted { verified: v } => + match file_compare_and_set(root: root, publication: DefaultAccessCreateOnly, verified: v) { + CasCommitted { committed: c } => AttemptAdvanced { state: record.state, generation: c.generation } + CasPreconditionFailed { expected: e, observed: o } => + AttemptLostRace { + expected: match e { ExpectSlotGeneration { generation: g } => join(["generation ", to_string(value: cas_generation_count(g: g))], "") ExpectSlotAbsent => "an absent slot" }, + observed: match o { CasReadablePresent { version: v2 } => join(["generation ", to_string(value: cas_generation_count(g: v2.generation))], "") CasReadableAbsent => "an absent slot" }, + } + CasStoreRefused { cause: c } => + AttemptTransitionRefused { + detail: match c { + CasSlotObservationRefused { cause: u } => join(["the attempt store refused the read: ", cas_unreadable_slot_detail(cause: u)], "") + CasGenerationPublicationRefused { detail: d } => join(["the attempt store refused the write: ", d as String], "") + }, + } + } + } +} + +// THE CEILING ON A SELF-DECLARED BOUND, AND WHY A DECLARATION IS NOT ENOUGH ON ITS OWN. +// +// The launch deadline is declared by the party it protects. A producer says what it needs for +// checkout and argv assembly, and that same declaration is what stops anyone reclaiming its seat -- +// so nothing in the mechanism as described stops a producer declaring an hour. The cost of an +// over-long declaration does not land on the producer: it lands on every other contender on that +// host, as a seat nobody may reclaim. That is the EXTERNALIZATION DESIGN 5 names -- an accepted +// risk quietly re-exported to another principal while the contract keeps its name -- and it is the +// reason a self-declared bound needs a bound of its own. +// +// FIVE MINUTES, AND IT IS A POLICY BUDGET RATHER THAN A MEASUREMENT, said plainly because the +// number is authored. What the window has to cover is one `git worktree add` of this repository and +// the assembly of an argv; the srv1 receipts on gunbc#11962 show whole build attempts, checkout +// included, completing in about four minutes, so a ceiling of five minutes for the checkout ALONE +// is generous by a wide margin and still bounded. It is not derived from a measured checkout +// distribution, and when one exists this row should be re-derived from it rather than defended. +// +// A DECLARATION ABOVE THE CEILING REFUSES AND IS NOT CLAMPED. Clamping would admit the attempt +// under a bound it did not ask for and did not agree to, then let it be reclaimed mid-checkout -- +// a widen wearing a safety limit's clothes. The refusal is typed and names both numbers, so the +// author of an over-long declaration learns what the ceiling is rather than discovering it as a +// mysterious reclaim. +data compute_pre_launch_ceiling_seconds: Seconds = 300 + +// OPENING: the attempt declares itself Reserved, and it must be the FIRST writer of this reference. +// ExpectSlotAbsent is what makes a duplicated reference a refusal rather than a silent overwrite of +// somebody else's attempt. +fn attempt_open(root: NonEmptyStr, record: AttemptRecord) -> AttemptTransition { + let declared = record.launch_deadline - record.opened_at + if declared > compute_pre_launch_ceiling_seconds { + AttemptTransitionRefused { + detail: join([ + "the attempt declared a pre-launch window of ", to_string(value: declared), + " seconds and the ceiling is ", to_string(value: compute_pre_launch_ceiling_seconds), + "; a window nobody may reclaim a seat inside is a cost borne by every other contender on this host, so an over-long declaration is refused rather than clamped", + ], ""), + } + } else if declared < 0 { + AttemptTransitionRefused { + detail: join([ + "the attempt declared a launch deadline of ", to_string(value: record.launch_deadline), + " which precedes the instant it opened, ", to_string(value: record.opened_at), + "; a window that has already closed would be reclaimable the moment it is written", + ], ""), + } + } else { + attempt_commit(root: root, record: attempt_record_with_state(r: record, state: AttemptReserved), expected: ExpectSlotAbsent) + } +} + +// THE LAUNCH GATE. Called BEFORE the unit is spawned, never after. +fn attempt_begin_launch(root: NonEmptyStr, record: AttemptRecord, expected: CasGeneration) -> AttemptTransition { + attempt_commit(root: root, record: attempt_record_with_state(r: record, state: AttemptLaunching), expected: ExpectSlotGeneration { generation: expected }) +} + +// THE TERMINAL TRANSITION. Carries the verdict AND why, so the generation that records the end also +// records the reason -- history the next reader can act on rather than a bare flag. +fn attempt_terminate(root: NonEmptyStr, record: AttemptRecord, expected: CasGeneration, verdict: AttemptVerdict, detail: String) -> AttemptTransition { + attempt_commit( + root: root, + record: attempt_record_with_state(r: record, state: AttemptTerminal { verdict: verdict, detail: detail }), + expected: ExpectSlotGeneration { generation: expected }) +} + +fn attempt_transition_wire(t: AttemptTransition) -> String { + match t { + AttemptAdvanced { state: s, generation: g } => join(["advanced to ", attempt_state_wire(s: s), " at generation ", to_string(value: cas_generation_count(g: g))], "") + AttemptLostRace { expected: e, observed: o } => join(["lost the race: expected ", e, " and the slot holds ", o], "") + AttemptTransitionRefused { detail: d } => join(["refused: ", d], "") + } +} + +fn attempt_transition_advanced(t: AttemptTransition) -> Bool { + match t { + AttemptAdvanced { state: _, generation: _ } => true + AttemptLostRace { expected: _, observed: _ } => false + AttemptTransitionRefused { detail: _ } => false + } +} + +// ── WHAT MAKES RECOVERY DECIDE AN ATTEMPT IS DEAD ───────────────────────────────────────────── +// +// THE GATE ALONE IS NOT ENOUGH AND THIS IS THE GAP IT DOES NOT CLOSE. A compare-and-set decides who +// WINS a race; it says nothing about whether recovery should have entered the race at all. A +// producer that is alive and simply has not reached its launch CAS yet sits in Reserved -- exactly +// the state an impatient recovery would terminate -- and the CAS then makes that outcome look +// CORRECT rather than wrong: the producer's own CAS refuses, it releases, and the system appears to +// be working while a legitimate attempt was killed by a bystander (ruling, loyal-swift-608). +// +// THE TRIGGER THEREFORE SPLITS ON THE STATE, and the reason is structural rather than a policy +// choice: +// +// WHICH CLOCK, AND WHY THIS ONE IS SAFE HERE. The comparison is made by a process that did not +// write the deadline, so the clock is a shared authority between two principals. It is the host's +// own epoch clock (gunbc.fabric_event_log_host now_epoch_seconds), and it is the RIGHT one for two +// reasons rather than for convenience: the compute pool is host-local by construction -- PR 1 +// placed its ledger on the host precisely because a host's own memory is not a fleet fact -- so +// both principals read one clock; and the pool's own lease terms are already denominated in these +// same epoch seconds, so reaching for a second time source here would be a second time authority +// for one quantity. +// +// THE STORE OFFERS NO ORDERING TO PREFER OVER IT. The slot's generations order TRANSITIONS, not +// elapsed time, so there is nothing in the store that answers "has the window passed". +// +// BOTH STEP DIRECTIONS, NAMED, AND THE ONE THAT MATTERS IS BOUNDED BY THE GATE RATHER THAN BY THE +// CLOCK. A clock that steps FORWARD makes recovery fire late: the seat stays charged longer, which +// is the fail-closed direction and costs throughput. A clock that steps BACKWARD makes recovery +// fire early against a live pre-launch producer -- and that is the dangerous-sounding one, so it is +// worth being exact about what it actually costs. It does NOT produce an unbacked launch: the +// producer's gate CAS then expects a generation recovery has moved, so it is refused and never +// spawns. The loss is the attempt, not the invariant -- a retry, not a seat handed to two holders. +// The deadline decides who may ENTER the race; the compare-and-set decides who wins it, and only +// the second is load-bearing for safety. +// +// IN Reserved THERE IS NO UNIT TO OBSERVE, so observation is INCAPABLE of distinguishing a +// pre-launch producer from a dead one -- both present exactly the same absence. An observational +// trigger here would read "nothing there" as "dead", which is criterion 4's absorbing fallback +// with the stakes reversed. So the trigger is TEMPORAL, and the window is bounded BY THE +// ATTEMPT'S OWN DECLARATION: the producer writes launch_deadline when it opens, and recovery may +// not terminate a reserved attempt before it. The producer declares what it needs; recovery +// respects what was declared; neither guesses. +// +// IN Launching THE UNIT EXISTS, so the trigger is the five-arm observation and criterion 4 +// applies in full: only the three ENDED arms may terminate, and still-running or unknown keep the +// charge. An unreadable observation is never read as dead. +// +// WHAT BOUNDS THE PRE-LAUNCH WINDOW, stated because "bounded by construction" is worth nothing if +// nobody says by what: between opening and launching, the provider resolves a checkout and builds +// an argv. That is the whole window, it is the producer's own to declare, and a producer that +// exceeds its declared budget does not get to launch anyway -- its gate CAS expects the generation +// recovery has by then moved, so it is refused before it spawns. The deadline does not decide the +// winner; it decides who may enter. +type RecoveryTrigger + = RecoveryMayTerminate { reason: String } + | RecoveryTooEarly { deadline: EpochSecs, now: EpochSecs } + | RecoveryUnitNotEnded { lifecycle: UnitLifecycle } + | RecoveryStateNotRecoverable { state: AttemptState } + +fn recovery_trigger(record: AttemptRecord, lifecycle: UnitLifecycle, now: EpochSecs) -> RecoveryTrigger { + match record.state { + AttemptReserved => + if now < record.launch_deadline { + RecoveryTooEarly { deadline: record.launch_deadline, now: now } + } else { + RecoveryMayTerminate { + reason: join([ + "the attempt declared a launch deadline of ", to_string(value: record.launch_deadline), + " and it is now ", to_string(value: now), + ", so the window the producer asked for has passed without a launch", + ], ""), + } + } + AttemptLaunching => + if unit_lifecycle_ended(u: lifecycle) { + RecoveryMayTerminate { reason: join(["the unit is ", unit_lifecycle_wire(u: lifecycle)], "") } + } else { + RecoveryUnitNotEnded { lifecycle: lifecycle } + } + AttemptTerminal { verdict: v, detail: d } => RecoveryStateNotRecoverable { state: AttemptTerminal { verdict: v, detail: d } } + } +} + +fn recovery_trigger_fires(t: RecoveryTrigger) -> Bool { + match t { + RecoveryMayTerminate { reason: _ } => true + RecoveryTooEarly { deadline: _, now: _ } => false + RecoveryUnitNotEnded { lifecycle: _ } => false + RecoveryStateNotRecoverable { state: _ } => false + } +} + +fn recovery_trigger_wire(t: RecoveryTrigger) -> String { + match t { + RecoveryMayTerminate { reason: r } => join(["may terminate: ", r], "") + RecoveryTooEarly { deadline: d, now: n } => + join(["TOO EARLY: the attempt declared a launch deadline of ", to_string(value: d), " and it is only ", to_string(value: n), "; a producer inside its own declared window is not dead"], "") + RecoveryUnitNotEnded { lifecycle: u } => join(["the unit has not ended: ", unit_lifecycle_wire(u: u)], "") + RecoveryStateNotRecoverable { state: s } => join(["the attempt is already ", attempt_state_wire(s: s), ", so there is nothing to recover"], "") + } +} diff --git a/dag/gunbc/compute/host_capacity.dag b/dag/gunbc/compute/host_capacity.dag index a4dbfb0a8a7..9db18e2d28f 100644 --- a/dag/gunbc/compute/host_capacity.dag +++ b/dag/gunbc/compute/host_capacity.dag @@ -365,15 +365,31 @@ fn compute_seat(subject: ComputeCapacitySubject, reference: NonEmptyStr, now: Ep // // A RELEASE THAT DID NOT LAND IS NOT A RELEASE. The append is retried against a moving head and // exhaustion is its own arm; nothing here reports a return of capacity it did not observe. +// NOTHING-TO-RELEASE IS ITS OWN ARM, BECAUSE A SEAT THE POOL DOES NOT HOLD IS NOT A FAILED RELEASE. +// Three states, not two: this caller returned the seat; there was no seat to return; the ledger +// could not return it. Folding the middle into the last manufactures an incident -- outcome.json +// says the seat is STILL CHARGED and carries the stuck-reservation remedy, and an operator chases a +// seat that recovery already returned. It is the same distinction gunbc.compute.work_provider_local +// makes at compute_settle_attempt, where AttemptUnsettleable projects to HostRecordWritten +// deliberately: a loss means something was OWED and not done, and a producer that owed nothing +// cannot have lost anything. Here it was unmade, and by a CATCH-ALL rather than by a decision -- +// `other => ComputeReleaseRefused` in the fold below, which reads as exhaustive while being a +// default, so SeatNotHeld arrived at the refusal arm nobody wrote it into. +// +// THE THREE PRE-GRANT ARMS BELOW WERE ALREADY SAYING IT IN PROSE. Each rendered `nothing to +// release: ...` into a REFUSED detail, which is the right sentence in the wrong constructor: a +// reservation that was never granted has nothing to return, and every reader deciding on the arm +// rather than the text saw a failure. type ComputeRelease = ComputeReleased { partition: PartitionId, reference: NonEmptyStr, reason: NonEmptyStr } + | ComputeNothingToRelease { detail: String } | ComputeReleaseRefused { detail: String } fn compute_release(reservation: ComputeReservation, reason: NonEmptyStr) -> ComputeRelease { match reservation { - ComputeCapacityFull { wire: w } => ComputeReleaseRefused { detail: join(["nothing to release: ", w], "") } - ComputeHostBelowFloor { requested: _, available: _ } => ComputeReleaseRefused { detail: "nothing to release: the host was below its live memory floor" } - ComputeReservationRefused { detail: d } => ComputeReleaseRefused { detail: join(["nothing to release: ", d], "") } + ComputeCapacityFull { wire: w } => ComputeNothingToRelease { detail: join(["nothing to release: ", w], "") } + ComputeHostBelowFloor { requested: _, available: _ } => ComputeNothingToRelease { detail: "nothing to release: the host was below its live memory floor" } + ComputeReservationRefused { detail: d } => ComputeNothingToRelease { detail: join(["nothing to release: ", d], "") } ComputeReserved { grant: g, partition: p, amount: _, store: store } => compute_release_on(store: store, partition: p, appropriation: kibibyte(count: 0), reference: g.reference, reason: reason) } @@ -385,14 +401,19 @@ fn compute_release(reservation: ComputeReservation, reason: NonEmptyStr) -> Comp // append; it would fail at every later READ, when the fold hits UnknownEncumbrance and refuses the // WHOLE partition. // -// THE OPERATOR'S RECOVERY DOOR IS NOT HERE, and its absence is declared rather than implied. The -// discharge of a seat whose release did not land needs a termination decision bound to the unit, an -// attempt-to-unit binding that cannot release another attempt's live reservation, and a settled -// state a retry consumes -- see gunbc.recurring_failure_mode -// a_held_compute_seat_has_no_in_corpus_discharge, whose trigger names that capability. Shipping a -// recovery route with any of those missing would FREE SEATS THAT SHOULD NOT BE FREED, which is -// worse than not having one: without it every failure here keeps the charge and the host merely -// under-admits. +// THE OPERATOR'S RECOVERY DOOR IS NOT HERE, AND IT IS NO LONGER ABSENT: it is one layer up, at +// gunbc.compute.work_provider_local compute_recover_cli, and it comes back through THIS function +// rather than growing a release path of its own. What had to exist before one could ship was named +// in this annotation and by gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge +// -- a termination decision bound to the unit, an attempt-to-unit binding that cannot release +// another attempt's live reservation, and a settled state a retry consumes. All three are now +// present, and the reason the door is up there rather than here is the same reason this fold takes +// a store and a partition rather than an instance: the pool knows about encumbrances, and deciding +// that a particular attempt is dead is not a fact about a pool. +// +// WHAT HAS NOT CHANGED is why a recovery may not simply free on doubt. Shipping one with any of +// those three missing would FREE SEATS THAT SHOULD NOT BE FREED, which is worse than having none: +// every failure here keeps the charge and the host merely under-admits. // // THE APPROPRIATION PASSED HERE IS NOT LOAD-BEARING AND THE ZERO IS NOT A FABRICATED READING. product.capacity.pool // ruled that replay never adjudicates the ceiling, so a release is decided by whether the ledger @@ -426,7 +447,10 @@ fn compute_release_on( budget: compute_partition_read_budget, ) { SeatReleased { reference: r, id: _ } => ComputeReleased { partition: partition, reference: r, reason: reason } - other => ComputeReleaseRefused { detail: seat_release_wire(r: other) } + SeatNotHeld { reference: r, wire: w } => + ComputeNothingToRelease { detail: join(["the pool is not holding ", r as String, ", so there is no seat to return: ", w, ". A double release reaches here -- recovery returning a seat the producer then releases again is the ordinary case -- and it is not a ledger failure"], "") } + SeatReleaseContended { attempts: a } => ComputeReleaseRefused { detail: seat_release_wire(r: SeatReleaseContended { attempts: a }) } + SeatReleaseRefused { step: st, reason: rs } => ComputeReleaseRefused { detail: seat_release_wire(r: SeatReleaseRefused { step: st, reason: rs }) } } } } diff --git a/dag/gunbc/compute/work_provider_local.dag b/dag/gunbc/compute/work_provider_local.dag index 13ca10a3a44..9a256bd0edf 100644 --- a/dag/gunbc/compute/work_provider_local.dag +++ b/dag/gunbc/compute/work_provider_local.dag @@ -1,6 +1,6 @@ module gunbc.compute.work_provider_local -import std.types { String, Bool, Int, List, NonEmptyStr, FilePath, GitRef } +import std.types { String, Bool, Int, List, NonEmptyStr, FilePath, GitRef, EpochSecs, Seconds } import std.process { ProcessExit, ExitSuccess, ExitFailure } import std.algebra { trim } import std.measure { byte_size_count } @@ -12,12 +12,26 @@ import extdeps.git { shape_git_worktree_add_detached_argv } import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_wire_hex } import extdeps.systemd.systemd_run { systemd_run_user_wait_arguments, systemd_run_property } import extdeps.systemd.systemctl +import extdeps.transports.shell { ShellOutcome, ShellExited, ShellSpawnRefused } import extdeps.linux.cgroup_v2 { cgroup_v2_mount_point, cgroup_v2_events_path, CgroupEventsDecoding, CgroupEventsDecoded, CgroupEventsUnparseable, decode_cgroup_events_populated, } import extdeps.cache.sccache { sccache_installed_binary_path } import gunbc.clock_read { clock_now_probed_at_or_unknown } +import gunbc.fabric_event_log_host { now_epoch_seconds } +import std.durable_compare_and_set { CasGeneration, cas_generation_count } +import gunbc.compute.attempt_lifecycle { + AttemptRecord, AttemptState, AttemptReserved, AttemptLaunching, AttemptTerminal, AttemptVerdict, AttemptWorkEnded, AttemptRecovered, + UnitLifecycle, UnitTerminatedSuccess, UnitTerminatedFailure, UnitTerminatedCauseUnknown, + UnitStillRunning, UnitLifecycleUnknown, unit_lifecycle_ended, unit_lifecycle_wire, + RecoveryTrigger, RecoveryMayTerminate, RecoveryTooEarly, RecoveryUnitNotEnded, RecoveryStateNotRecoverable, + recovery_trigger, recovery_trigger_fires, recovery_trigger_wire, + AttemptTransition, AttemptAdvanced, AttemptLostRace, AttemptTransitionRefused, + AttemptSlotReading, AttemptSlotAbsent, AttemptSlotHeld, AttemptSlotUnreadable, + attempt_open, attempt_begin_launch, attempt_terminate, attempt_transition_wire, attempt_slot_read, + compute_pre_launch_ceiling_seconds, +} import gunbc.roadmap_dashboard_instance { HostDashboardInstance, dashboard_instance_for_repo_root, DashboardInstanceResolved, DashboardInstanceRootUnknown, dashboard_instance_compute_root, @@ -26,12 +40,15 @@ import gunbc.roadmap_dispatch_actuator { dispatch_capability_program } import gunbc.roadmap_execution_contract { ExecutionCapability, GitWorkspaceCapability, CargoCapability, RustcCapability, AttemptStateDirectoryCapability, } -import std.measure { Kibibyte, kibibyte_count, kibibyte_to_byte_size } +import std.measure { Kibibyte, kibibyte_to_byte_size } import gunbc.compute.host_capacity { ComputeReservation, ComputeReserved, ComputeCapacityFull, ComputeHostBelowFloor, ComputeReservationRefused, - ComputeRelease, ComputeReleased, ComputeReleaseRefused, compute_reserve, compute_release, compute_reservation_wire, + ComputeRelease, ComputeReleased, ComputeNothingToRelease, ComputeReleaseRefused, compute_reserve, compute_release, compute_reservation_wire, ComputeCapacityStanding, ComputeCapacityStandingRead, ComputeCapacityStandingUnread, compute_capacity_standing, compute_capacity_standing_wire, + ComputeCapacitySubject, ComputeSubjectResolution, ComputeSubjectResolved, ComputeSubjectHostUnresolved, + compute_capacity_subject, compute_capacity_store, compute_release_on, } +import std.measure { kibibyte } import gunbc.compute.work_request { WorkSubject, ExactTree, WorkOperation, BuildGunbcBinaries, CompileEntry, RunClaims, CargoProfile, CargoRelease, CargoDebug, WorkToolchainIdentity, work_identity, work_identity_hex, work_default_build, work_declared_outputs, @@ -40,7 +57,7 @@ import gunbc.compute.work_request { WorkInfrastructureRefusal, ProducerInFlight, HostComputeCapacityFull, HostBelowMemoryFloor, ComputeCapacityLedgerUnavailable, CheckoutUnavailable, StoreUnavailable, ToolchainUnobserved, DependencyNotSucceeded, SubjectUnresolved, - work_outcome_wire, work_outcome_ending, StoredOutcomeRead, StoredOutcomeFound, StoredOutcomeUnreadable, stored_outcome_decode, stored_outcome_is_success, + work_outcome_wire, work_outcome_ending, work_outcome_ending_of, StoredOutcomeRead, StoredOutcomeFound, StoredOutcomeUnreadable, stored_outcome_decode, stored_outcome_is_success, } // THE LOCAL PROVIDER: one of N behind the exact work contract, serving the host it runs on. It is a @@ -72,6 +89,7 @@ type ComputeLayout { log_path: String outcome_path: String consumption_path: String + attempts_dir: String } fn compute_layout(instance: HostDashboardInstance, identity_hex: String) -> ComputeLayout { @@ -89,6 +107,7 @@ fn compute_layout(instance: HostDashboardInstance, identity_hex: String) -> Comp log_path: join([work_dir, "/log"], ""), outcome_path: join([work_dir, "/outcome.json"], ""), consumption_path: join([work_dir, "/consumption"], ""), + attempts_dir: join([root, "/attempts"], ""), } } @@ -408,21 +427,31 @@ type UnitPopulation | PopulationEmpty { detail: String } | PopulationUnknown { detail: String } -fn unit_population(o: UnitObservations) -> UnitPopulation { - if !o.control_group.queried { +// IT TAKES THE TWO READINGS IT USES AND NOT THE PRODUCER'S WHOLE OBSERVATION RECORD, and that is +// a structural fact rather than tidiness. UnitObservations carries `attempt_completed` -- the +// first-hand fact that only the process which ran `systemd-run --wait` can have. If this fold took +// that record, RECOVERY WOULD HAVE TO CONSTRUCT ONE, and a caller that must supply a field it +// cannot observe supplies a fabricated value; the honest-looking `false` is still a value recovery +// invented. Narrowing the parameters means recovery has no carrier for first-hand completion +// anywhere in its route -- the distinction is unwritable rather than merely unwritten +// (ruling, loyal-swift-608, 2026-09-22: make the difference structural or the two folds can come +// to disagree about the same facts, which is the moment they become two authorities for one +// question). The kernel-outranks-systemd rule still has exactly ONE authority, and it is this one. +fn unit_population(control_group: UnitPropertyReading, events: UnitPropertyReading) -> UnitPopulation { + if !control_group.queried { PopulationUnknown { detail: "the control group could not be queried" } - } else if trim(s: o.control_group.value) == "" { + } else if trim(s: control_group.value) == "" { PopulationUnknown { detail: "the unit holds no control group, which is EITHER a unit that has finished OR a start that is still pending -- the cgroup is realized at spawn" } - } else if !o.events.queried { - PopulationUnknown { detail: join(["the cgroup events of ", trim(s: o.control_group.value), " could not be read"], "") } + } else if !events.queried { + PopulationUnknown { detail: join(["the cgroup events of ", trim(s: control_group.value), " could not be read"], "") } } else { - match decode_cgroup_events_populated(body: o.events.value) { - CgroupEventsUnparseable { cause: c } => PopulationUnknown { detail: join(["the cgroup events of ", trim(s: o.control_group.value), " could not be decoded: ", c], "") } + match decode_cgroup_events_populated(body: events.value) { + CgroupEventsUnparseable { cause: c } => PopulationUnknown { detail: join(["the cgroup events of ", trim(s: control_group.value), " could not be decoded: ", c], "") } CgroupEventsDecoded { populated: p } => if p { - PopulationOccupied { detail: join(["processes remain in ", trim(s: o.control_group.value)], "") } + PopulationOccupied { detail: join(["processes remain in ", trim(s: control_group.value)], "") } } else { - PopulationEmpty { detail: join([trim(s: o.control_group.value), " reports populated 0"], "") } + PopulationEmpty { detail: join([trim(s: control_group.value), " reports populated 0"], "") } } } } @@ -440,7 +469,7 @@ fn unit_population(o: UnitObservations) -> UnitPopulation { // reading serves only to CONFIRM a completion or to REFUSE one. Establishing termination without a // completed attempt is the lifecycle capability's job, not this one's. fn unit_termination_decide(o: UnitObservations) -> UnitTermination { - let population = unit_population(o: o) + let population = unit_population(control_group: o.control_group, events: o.events) match population { PopulationOccupied { detail: d } => UnitPopulated { detail: d } _ => @@ -475,6 +504,129 @@ fn unit_termination_decide(o: UnitObservations) -> UnitTermination { } } +// ── THE LIFECYCLE VERDICT, WHICH IS WHAT RECOVERY ASKS AND SETTLEMENT DOES NOT ──────────────── +// +// THE TWO FOLDS ARE NOT A FORK AND THE DIFFERENCE IS WHAT EACH ONE IS ENTITLED TO ASSUME. +// unit_termination_decide answers for a producer that JUST RAN `systemd-run --wait` and therefore +// holds a fact nobody else has -- whether its own attempt completed -- and it is deliberately +// conservative because its wrong answer frees a live seat. This fold answers for RECOVERY, which +// holds no such fact and must decide from the manager alone. Merging them would mean giving one of +// the two callers evidence it does not have: either recovery inherits a completion it never +// observed, or the producer throws away the one reading that makes its release safe. +// +// WHAT THEY DO SHARE IS THE POPULATION READING, and it is shared rather than restated -- +// unit_population is called by both, so the kernel-outranks-systemd rule has ONE authority. +type UnitLifecycleObservations { + load_state: UnitPropertyReading + active_state: UnitPropertyReading + result: UnitPropertyReading + population: UnitPopulation +} + +data unit_active_state_property: NonEmptyStr = "ActiveState" as NonEmptyStr +data unit_result_property: NonEmptyStr = "Result" as NonEmptyStr +data unit_active_state_failed_wire: String = "failed" +data unit_active_state_inactive_wire: String = "inactive" +data unit_result_success_wire: String = "success" + +// FOUR STATES AND UNKNOWN IS AN ARM RATHER THAN A DEFAULT (criterion 1). Every path that cannot +// establish an end answers UnitLifecycleUnknown CARRYING WHY, and the seat stays charged on it -- +// "I could not tell" is a reading recovery must act on by NOT acting, never a gap a caller fills. +// +// THE ORDER IS THE SAFETY PROPERTY AND IT IS PR 1'S ORDER. A positively occupied cgroup refuses +// first and no manager property overrides it: the kernel saying processes are there outranks +// systemd's bookkeeping about what it thinks it ran. +// +// LoadState=not-found IS AN ENDING AND ITS CAUSE IS GONE WITH IT. These are transient --collect +// units, so one that ran and finished is REMOVED and the manager truthfully has no record. Calling +// that success would be fabrication and calling it failure would be pessimism, so it is the third +// ended arm -- which is exactly PR 1's authoritative absence under the name that says what it is. +fn unit_lifecycle_decide(o: UnitLifecycleObservations) -> UnitLifecycle { + match o.population { + PopulationOccupied { detail: d } => UnitStillRunning { detail: d } + _ => + if !o.load_state.queried { + UnitLifecycleUnknown { detail: "the user manager could not be queried for this unit's load state" } + } else if trim(s: o.load_state.value) == unit_load_state_absent_wire { + UnitTerminatedCauseUnknown { detail: join(["LoadState=", unit_load_state_absent_wire, ", so the manager has no record of this unit: a transient --collect unit that ran has been removed, and its cause went with it"], "") } + } else if !o.active_state.queried { + UnitLifecycleUnknown { detail: "the unit is known to the manager but its active state could not be read" } + } else if trim(s: o.active_state.value) == unit_active_state_failed_wire { + UnitTerminatedFailure { detail: join(["ActiveState=failed, Result=", if o.result.queried { trim(s: o.result.value) } else { "" }], "") } + } else if trim(s: o.active_state.value) != unit_active_state_inactive_wire { + UnitStillRunning { detail: join(["ActiveState=", trim(s: o.active_state.value)], "") } + } else if !o.result.queried { + UnitLifecycleUnknown { detail: "the unit is inactive but its Result could not be read, so whether it ended well is not established" } + } else if trim(s: o.result.value) == "" { + UnitLifecycleUnknown { detail: "the unit is inactive and the manager answered its Result with nothing, which is not a verdict" } + } else if trim(s: o.result.value) == unit_result_success_wire { + UnitTerminatedSuccess { detail: join(["ActiveState=", unit_active_state_inactive_wire, ", Result=", unit_result_success_wire], "") } + } else { + UnitTerminatedFailure { detail: join(["ActiveState=", unit_active_state_inactive_wire, ", Result=", trim(s: o.result.value)], "") } + } + } +} + +// THE UNIT NAME COMES FROM THE ATTEMPT RECORD (criterion 2). This fold takes the name it is given +// and never rebuilds it from an identity, a path spelling or a listing: a recovery acting on a name +// it invented can stop a unit belonging to a different attempt, and the record is the only +// authority for that binding. +fn observe_unit_lifecycle(unit: NonEmptyStr) -> UnitLifecycle { + let cg = read_user_unit_property(unit: unit, property: unit_control_group_property) + unit_lifecycle_decide(o: UnitLifecycleObservations { + load_state: read_user_unit_property(unit: unit, property: unit_load_state_property), + active_state: read_user_unit_property(unit: unit, property: unit_active_state_property), + result: read_user_unit_property(unit: unit, property: unit_result_property), + population: unit_population(control_group: cg, events: read_cgroup_events(control_group: cg)), + }) +} + +// ONE READER FOR A USER-UNIT PROPERTY, AND IT FOLDS THE TRANSPORT'S ANSWER BEFORE THE PROGRAM'S. +// systemctl answering nonzero and systemctl NOT RUNNING are different facts with different +// remedies (extdeps.transports.shell ShellOutcome): the first is the manager refusing a question, +// the second is a host with no manager to ask. Before this reader the second ended the whole +// evaluation as a shell-spawn-refused runtime error -- the settlement or recovery died mid-route, +// leaving the seat charged AND the producer lease held with no record saying why, which is the +// wedged state the recovery door exists to undo, manufactured by the driver itself. The fold's +// unavailable arm was never reached because the refusal pre-empted it. Now a spawn refusal is a +// property that was NOT QUERIED, and the fold decides exactly as it does for a manager that could +// not be read: the charge is kept and the outcome says the manager could not be asked. No caller +// branched on the difference before, because no field carried it; the difference is that the +// route now reaches its own unavailable arm instead of a diagnostic about a program. +fn read_user_unit_property(unit: NonEmptyStr, property: NonEmptyStr) -> UnitPropertyReading { + let read = systemd.Systemctl.ShowUserProperty(unit: unit, property: property) + unit_property_from_shell(outcome: read.outcome, success: read.success, value: read.value) +} + +// THE DECISION IS SEPARATED FROM THE EFFECT SO A CONTROL CAN REACH IT (review 69970). Fused to the +// ShowUserProperty call, this mapping was only observable on a host with NO systemd user manager, +// and the one lane the witness runs on HAS one -- so the claim over it was `if present { true }`, +// permanently green on the only route that executes it, which DESIGN 4b names as worse than absent +// because it will be cited as coverage. As a fold over a supplied ShellOutcome it is a claim at ONE +// INTERFACE with both arms authorable anywhere, and the wet witness keeps the inhabitance half: +// that the real producer on a host WITH a manager emits ShellExited and reaches a queried reading. +// +// A REFUSED SPAWN IS NOT A FALSE ANSWER, which is the whole content of the fold. systemctl +// answering nonzero means the manager refused the question; systemctl not running means there was +// no manager to ask. Only the first is a reading, so the second is queried: false and carries no +// value -- and the decide folds downstream already route a not-queried property to their own +// unavailable arm, keeping the charge and saying the manager could not be asked. +fn unit_property_from_shell(outcome: ShellOutcome, success: Bool, value: String) -> UnitPropertyReading { + match outcome { + ShellSpawnRefused { program: _, cause: _ } => UnitPropertyReading { queried: false, value: "" } + ShellExited => UnitPropertyReading { queried: success, value: value } + } +} + +fn read_cgroup_events(control_group: UnitPropertyReading) -> UnitPropertyReading { + let events = if control_group.queried && trim(s: control_group.value) != "" { + linux.CgroupV2.ReadEvents(events_path: cgroup_v2_events_path(cgroup_path: join([cgroup_v2_mount_point as String, trim(s: control_group.value)], "") as NonEmptyStr)) + } else { + linux.CgroupV2.ReadEvents(events_path: cgroup_v2_events_path(cgroup_path: cgroup_v2_mount_point)) + } + UnitPropertyReading { queried: events.success, value: events.value } +} + // THE USER MANAGER IS ASKED, NOT THE SYSTEM ONE. systemctl_show_load_state_argv exists and is // system-scope; these are transient --user units, so asking the system manager would answer // not-found for EVERY one of them -- a fabricated authoritative absence, the worst answer this fold @@ -485,18 +637,12 @@ fn unit_termination_decide(o: UnitObservations) -> UnitTermination { // property become a conclusion in the first place. fn observe_unit_termination(identity_hex: String, attempt_completed: Bool) -> UnitTermination { let unit = compute_unit_name(identity_hex: identity_hex) - let load = systemd.Systemctl.ShowUserProperty(unit: unit, property: unit_load_state_property) - let cg = systemd.Systemctl.ShowUserProperty(unit: unit, property: unit_control_group_property) - let events = if cg.success && trim(s: cg.value) != "" { - linux.CgroupV2.ReadEvents(events_path: cgroup_v2_events_path(cgroup_path: join([cgroup_v2_mount_point as String, trim(s: cg.value)], "") as NonEmptyStr)) - } else { - linux.CgroupV2.ReadEvents(events_path: cgroup_v2_events_path(cgroup_path: cgroup_v2_mount_point)) - } + let cg = read_user_unit_property(unit: unit, property: unit_control_group_property) unit_termination_decide(o: UnitObservations { attempt_completed: attempt_completed, - load_state: UnitPropertyReading { queried: load.success, value: load.value }, - control_group: UnitPropertyReading { queried: cg.success, value: cg.value }, - events: UnitPropertyReading { queried: events.success, value: events.value }, + load_state: read_user_unit_property(unit: unit, property: unit_load_state_property), + control_group: cg, + events: read_cgroup_events(control_group: cg), }) } @@ -596,10 +742,182 @@ fn compute_attempt_completed(outcome: WorkOutcome) -> Bool { WorkOutputMismatch { identity: _, detail: _ } => true WorkFailed { identity: _, exit_code: _, log_path: _ } => false WorkRefusedByInfrastructure { identity: _, cause: _ } => false - WorkCancelled { identity: _ } => false + WorkCancelled { identity: _, detail: _ } => false + } +} + +// ── THE ATTEMPT GATE ON THE REAL PROVIDER ROUTE ────────────────────────────────────────────── +// +// THIS IS WHERE CRITERION 3 STOPS BEING A CARRIER PROPERTY AND BECOMES A PROPERTY OF THIS +// PROVIDER. gunbc.compute.attempt_lifecycle can refuse a launch that lost its generation, but a +// refusal nothing calls stops nothing: until the producer asks the gate in the real order -- +// reserve, open, ASK, spawn -- the module is a wall beside the door rather than in it. So the +// spawn is downstream of the gate's answer by construction, and every failure arm below returns +// WITHOUT reaching compute_run_unit. +// +// AND THE ASK SITS AFTER THE CHECKOUT, NOT BEFORE IT, because the window the launch deadline +// protects IS the checkout. Placing the ask before it made the two steps adjacent -- the gate +// would have been asked microseconds after the open, so the interleaving it exists to refuse could +// not occur on the real route and the wall would have been a decoration in the DESIGN 4b sense +// (ask whether the RED is authorable). Reserve, open, check out, ASK, spawn: the ask is the last +// thing that happens before a unit exists. +// +// THE CLOCK IS AN INPUT AND AN UNREADABLE ONE REFUSES. Both bounds the attempt declares -- when it +// opened and when its pre-launch window closes -- are instants, and a fabricated instant is worse +// than no attempt: a zero opened_at makes the window look long expired, so recovery would reclaim +// the seat out from under a producer that is running normally. There is no honest default, so the +// arm refuses and releases (DESIGN 5: a failure arm refuses, never widens). +type LeasedRun { + outcome: WorkOutcome + gate: AttemptGate +} + +type AttemptGate + = AttemptGateReady { record: AttemptRecord, generation: CasGeneration } + | AttemptGateRefused { detail: String } + +// THE WINDOW THE PRODUCER DECLARES, AND IT IS AT THE CEILING RATHER THAN UNDER IT BY ACCIDENT. +// What it has to cover is one `git worktree add` of this repository plus argv assembly, and the +// ceiling in attempt_lifecycle is the authority on what is tolerable to the other contenders on +// this host. Naming the ceiling's own row rather than restating 300 keeps one number: a change +// there moves this declaration with it instead of silently leaving the producer at a stale bound. +data compute_launch_window_seconds: Seconds = compute_pre_launch_ceiling_seconds + +// THE UNIT NAME IS WRITTEN INTO THE RECORD BY THE ATTEMPT THAT OWNS IT, from the same fold the +// invocation uses. That is the binding criterion 2 is about: recovery reads this field rather than +// rebuilding the name from the identity, so a recovery can never act on a unit it named itself. +fn compute_attempt_record(identity: String, reference: NonEmptyStr, granted: Kibibyte, now: EpochSecs) -> AttemptRecord { + AttemptRecord { + identity: identity, + reference: reference as String, + unit: compute_unit_name(identity_hex: identity) as String, + granted: granted, + opened_at: now, + launch_deadline: now + compute_launch_window_seconds, + state: AttemptReserved, } } +fn compute_gate_from_transition(t: AttemptTransition, record: AttemptRecord, what: String) -> AttemptGate { + match t { + AttemptAdvanced { state: _, generation: g } => AttemptGateReady { record: record, generation: g } + AttemptLostRace { expected: e, observed: o } => + AttemptGateRefused { detail: join([what, " did not happen: the attempt slot expected ", e, " and holds ", o, ", so this attempt is no longer the one entitled to the seat"], "") } + AttemptTransitionRefused { detail: d } => AttemptGateRefused { detail: join([what, " was refused: ", d], "") } + } +} + +fn compute_open_attempt(layout: ComputeLayout, identity: String, reference: NonEmptyStr, granted: Kibibyte) -> AttemptGate { + match now_epoch_seconds() { + Absent => AttemptGateRefused { detail: "the host clock could not be read as epoch seconds, and an attempt's opened_at and launch deadline are both instants -- a fabricated one would make this attempt look expired to recovery the moment it is written" } + Present { value: now } => { + let record = compute_attempt_record(identity: identity, reference: reference, granted: granted, now: now) + compute_gate_from_transition(t: attempt_open(root: layout.attempts_dir as NonEmptyStr, record: record), record: record, what: "opening the attempt") + } + } +} + +// THE ASK, IMMEDIATELY BEFORE THE SPAWN. Reserved -> Launching against the generation the open +// returned. A terminal transition that got there first moved the generation, so this is refused by +// the STORE -- one linearized step -- and the producer learns it here rather than discovering it +// after a unit is already consuming memory nobody holds. +fn compute_begin_launch(layout: ComputeLayout, gate: AttemptGate) -> AttemptGate { + match gate { + AttemptGateRefused { detail: d } => AttemptGateRefused { detail: d } + AttemptGateReady { record: rec, generation: g } => + compute_gate_from_transition(t: attempt_begin_launch(root: layout.attempts_dir as NonEmptyStr, record: rec, expected: g), record: rec, what: "the launch") + } +} + +// SETTLEMENT CLOSES THE SLOT, AND A FAILURE TO CLOSE IT IS A HOST-RECORD LOSS RATHER THAN SILENCE. +// The terminal generation carries the verdict and why (criterion 6: the obligation is settled and +// the history is kept), and if the transition does not land the attempt is still open in the store +// -- which is a fact an operator needs, so it rides out on the same carrier as every other +// recording failure this provider can suffer. +// SETTLEMENT IS A THREE-VALUED FACT AND IT GETS A THREE-ARMED CARRIER. Review 69967 found the third +// value forced onto HostRecordStatus, which has two arms, so "this producer never held the slot" +// landed in the arm that means "recorded". The consumption receipt then read `attempt: settled in +// the attempt slot` on a LOST LAUNCH RACE -- a reachable path, and the inverse of the argument the +// settlement line exists for: a line that says nothing on the good path cannot be read as evidence, +// and a line that says the good path happened where it did not is worse. +// +// WHY A NEW TYPE RATHER THAN A THIRD ARM ON HostRecordStatus, which was the other constructive +// option. HostRecordStatus answers ONE question -- did this host record its own side facts, or is +// there a loss an operator must hear about -- for five producers (the release, the lease drop, the +// measurement write, the joins over all of them). `nothing was owed here` is not an answer to that +// question for any of the others, so the arm would be uninhabitable everywhere but this call and +// would owe `host_record_join` and `host_record_was_written` a rule with no meaning to carry. The +// three-valued fact belongs to SETTLEMENT, so it gets settlement's own type, and the projection into +// the shared carrier below is total and says exactly why each arm maps where it does. +type AttemptSettlement + = AttemptSettled + | AttemptNotSettled { detail: String } + | AttemptUnsettleable { detail: String } + +fn compute_settle_attempt(layout: ComputeLayout, gate: AttemptGate, verdict: AttemptVerdict, detail: String) -> AttemptSettlement { + match gate { + AttemptGateRefused { detail: d } => AttemptUnsettleable { detail: d } + AttemptGateReady { record: rec, generation: g } => + match attempt_terminate(root: layout.attempts_dir as NonEmptyStr, record: rec, expected: g, verdict: verdict, detail: detail) { + AttemptAdvanced { state: _, generation: _ } => AttemptSettled + AttemptLostRace { expected: e, observed: o } => + AttemptNotSettled { detail: join(["the attempt slot for ", rec.reference, " could not be closed: expected ", e, " and it holds ", o, "; the attempt stays open in the store and the seat's settlement is recorded only here"], "") } + AttemptTransitionRefused { detail: d } => + AttemptNotSettled { detail: join(["the attempt slot for ", rec.reference, " could not be closed: ", d, "; the attempt stays open in the store"], "") } + } + } +} + +// THE PROJECTION INTO THE HOST-RECORD CARRIER, AND UNSETTLEABLE IS DELIBERATELY NOT A LOSS. A loss +// means this host owed a record and failed to write it, which is an operator action. A producer +// whose gate was refused owed nothing: it never held the slot, so there is no missing record and +// nothing for an operator to chase. Mapping it to HostRecordLost would manufacture an incident, which +// is the same fabrication as the success arm did, pointed the other way. +fn attempt_settlement_host_record(s: AttemptSettlement) -> HostRecordStatus { + match s { + AttemptSettled => HostRecordWritten + AttemptNotSettled { detail: d } => HostRecordLost { detail: d } + AttemptUnsettleable { detail: _ } => HostRecordWritten + } +} + +// THE SETTLEMENT LINE HAS ITS OWN WORDS BECAUSE host_record_wire RENDERS SUCCESS AS THE EMPTY +// STRING -- it is built to be APPENDED to a sentence, so reusing it here produced a receipt line +// reading "attempt: " with nothing after it. A line that says nothing on the good path cannot be +// read as evidence that the good path happened, which is the whole reason the line is in the +// receipt. Found in the first srv1 run at this head. +fn compute_attempt_settlement_wire(closed: AttemptSettlement) -> String { + match closed { + AttemptSettled => "settled in the attempt slot" + AttemptNotSettled { detail: d } => join(["NOT SETTLED -- ", d], "") + AttemptUnsettleable { detail: d } => join(["NOT SETTLED BY THIS PRODUCER -- it never held the attempt slot: ", d, ". Whatever the slot holds was written by whoever did hold it, and this run observed none of it"], "") + } +} + +// A GATE REFUSAL RELEASES THE SEAT IT NEVER USED. Nothing was spawned, so the reservation is +// returned unconditionally rather than through the unit-termination fold -- there is no unit to +// observe, and routing an unspawned attempt through a termination decision would make the release +// depend on evidence that cannot exist. +fn compute_refused_before_launch( + identity: String, + subject: WorkSubject, + op: WorkOperation, + layout: ComputeLayout, + reservation: ComputeReservation, + detail: String, +) -> ProvideResult { + let returned = compute_release(reservation: reservation, reason: join(["the attempt never launched: ", detail], "") as NonEmptyStr) + let dropped = compute_drop_producer_lease(layout: layout) + let fresh = compute_fresh( + outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: join([detail, "; ", compute_release_wire(r: returned)], "") } }, + subject: subject, op: op) + provide_result_with_host_record( + r: fresh, + carried: host_record_join( + a: compute_lease_drop_record(dropped: dropped, layout: layout), + b: if compute_release_landed(r: returned) { HostRecordWritten } else { HostRecordLost { detail: join(["the seat for this unlaunched attempt was NOT returned: ", compute_release_wire(r: returned)], "") } })) +} + fn compute_run_and_settle( instance: HostDashboardInstance, commit: String, @@ -612,7 +930,33 @@ fn compute_run_and_settle( reference: NonEmptyStr, reservation: ComputeReservation, ) -> ProvideResult { - let outcome = compute_run_leased(instance: instance, commit: commit, layout: layout, identity: identity, op: op, dependency_store: dependency_store, granted: granted) + match compute_open_attempt(layout: layout, identity: identity, reference: reference, granted: granted) { + AttemptGateRefused { detail: d } => + compute_refused_before_launch(identity: identity, subject: subject, op: op, layout: layout, reservation: reservation, detail: d) + AttemptGateReady { record: rec, generation: g } => + compute_run_under_grant( + instance: instance, commit: commit, layout: layout, identity: identity, subject: subject, op: op, + dependency_store: dependency_store, granted: granted, reference: reference, reservation: reservation, + opened: AttemptGateReady { record: rec, generation: g }) + } +} + +fn compute_run_under_grant( + instance: HostDashboardInstance, + commit: String, + layout: ComputeLayout, + identity: String, + subject: WorkSubject, + op: WorkOperation, + dependency_store: String, + granted: Kibibyte, + reference: NonEmptyStr, + reservation: ComputeReservation, + opened: AttemptGate, +) -> ProvideResult { + let run = compute_run_leased(instance: instance, commit: commit, layout: layout, identity: identity, op: op, dependency_store: dependency_store, granted: granted, opened: opened) + let outcome = run.outcome + let launched = run.gate let standing = compute_capacity_standing(instance: instance) let termination = observe_unit_termination(identity_hex: identity, attempt_completed: compute_attempt_completed(outcome: outcome)) let returned = if unit_termination_frees_capacity(t: termination) { @@ -627,22 +971,27 @@ fn compute_run_and_settle( layout: layout, identity: identity, subject: subject, op: op, outcome: outcome, reservation: reservation, returned: returned, reference: reference, termination: termination) } - let dropped = Filesystem.Delete(path: layout.lease_path) + let closed = compute_settle_attempt( + layout: layout, gate: launched, + verdict: AttemptWorkEnded { ending: work_outcome_ending_of(o: outcome) }, + detail: join([unit_termination_wire(t: termination), "; ", compute_release_wire(r: returned)], "")) + let dropped = compute_drop_producer_lease(layout: layout) let measured = Filesystem.Write( path: layout.consumption_path, content: join([ compute_capacity_standing_wire(s: standing), "\n", "unit: ", unit_termination_wire(t: termination), "\n", "reservation: ", compute_release_wire(r: returned), "\n", - if dropped.success { "" } else { compute_stale_lease_note(layout: layout, error: dropped.error) }, + "attempt: ", compute_attempt_settlement_wire(closed: closed), "\n", + match dropped { LeaseDropped => "" LeaseNotDropped { detail: d } => compute_stale_lease_note(layout: layout, error: d) }, ], "")) - if measured.success { - settled - } else { - compute_with_lost_host_record( - settled: settled, layout: layout, - dropped_ok: dropped.success, dropped_error: dropped.error, error: measured.error) - } + provide_result_with_host_record( + r: if measured.success { + settled + } else { + compute_with_lost_host_record(settled: settled, layout: layout, dropped: dropped, error: measured.error) + }, + carried: attempt_settlement_host_record(s: closed)) } // THE HOST RECORD IS THE ONLY DURABLE CARRIER OF THREE FACTS, so losing it is reported rather than @@ -672,17 +1021,15 @@ fn compute_run_and_settle( fn compute_with_lost_host_record( settled: ProvideResult, layout: ComputeLayout, - dropped_ok: Bool, - dropped_error: String, + dropped: LeaseDrop, error: String, ) -> ProvideResult { let detail = join([ "this host's record at ", layout.consumption_path, " could not be written: ", error, "; the consumption reading is lost, and ", - if dropped_ok { - "the producer lease was dropped, so nothing else is outstanding" - } else { - join(["THE PRODUCER LEASE AT ", layout.lease_path, " IS ALSO STILL HELD (", dropped_error, ") AND NOTHING NOW RECORDS THAT IT IS STALE: an operator must remove the name before this identity can be produced again"], "") + match dropped { + LeaseDropped => "the producer lease was dropped, so nothing else is outstanding" + LeaseNotDropped { detail: d } => join(["THE PRODUCER LEASE AT ", layout.lease_path, " IS ALSO STILL HELD (", d, ") AND NOTHING NOW RECORDS THAT IT IS STALE: an operator must remove the name before this identity can be produced again"], "") }, ], "") provide_result_with_host_record(r: settled, carried: HostRecordLost { detail: detail }) @@ -778,9 +1125,9 @@ fn compute_unreleased_record( // WHAT KEEPS IT FAIL-CLOSED MEANWHILE: every arm that cannot prove the unit is gone keeps the // charge, so the host UNDER-admits. Nothing is over-promised; the pool simply shrinks until an // operator clears the partition by hand. That is the direction a capacity ledger must fail in. -data compute_stuck_reservation_remedy: String = "There is NO safe discharge for this seat while this host is admitting work: clearing the capacity partition by hand under live admission removes the record the admission arithmetic is computed from, so the next requests would be admitted against memory this one still holds -- trading a host that under-admits for one that over-promises. The discharge is the compute lifecycle capability (gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge). Any manual intervention before then requires compute admission STOPPED on this host and every gunbc-compute unit PROVEN gone, in that order. Until then this host under-admits, which is the fail-closed direction and is not an incident." +data compute_stuck_reservation_remedy: String = "THE REMEDY IS compute_recover_cli, run with this reservation reference: it reads the attempt slot, observes the unit through the manager and its cgroup, and releases the seat ONLY if the unit has ended -- refusing, and saying why, if it has not. What is still NOT safe is clearing the capacity partition by hand under live admission: that removes the record the admission arithmetic is computed from, so the next requests would be admitted against memory this one still holds, trading a host that under-admits for one that over-promises. If the door declines, the seat is meant to stay charged; a manual intervention over its refusal requires compute admission STOPPED on this host and every gunbc-compute unit PROVEN gone, in that order. Until the door is run this host under-admits, which is the fail-closed direction and is not an incident." -// THE ORDER THE TWO HOLDS ARE TAKEN IN// THE ORDER THE TWO HOLDS ARE TAKEN IN, and they are two facts rather than one. The producer lease +// THE ORDER THE TWO HOLDS ARE TAKEN IN, and they are two facts rather than one. The producer lease // excludes a SECOND PRODUCER OF THIS IDENTITY and is a NAME, so an exclusive create settles it; the // reservation is a QUANTITY on the host, and no exclusive create of any name settles that. The // lease is taken first because a request that then loses on capacity releases a name it holds @@ -803,6 +1150,63 @@ data compute_stuck_reservation_remedy: String = "There is NO safe discharge for // attached to MODULE-SCOPE declarations only, and the interpreter route this provider's witnesses // run on tolerates a body-position block that `gunbc compile` refuses outright -- 14 blocking // errors on a module every witness had reported green. +// THE ATTACH CHECK IS MADE TWICE, AND THE SECOND ONE IS THE LOAD-BEARING ONE. +// +// The first read happens BEFORE the producer lease exists, which makes it evidence about a past +// world: between reading "no stored outcome" and winning the lease, another producer can finish and +// publish one. The first caller then re-produces work that is already done AND takes a second +// reservation for an identity that is already satisfied -- the dedup the contract promises, lost to +// a window nobody was holding anything across. +// +// So whatever was observed before the lease is re-observed while holding it. The early read is kept +// because it lets the overwhelmingly common case -- an identity that is already built -- answer +// without touching the lease at all; it is an optimisation, and the one inside the lease is the +// decision. +fn compute_read_stored_outcome(layout: ComputeLayout) -> StoredOutcomeRead { + let stored = Filesystem.Read(path: layout.outcome_path) + if stored.success { stored_outcome_decode(text: stored.content) } else { StoredOutcomeUnreadable { reason: "no stored outcome" } } +} + +// ATTACHING FROM INSIDE THE LEASE MEANS GIVING THE LEASE BACK, and a failure to do so is reported +// through the one lease-drop authority rather than a second spelling of it. +fn compute_attach_under_lease(layout: ComputeLayout, identity: String, subject: WorkSubject, op: WorkOperation) -> ProvideResult { + let attached = compute_read_stored_outcome(layout: layout) + let dropped = compute_drop_producer_lease(layout: layout) + match attached { + StoredOutcomeFound { ending, identity: stored_identity, document } => + ProvideAttached { identity: stored_identity, ending: ending, document: document, host_record: compute_lease_drop_record(dropped: dropped, layout: layout) } + StoredOutcomeUnreadable { reason } => + compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: reason } }, subject: subject, op: op) + } +} + +// ONE AUTHORITY FOR "THE PRODUCER LEASE WAS NOT DROPPED", because there were three. +// +// compute_refused_unreserved mapped a failed drop to StoreUnavailable; compute_run_and_settle +// folded it into the consumption note; and the attach path above would have needed a third. Three +// places deciding one fact is the DESIGN 3 fork, and the thing to delete rather than to keep +// consistent by hand -- they were already inconsistent, since one turned the failure into a verdict +// about the work and another did not. +// +// THE CONTRACT, stated once and applied everywhere: a lease that could not be dropped NEVER changes +// what the work did. It is a host-operational fact, it rides as a HostRecordLost so the caller hears +// it without the stored record being contradicted, and the remedy is an operator removing the name. +type LeaseDrop + = LeaseDropped + | LeaseNotDropped { detail: String } + +fn compute_drop_producer_lease(layout: ComputeLayout) -> LeaseDrop { + let dropped = Filesystem.Delete(path: layout.lease_path) + if dropped.success { LeaseDropped } else { LeaseNotDropped { detail: dropped.error } } +} + +fn compute_lease_drop_record(dropped: LeaseDrop, layout: ComputeLayout) -> HostRecordStatus { + match dropped { + LeaseDropped => HostRecordWritten + LeaseNotDropped { detail: d } => HostRecordLost { detail: compute_stale_lease_note(layout: layout, error: d) } + } +} + fn compute_provide_leaf( instance: HostDashboardInstance, commit: String, @@ -813,19 +1217,20 @@ fn compute_provide_leaf( ) -> ProvideResult { let identity = work_identity_hex(id: work_identity(subject: subject, op: op, toolchain: toolchain)) let layout = compute_layout(instance: instance, identity_hex: identity) - let stored = Filesystem.Read(path: layout.outcome_path) - let attached = if stored.success { stored_outcome_decode(text: stored.content) } else { StoredOutcomeUnreadable { reason: "no stored outcome" } } + let attached = compute_read_stored_outcome(layout: layout) if stored_outcome_is_success(r: attached) { match attached { StoredOutcomeFound { ending, identity: stored_identity, document } => ProvideAttached { identity: stored_identity, ending: ending, document: document, host_record: HostRecordWritten } StoredOutcomeUnreadable { reason } => compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: reason } }, subject: subject, op: op) } - } else if !(compute_ensure_dir(instance: instance, path: layout.work_dir) && compute_ensure_dir(instance: instance, path: layout.leases_dir) && compute_ensure_dir(instance: instance, path: layout.store_dir) && compute_ensure_dir(instance: instance, path: layout.target_dir)) { + } else if !(compute_ensure_dir(instance: instance, path: layout.work_dir) && compute_ensure_dir(instance: instance, path: layout.leases_dir) && compute_ensure_dir(instance: instance, path: layout.store_dir) && compute_ensure_dir(instance: instance, path: layout.target_dir) && compute_ensure_dir(instance: instance, path: layout.attempts_dir)) { compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: join(["could not create the compute directories under ", layout.root], "") } }, subject: subject, op: op) } else { let lease = Filesystem.WriteCreateNew(path: layout.lease_path, content: join([commit, " ", clock_now_probed_at_or_unknown() as String, "\n"], "")) if !lease.success { compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: ProducerInFlight { lease_path: layout.lease_path } }, subject: subject, op: op) + } else if stored_outcome_is_success(r: compute_read_stored_outcome(layout: layout)) { + compute_attach_under_lease(layout: layout, identity: identity, subject: subject, op: op) } else { let reference = compute_reservation_reference(identity: identity) let reservation = compute_reserve(instance: instance, reference: reference, term_seconds: compute_reservation_term_seconds) @@ -876,22 +1281,22 @@ fn compute_refused_unreserved( layout: ComputeLayout, cause: WorkInfrastructureRefusal, ) -> ProvideResult { - let dropped = Filesystem.Delete(path: layout.lease_path) - if dropped.success { - compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: cause }, subject: subject, op: op) - } else { - compute_fresh( - outcome: WorkRefusedByInfrastructure { - identity: identity, - cause: StoreUnavailable { detail: join(["a capacity refusal could not drop its producer lease at ", layout.lease_path, ": ", dropped.error], "") }, - }, - subject: subject, op: op) + let dropped = compute_drop_producer_lease(layout: layout) + match compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: cause }, subject: subject, op: op) { + ProvideFresh { outcome: o, document: d, host_record: _ } => + ProvideFresh { outcome: o, document: d, host_record: compute_lease_drop_record(dropped: dropped, layout: layout) } + ProvideAttached { identity: i, ending: e, document: d, host_record: h } => + ProvideAttached { identity: i, ending: e, document: d, host_record: h } } } +// A SEAT NOBODY HOLDS IS NOT A CHARGE, so ComputeNothingToRelease LANDS. This fn is what gates the +// settled record against compute_unreleased_record, and routing a double release to the unreleased +// record is exactly the false incident that arm exists to stop. fn compute_release_landed(r: ComputeRelease) -> Bool { match r { ComputeReleased { partition: _, reference: _, reason: _ } => true + ComputeNothingToRelease { detail: _ } => true ComputeReleaseRefused { detail: _ } => false } } @@ -899,6 +1304,7 @@ fn compute_release_landed(r: ComputeRelease) -> Bool { fn compute_release_wire(r: ComputeRelease) -> String { match r { ComputeReleased { partition: _, reference: ref_, reason: why } => join(["released ", ref_ as String, " (", why as String, ")"], "") + ComputeNothingToRelease { detail: d } => join(["no seat to return -- ", d], "") ComputeReleaseRefused { detail: d } => join(["NOT released: ", d], "") } } @@ -915,7 +1321,8 @@ fn compute_run_leased( op: WorkOperation, dependency_store: String, granted: Kibibyte, -) -> WorkOutcome { + opened: AttemptGate, +) -> LeasedRun { let existing = Filesystem.List(path: layout.checkout) let checkout = if existing.success { ComputeExecOk { stdout: "", stderr: "" } @@ -928,22 +1335,42 @@ fn compute_run_leased( } match checkout { ComputeExecFailed { exit_code, stdout: _, stderr } => - WorkRefusedByInfrastructure { identity: identity, cause: CheckoutUnavailable { detail: join(["git worktree add exited ", to_string(value: exit_code), ": ", stderr], "") } } - ComputeExecOk { stdout: _, stderr: _ } => { - let run = compute_run_unit(instance: instance, layout: layout, identity_hex: identity, argv: compute_command_argv(instance: instance, layout: layout, op: op, dependency_store: dependency_store), granted: granted) - let log = Filesystem.Write(path: layout.log_path, content: match run { - ComputeExecOk { stdout, stderr } => join([stdout, stderr], "") - ComputeExecFailed { exit_code: _, stdout, stderr } => join([stdout, stderr], "") - }) - match run { - ComputeExecFailed { exit_code, stdout: _, stderr: _ } => WorkFailed { identity: identity, exit_code: exit_code, log_path: layout.log_path } - ComputeExecOk { stdout: _, stderr: _ } => - match compute_return_outputs(instance: instance, layout: layout, declared: work_declared_outputs(op: op)) { - OutputsMismatch { detail } => WorkOutputMismatch { identity: identity, detail: detail } - OutputsReturned { outputs } => WorkSucceeded { identity: identity, outputs: outputs, log_path: if log.success { layout.log_path } else { "" } } - } + LeasedRun { outcome: WorkRefusedByInfrastructure { identity: identity, cause: CheckoutUnavailable { detail: join(["git worktree add exited ", to_string(value: exit_code), ": ", stderr], "") } }, gate: opened } + ComputeExecOk { stdout: _, stderr: _ } => + match compute_begin_launch(layout: layout, gate: opened) { + AttemptGateRefused { detail: d } => LeasedRun { outcome: WorkCancelled { identity: identity, detail: d }, gate: AttemptGateRefused { detail: d } } + AttemptGateReady { record: rec2, generation: g2 } => + compute_spawn_and_collect( + instance: instance, layout: layout, identity: identity, op: op, dependency_store: dependency_store, + granted: granted, launched: AttemptGateReady { record: rec2, generation: g2 }) } - } + } +} + +fn compute_spawn_and_collect( + instance: HostDashboardInstance, + layout: ComputeLayout, + identity: String, + op: WorkOperation, + dependency_store: String, + granted: Kibibyte, + launched: AttemptGate, +) -> LeasedRun { + let run = compute_run_unit(instance: instance, layout: layout, identity_hex: identity, argv: compute_command_argv(instance: instance, layout: layout, op: op, dependency_store: dependency_store), granted: granted) + let log = Filesystem.Write(path: layout.log_path, content: match run { + ComputeExecOk { stdout, stderr } => join([stdout, stderr], "") + ComputeExecFailed { exit_code: _, stdout, stderr } => join([stdout, stderr], "") + }) + LeasedRun { + gate: launched, + outcome: match run { + ComputeExecFailed { exit_code, stdout: _, stderr: _ } => WorkFailed { identity: identity, exit_code: exit_code, log_path: layout.log_path } + ComputeExecOk { stdout: _, stderr: _ } => + match compute_return_outputs(instance: instance, layout: layout, declared: work_declared_outputs(op: op)) { + OutputsMismatch { detail } => WorkOutputMismatch { identity: identity, detail: detail } + OutputsReturned { outputs } => WorkSucceeded { identity: identity, outputs: outputs, log_path: if log.success { layout.log_path } else { "" } } + } + }, } } @@ -1036,6 +1463,157 @@ fn compute_request_cli(repo_root: String, commit: String, operation: String, ent } } +// ── THE RECOVERY DOOR (criteria 4, 5, 6) ───────────────────────────────────────────────────── +// +// THIS IS THE CAPABILITY gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge +// NAMES AS ITS TRIGGER, and PR 1's compute_release_on says in its own annotation what had to exist +// before a discharge could ship: a termination decision bound to the unit, an attempt-to-unit +// binding that cannot release another attempt's live reservation, and a settled state a retry +// consumes. All three are here -- observe_unit_lifecycle decides from the manager, the unit name +// comes from the attempt record rather than from an identity or a listing, and the terminal +// generation IS the settled state. +// +// THAT DOES NOT DISCHARGE THE TRIGGER AND THE ROW NO LONGER SAYS IT DOES (review round four on +// gunbc#12040). The trigger asks for the capability CONSUMED BY A REAL CALLER, and this door has one +// call site -- compute_recover_cli -- with nothing executing it: the wet witnesses reach +// attempt_open, attempt_begin_launch and attempt_terminate, never this fold, and the only test-side +// mention of the door is a string_contains over the remedy TEXT. The obstacle is visible in this +// function's own first line: the attempts root is DERIVED from a HostDashboardInstance, so no +// fixture can point the door at a temporary store, and the control cannot be written before the +// store is a parameter. That parameterization is the row's trigger now. +// +// EVERY REFUSAL ARM BELOW EXISTS BECAUSE ITS OPPOSITE FREES A SEAT THAT SHOULD STAY HELD, so none +// of them widens toward "release anyway". An unreadable slot is NOT an absent one (criterion 4): a +// recovery that read "absent" from a failed read would release a seat whose attempt it never saw. +// THE ATTEMPT SLOTS ARE PER-HOST, NOT PER-IDENTITY, which is why this is its own fold rather than +// a field read off a layout: a layout is built around one work identity and recovery arrives +// holding a reference, not an identity. Deriving the root through a layout with an empty identity +// would work and would also be a second spelling of the same path (DESIGN 3). +fn compute_attempts_root(instance: HostDashboardInstance) -> NonEmptyStr { + join([dashboard_instance_compute_root(instance: instance) as String, "/attempts"], "") as NonEmptyStr +} + +// THE TERMINAL TRANSITION AND THE RELEASE ARE TWO FACTS AND THE MIDDLE ARM IS THE ONE THAT +// MATTERS. The attempt can settle -- history written, generation advanced -- and the seat can still +// fail to come back, and reporting that as a success would be exactly the recording-failure-as- +// verdict conflation the settlement path already had to be repaired for. It gets its own arm so +// the operator learns the attempt is closed AND the memory is still charged. +type ComputeRecovery + = RecoveryReleased { reference: String, verdict: String, seat: String } + | RecoverySettledButHeld { reference: String, verdict: String, seat: String } + | RecoveryDeclined { reference: String, why: String } + | RecoveryRefused { detail: String } + +fn compute_recovery_wire(r: ComputeRecovery) -> String { + match r { + RecoveryReleased { reference: ref_, verdict: v, seat: rel } => join(["recovered ", ref_, ": ", v, "; ", rel], "") + RecoverySettledButHeld { reference: ref_, verdict: v, seat: rel } => + join(["SETTLED BUT STILL CHARGED ", ref_, ": the attempt is closed (", v, ") and the seat did NOT come back -- ", rel, "; this host under-admits by that grant until the ledger accepts a release for this reference"], "") + RecoveryDeclined { reference: ref_, why: w } => join(["declined ", ref_, ": ", w], "") + RecoveryRefused { detail: d } => join(["recovery refused: ", d], "") + } +} + +// THE RE-CHECK UNDER THE LEASE (criterion 5), AND IT IS THE SAME GENERATION OR IT IS NOTHING. +// The slot is read, the unit is observed, the trigger is evaluated -- and then the terminal +// transition is committed EXPECTING THE GENERATION THAT WAS READ. If the producer advanced in the +// meantime, the observation recovery decided on is stale and the store refuses it. The re-check is +// not a second read that could also go stale; it is the compare-and-set itself, which is the only +// form of re-check that cannot be overtaken between the checking and the acting. +fn compute_recover_attempt(instance: HostDashboardInstance, reference: NonEmptyStr) -> ComputeRecovery { + let attempts_root = compute_attempts_root(instance: instance) + match attempt_slot_read(root: attempts_root, reference: reference) { + AttemptSlotUnreadable { detail: d } => + RecoveryRefused { detail: join(["the attempt slot for ", reference as String, " could not be read (", d, "), and an unreadable slot is not an absent one -- releasing on a read that failed would return a seat whose attempt was never observed"], "") } + AttemptSlotAbsent => + RecoveryRefused { detail: join(["no attempt slot exists for ", reference as String, "; there is no record binding that reference to a unit, and this door will not release a seat it cannot name the attempt of"], "") } + AttemptSlotHeld { record: rec, generation: g } => { + let lifecycle = observe_unit_lifecycle(unit: rec.unit as NonEmptyStr) + match now_epoch_seconds() { + Absent => RecoveryRefused { detail: "the host clock could not be read as epoch seconds, and the reserved-state trigger is a comparison against a deadline" } + Present { value: now } => + match recovery_trigger(record: rec, lifecycle: lifecycle, now: now) { + RecoveryTooEarly { deadline: d, now: n } => RecoveryDeclined { reference: rec.reference, why: recovery_trigger_wire(t: RecoveryTooEarly { deadline: d, now: n }) } + RecoveryUnitNotEnded { lifecycle: u } => RecoveryDeclined { reference: rec.reference, why: recovery_trigger_wire(t: RecoveryUnitNotEnded { lifecycle: u }) } + RecoveryStateNotRecoverable { state: st } => RecoveryDeclined { reference: rec.reference, why: recovery_trigger_wire(t: RecoveryStateNotRecoverable { state: st }) } + RecoveryMayTerminate { reason: why } => + match attempt_terminate(root: attempts_root, record: rec, expected: g, verdict: AttemptRecovered, detail: join([why, "; unit ", unit_lifecycle_wire(u: lifecycle)], "")) { + AttemptLostRace { expected: e, observed: o } => + RecoveryRefused { detail: join(["the attempt moved while recovery was deciding: expected ", e, " and the slot holds ", o, "; the observation this recovery would act on is stale, so nothing is released"], "") } + AttemptTransitionRefused { detail: d } => RecoveryRefused { detail: join(["the attempt slot would not take the terminal generation: ", d], "") } + AttemptAdvanced { state: _, generation: _ } => + compute_recovery_after_settlement( + reference: rec.reference, + verdict: join([why, "; unit ", unit_lifecycle_wire(u: lifecycle)], ""), + returned: compute_recover_release(instance: instance, reference: reference, reason: why)) + } + } + } + } + } +} + +fn compute_recovery_after_settlement(reference: String, verdict: String, returned: ComputeRelease) -> ComputeRecovery { + if compute_release_landed(r: returned) { + RecoveryReleased { reference: reference, verdict: verdict, seat: compute_release_wire(r: returned) } + } else { + RecoverySettledButHeld { reference: reference, verdict: verdict, seat: compute_release_wire(r: returned) } + } +} + +// THE SEAT COMES BACK THROUGH PR 1'S OWN RELEASE PATH, never a second one. compute_release_on +// reads, folds and PROPOSES against the folded pool, so a reference the ledger is not holding is +// refused at the proposal rather than appended -- which is what keeps a recovery from poisoning the +// whole partition with an UnknownEncumbrance every later read would refuse on. +fn compute_recover_release(instance: HostDashboardInstance, reference: NonEmptyStr, reason: String) -> ComputeRelease { + match compute_capacity_subject(instance: instance) { + ComputeSubjectHostUnresolved { host: h } => ComputeReleaseRefused { detail: join(["no capacity subject resolves for host ", h as String], "") } + ComputeSubjectResolved { subject: subj } => + compute_release_on( + store: compute_capacity_store(subject: subj), + partition: subj.partition, + appropriation: kibibyte(count: 0), + reference: reference, + reason: join(["recovered: ", reason], "") as NonEmptyStr) + } +} + +// THE DOOR A WORKER OR AN OPERATOR ACTUALLY OPENS. Three exits and they are the three the rest of +// this provider uses: 0 the seat came back, 1 recovery looked and declined (which is the SAFE +// answer and must not read as a tool failure), 2 recovery could not establish enough to answer. +fn compute_recover_cli(repo_root: String, reference: String, receipt_path: String) -> ProcessExit { + match dashboard_instance_for_repo_root(repo_root: repo_root) { + DashboardInstanceRootUnknown { repo_root: r } => ExitFailure { code: 2, reason: join(["compute-recover: no dashboard instance is rooted at ", r], "") } + DashboardInstanceResolved { instance } => + if trim(s: reference) == "" { + ExitFailure { code: 2, reason: "compute-recover: a reservation reference is required (it is the attempt slot's key: @)" } + } else { + compute_recover_exit( + outcome: compute_recover_attempt(instance: instance, reference: trim(s: reference) as NonEmptyStr), + receipt_path: receipt_path) + } + } +} + +// THE RECOVERED CASE WRITES ITS RECEIPT TOO, and that is not symmetry for its own sake: exit 0 +// carries no text, so a discharge that reported only a status would leave the operator who ran it +// unable to say WHICH seat came back or on what evidence. The durable history is the attempt +// slot's terminal generation; this is the copy the caller can read without opening the store. +fn compute_recover_exit(outcome: ComputeRecovery, receipt_path: String) -> ProcessExit { + let wire = compute_recovery_wire(r: outcome) + let written = Filesystem.Write(path: receipt_path, content: join([wire, "\n"], "")) + if !written.success { + ExitFailure { code: 2, reason: join(["compute-recover: the receipt could not be written to ", receipt_path, ": ", written.error, "; the outcome was ", wire], "") } + } else { + match outcome { + RecoveryReleased { reference: _, verdict: _, seat: _ } => ExitSuccess + RecoverySettledButHeld { reference: _, verdict: _, seat: _ } => ExitFailure { code: 2, reason: wire } + RecoveryDeclined { reference: _, why: _ } => ExitFailure { code: 1, reason: wire } + RecoveryRefused { detail: _ } => ExitFailure { code: 2, reason: wire } + } + } +} + // THE RECEIPT STAYS THE DOCUMENT, AND THE HOST-RECORD FACT GETS ITS OWN FILE BESIDE IT. // // The first version of this appended the host-record sentence to the receipt, and the srv1 diff --git a/dag/gunbc/compute/work_request.dag b/dag/gunbc/compute/work_request.dag index 16883a0830b..55753c06478 100644 --- a/dag/gunbc/compute/work_request.dag +++ b/dag/gunbc/compute/work_request.dag @@ -127,11 +127,17 @@ type WorkOutput { // THE FIVE ENDINGS, and only five (compute-exact-work-contract's red control: a machine that killed // the work cannot render as the work having failed). Every arm carries the identity so a caller can // never attach a verdict to a different request. +// A CANCELLATION CARRIES WHY, and the arm was a bare identity until a real run made the gap +// visible. The only producer of this arm is a launch refused by the attempt gate -- somebody else +// ended this attempt before it spawned -- and an ending of "cancelled" with no cause cannot be +// told apart from any other cancellation by the caller who reads the document. The detail is in +// the durable outcome for the same reason every other arm's is: the next reader of this identity +// gets the same account the first caller got. type WorkOutcome = WorkSucceeded { identity: String, outputs: List, log_path: String } | WorkFailed { identity: String, exit_code: Int, log_path: String } | WorkRefusedByInfrastructure { identity: String, cause: WorkInfrastructureRefusal } - | WorkCancelled { identity: String } + | WorkCancelled { identity: String, detail: String } | WorkOutputMismatch { identity: String, detail: String } // Infrastructure refusals are typed and counted, never a widen: a producer already holds the lease @@ -170,21 +176,55 @@ fn work_outcome_identity(o: WorkOutcome) -> String { WorkSucceeded { identity, outputs: _, log_path: _ } => identity WorkFailed { identity, exit_code: _, log_path: _ } => identity WorkRefusedByInfrastructure { identity, cause: _ } => identity - WorkCancelled { identity } => identity + WorkCancelled { identity, detail: _ } => identity WorkOutputMismatch { identity, detail: _ } => identity } } -fn work_outcome_ending(o: WorkOutcome) -> String { +// HOW A WORK OUTCOME ENDED, WITH ITS PAYLOAD DROPPED. It is the closed set the ending words were +// always drawn from, typed once so a reader that stores an ending (the attempt slot's terminal +// generation) decodes against the set rather than accepting any word. work_outcome_ending is its +// spelling, and work_ending_decode is the inverse of that one spelling, not a second vocabulary. +type WorkEnding + = WorkEndedSucceeded + | WorkEndedFailed + | WorkEndedRefusedByInfrastructure + | WorkEndedCancelled + | WorkEndedOutputMismatch + +fn work_outcome_ending_of(o: WorkOutcome) -> WorkEnding { match o { - WorkSucceeded { identity: _, outputs: _, log_path: _ } => "succeeded" - WorkFailed { identity: _, exit_code: _, log_path: _ } => "failed" - WorkRefusedByInfrastructure { identity: _, cause: _ } => "refused_by_infrastructure" - WorkCancelled { identity: _ } => "cancelled" - WorkOutputMismatch { identity: _, detail: _ } => "output_mismatch" + WorkSucceeded { identity: _, outputs: _, log_path: _ } => WorkEndedSucceeded + WorkFailed { identity: _, exit_code: _, log_path: _ } => WorkEndedFailed + WorkRefusedByInfrastructure { identity: _, cause: _ } => WorkEndedRefusedByInfrastructure + WorkCancelled { identity: _, detail: _ } => WorkEndedCancelled + WorkOutputMismatch { identity: _, detail: _ } => WorkEndedOutputMismatch + } +} + +fn work_ending_wire(e: WorkEnding) -> String { + match e { + WorkEndedSucceeded => "succeeded" + WorkEndedFailed => "failed" + WorkEndedRefusedByInfrastructure => "refused_by_infrastructure" + WorkEndedCancelled => "cancelled" + WorkEndedOutputMismatch => "output_mismatch" } } +fn work_ending_decode(word: String) -> WorkEnding? { + if word == work_ending_wire(e: WorkEndedSucceeded) { Present { value: WorkEndedSucceeded } } + else if word == work_ending_wire(e: WorkEndedFailed) { Present { value: WorkEndedFailed } } + else if word == work_ending_wire(e: WorkEndedRefusedByInfrastructure) { Present { value: WorkEndedRefusedByInfrastructure } } + else if word == work_ending_wire(e: WorkEndedCancelled) { Present { value: WorkEndedCancelled } } + else if word == work_ending_wire(e: WorkEndedOutputMismatch) { Present { value: WorkEndedOutputMismatch } } + else { none } +} + +fn work_outcome_ending(o: WorkOutcome) -> String { + work_ending_wire(e: work_outcome_ending_of(o: o)) +} + fn work_refusal_detail(r: WorkInfrastructureRefusal) -> String { match r { ProducerInFlight { lease_path } => join(["a producer already holds the lease at ", lease_path, "; attach later, do not start a second one"], "") @@ -228,7 +268,9 @@ fn work_outcome_json(o: WorkOutcome, subject: WorkSubject, op: WorkOperation) -> WorkRefusedByInfrastructure { identity: _, cause } => [ json_kv(key: "cause", value: json_string(s: work_refusal_detail(r: cause))), ] - WorkCancelled { identity: _ } => [] + WorkCancelled { identity: _, detail } => [ + json_kv(key: "detail", value: json_string(s: detail)), + ] WorkOutputMismatch { identity: _, detail } => [ json_kv(key: "detail", value: json_string(s: detail)), ] diff --git a/dag/gunbc/recurring_failure_mode/a_control_that_shares_its_derivation_with_its_subject.dag b/dag/gunbc/recurring_failure_mode/a_control_that_shares_its_derivation_with_its_subject.dag new file mode 100644 index 00000000000..ca61c314f95 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/a_control_that_shares_its_derivation_with_its_subject.dag @@ -0,0 +1,39 @@ +module gunbc.recurring_failure_mode.a_control_that_shares_its_derivation_with_its_subject + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data a_control_that_shares_its_derivation_with_its_subject: RecurringFailureMode = RecurringFailureMode { + identity: "a_control_that_shares_its_derivation_with_its_subject" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a control whose content is DERIVED FROM the thing it is meant to discriminate, so it cannot disagree with it. The general form is one sentence -- A CONTROL WRITTEN FROM THE IMPLEMENTATION CAN ONLY AGREE WITH IT -- and the two routes to it look different enough that neither author recognised the other's until they were put side by side. DESCRIBING: read what the code does, write the assertion that says so. COPYING: inline the production body into the control with one input swapped. Copying is simply the most literal way of writing a control from the implementation.", + + "HARM: the suite reports coverage where it has none, and reports it most confidently exactly where the subject is most load-bearing, because a heavily-relied-on fold is the one an author is most likely to describe accurately rather than interrogate. The mutation that removes the wall leaves the control green, so the wall's absence is invisible to every later reader -- and the control is then CITED as the reason the wall is safe to lean on.", + + "SPECIMEN ONE, DESCRIBING (gunbc#11962, review 69784, 2026-09-21). A witness over the /proc/meminfo parse asserted count(all_metrics) == 8 against a fixture whose eighth line is `HugePages_Total: 0` -- a unitless page count the parse was minting as a Kibibyte. The control did not catch the defect; it RECORDED it, because it was written by reading the fold and stating the result. The same change carried a second instance: a termination control that asserted completed-plus-unknown frees a seat, which was the defect the four-state predicate existed to remove.", + + "SPECIMEN TWO, COPYING (gunbc#12017, review 69791, 2026-09-21, session loyal-swift-608). a_refused_identity_refuses_the_store -- a RED written to satisfy a previous review -- carried the production door's body INLINED with only the verdict source swapped, so it evaluated its own copy of the green test it existed to guard. Deleting that test from the real door would have left the control green. The annotation above it asserted the opposite in as many words.", + + "THE SMELL THAT NEEDS NO RUN, and it is what makes this cheaper to catch than to prove: ASK WHAT THE CONTROL SHARES WITH ITS SUBJECT. If it re-derives, re-implements or re-describes the thing under test, it is suspect before any mutation is attempted. Specimen two shared a copied body; specimen one shared a description. The mutation is the proof; the shared-derivation question is the smell that says to go looking.", + + "AND THE REPAIR HAS ITS OWN FAILURE MODE, WHICH IS THE MORE TRANSFERABLE HALF. The first fix of specimen one added the missing unit comparison -- and mutating that comparison away left the control STILL GREEN. A unitless line is excluded by the ARITY requirement rather than by the comparison, and /proc/meminfo publishes no wrong-unit line at all, so the comparison had no instance in the fixture population to discriminate and was a permanently green decoration (DESIGN 4b: worse than absent, because it is cited as coverage). THE FIXTURE POPULATION HAS TO CONTAIN THE CASE THE CHECK EXISTS FOR -- and a REAL-WORLD CORPUS IS EXACTLY WHERE THAT CASE TENDS NOT TO OCCUR, which is why the fixture is where it must be authored. Adding `SomeFutureField: 64 MB` is what made the mutation fail.", + + "NOT predicate_vacuously_true_on_an_empty_domain, and the boundary matters because the remedy differs. There the domain is EMPTY and the check answers true about nothing. Here the domain is POPULATED and healthy-looking -- seven real metrics -- and merely lacks the one case the check discriminates. An emptiness guard does not catch it; only asking what case this check exists for, and whether the fixture contains it, does.", + + "RUNG FOUND AT: mitigatable, by the two habits above -- run the mutation before reporting a control, and ask what the control shares with its subject. Nothing refuses a control that agrees with its subject, because agreement is what a passing control looks like.", + + "CEILING: mechanically preventable. A mutation pass that rebinds each control's subject to a wrong arm and requires the control to red is decidable over the corpus, and a control that survives every mutation of its own subject is reportable as establishing nothing.", + + "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: every control is executed against a mutated subject and must red, with a control that survives all mutations of its subject reported as non-discriminating. Deliberately not 'review controls for copied bodies' -- specimen one had no copied body and would pass that review unchanged.", + + "CONSUMPTION: the derived gunbc.recurring_failure_mode.roster recurring_failure_mode_roster includes this per-class declaration.", + ], + + evidence: [ + decl_ref(module_path: "extdeps.linux.proc_meminfo", decl_name: "meminfo_line_metric"), + decl_ref(module_path: "test.claim.os_proc_meminfo_witness", decl_name: "parsing_meminfo_reads_the_named_fields_and_refuses_a_missing_one"), + decl_ref(module_path: "gunbc.compute.work_provider_local", decl_name: "unit_termination_decide"), + ], +} diff --git a/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag b/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag index 7abfa38c7ee..4d4687f45b5 100644 --- a/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag +++ b/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag @@ -18,11 +18,17 @@ data a_held_compute_seat_has_no_in_corpus_discharge: RecurringFailureMode = Recu "THERE IS NO SAFE MANUAL DISCHARGE UNDER LIVE ADMISSION, and saying so is part of the row rather than a caveat on it. Clearing the capacity partition by hand while this host is admitting work removes the very record the admission arithmetic folds, so the next requests are admitted against memory the stuck grant still holds -- trading a host that under-admits for one that over-promises, which is the direction this whole change exists to prevent. Any manual intervention requires compute admission STOPPED on the host and every gunbc-compute unit PROVEN gone, in that order.", + "THE TRIGGER HAS NOT FIRED, AND AN EARLIER REVISION OF THIS ROW SAID IT HAD. The lifecycle capability the trigger names is gunbc.compute.work_provider_local compute_recover_cli, and the CORPUS half is real: it decides termination from the manager and the cgroup through unit_lifecycle_decide rather than from a state word; it binds the unit from the attempt record the producer wrote, so it cannot stop a unit belonging to a different attempt; it commits the terminal generation EXPECTING the generation it read, so a producer that advanced in the meantime wins and the recovery is refused by the store; and the terminal generation IS the settled state, carrying the verdict and why. What is missing is the half the trigger actually asked for -- CONSUMED BY A REAL CALLER. At gunbc#12040 head d2be4987 compute_recover_attempt appears exactly twice in the tree: its own definition, and one call from compute_recover_cli. The only test-side mention of the door is a string_contains over the remedy TEXT in work_request_witness_test, and DESIGN section 5 rules in those words that a typecheck and a .contains() grep are not consumers. The wet witnesses reach attempt_open, attempt_begin_launch, attempt_terminate and the provider gate; none of them reach this door. So the row failed the test it wrote for itself, which is the sharpest form of rung inflation: not an optimistic reading of the evidence, but a retirement condition marked discharged while its own words went unmet.", + + "AND THE DISCHARGE DOES NOT ANNOUNCE ITSELF ON A HALF-SUCCESS, which is the arm that would have quietly re-created this class under a name that reads as fixed. The terminal transition landing and the seat coming back are two facts: gunbc.compute.work_provider_local RecoverySettledButHeld is the arm where the attempt closed and the ledger refused the release, and it exits 2 saying the host still under-admits by that grant. A recovery that reported success on the transition alone would leave exactly the state this row describes while claiming the row was retired.", + "RUNG FOUND AT: mitigatable. The state is reachable, its harm is bounded to one host's compute appropriation, it is visible in the outcome document and in the partition, and it never over-promises.", - "CEILING: mechanically preventable. A discharge route exists to be built -- the evidence needed is a termination decision bound to the unit plus a settled lifecycle state that a retry consumes -- so this is not a class that must stay a ratchet.", + "CURRENT RUNG: mitigatable, the same rung this class was found at. It is stated here rather than left implied by the absence of a climb, because this row PREVIOUSLY REPORTED mechanically preventable and a reader who saw that number is owed the correction explicitly. Nothing about the code moved to justify the demotion and nothing has regressed: the door is as good as it was, and the evidence for it never existed. DESIGN section 4b(1) is the governing sentence -- the reported rung must equal the rung established by EXECUTED evidence, a discriminating RED on the real acceptance path plus an accepted positive control -- and a door with one call site and no executing control establishes nothing, however well it is written. Rung inflation is worse than sitting low because an inflated class never ranks for climbing, and the thing that stops being asked about here is a compute seat nobody can reclaim.", + + "CEILING: mechanically preventable, and the reason it goes no higher is worth stating rather than leaving as an unexplained stop. Structural impossibility would mean no reachable state in which a seat is held with nothing running, and that would require proving a systemd transient unit has stopped using memory from outside it -- an external fact at the boundary DESIGN 4b keeps OFF the ladder. So this class is at its ceiling, and the honest residual is that a seat stays charged until someone runs the door.", - "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY AND NOT AN ARTIFACT: the compute reservation LIFECYCLE capability -- a discharge that (a) decides termination from authoritative absence or an observed-empty cgroup rather than from a state word, (b) binds the attempt and its unit from the authoritative attempt record so releasing one cannot release another's live reservation, (c) coordinates with a pending producer so a release cannot race a launch that has not happened yet, and (d) produces a settled state a retry consumes, with history kept. Until a discharge with all four properties is consumed by a real caller, this row stands.", + "NEXT-RUNG TRIGGER, A CAPABILITY AND NOT A CHORE: a door whose STORE IS A PARAMETER, sufficient for an executing control to drive a held seat through discharge against a temporary store. The distinction matters because write a test is not the obstacle here and naming it as the trigger would be a trigger nobody can satisfy. compute_recover_attempt takes a HostDashboardInstance and derives its attempts root from it through compute_attempts_root, so a fixture cannot point the door anywhere but the real compute root of a real instance -- there is no argument that would let a witness build the held slot in the tempdir the wet harness already creates for every other attempt-lifecycle claim. That is a design fact about this door and not a gap in the harness, which is why the trigger names the parameterization rather than the control. Once the store is a parameter, the control is within reach of machinery that already exists: the wet witness builds real CAS slots in a temporary directory today. THE CONTROL IS WHAT RETIRES THIS ROW, and the parameterization is what makes the control writable.", "CONSUMPTION: the derived gunbc.recurring_failure_mode.roster recurring_failure_mode_roster includes this per-class declaration, and gunbc.compute.work_provider_local compute_stuck_reservation_remedy carries the remedy sentence into the refusal a caller actually receives.", ], @@ -32,5 +38,8 @@ data a_held_compute_seat_has_no_in_corpus_discharge: RecurringFailureMode = Recu decl_ref(module_path: "gunbc.compute.work_provider_local", decl_name: "unit_termination_frees_capacity"), decl_ref(module_path: "gunbc.compute.host_capacity", decl_name: "compute_release"), decl_ref(module_path: "test.claim.compute.work_request_witness_test", decl_name: "only_proven_absence_or_an_ended_cgroup_frees_a_seat"), + decl_ref(module_path: "gunbc.compute.work_provider_local", decl_name: "compute_recover_cli"), + decl_ref(module_path: "gunbc.compute.work_provider_local", decl_name: "unit_lifecycle_decide"), + decl_ref(module_path: "test.claim.compute.work_request_witness_test", decl_name: "the_lifecycle_verdict_has_four_states_and_unknown_carries_why"), ], } diff --git a/dag/gunbc/recurring_failure_mode/an_enumeration_capped_by_its_reading_tool.dag b/dag/gunbc/recurring_failure_mode/an_enumeration_capped_by_its_reading_tool.dag new file mode 100644 index 00000000000..971c6e0b9ee --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/an_enumeration_capped_by_its_reading_tool.dag @@ -0,0 +1,41 @@ +module gunbc.recurring_failure_mode.an_enumeration_capped_by_its_reading_tool + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data an_enumeration_capped_by_its_reading_tool: RecurringFailureMode = RecurringFailureMode { + identity: "an_enumeration_capped_by_its_reading_tool" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a census whose denominator was silently reduced by the READING TOOL, and then used as the justification for a deletion or a re-signature. The author enumerates the consumers -- correctly -- and pipes the enumeration through a display cap (`head -n`, a `take`, a paged view, a truncating summary). Every line that survives is true. Nothing in the output says a line did not survive. The edit is then made against the survivors and is complete with respect to a population that was never the population.", + + "HARM, AND THE SHARP EDGE IS THAT IT DOES NOT FAIL RANDOMLY. The cap fails TOWARD THE CONSUMERS NOTHING ELSE WOULD CATCH. A module with few mentions of the symbol sorts to the bottom of the enumeration and is cut first -- and having few mentions is exactly what makes it unlikely to be caught by any other route. So the arms the cap hides are CORRELATED with the arms that matter, and the correlation is positive: the less a consumer is referenced, the more likely both that the cap hides it and that no gate compiles it.", + + "WHY IT SURVIVES REVIEW, WHICH IS WHAT MAKES IT A CLASS RATHER THAN A SLIP: incompleteness is a property of the READING, not of the diff. The diff is internally consistent, every migrated site is correct, the typechecker is silent because the missed consumers are outside whatever closure the gate compiles, and the enumeration itself is not an artifact anybody reviews -- it happened in a shell and left no trace. A reviewer re-running the enumeration UNCAPPED is the only thing that finds it.", + + "SPECIMEN (gunbc#11962, review 69769, 2026-09-21). product.capacity.pool_events SeatRequest was re-signatured to SeatRequest. The consumers WERE enumerated before the change -- and the enumeration was piped through `head -12`. Six construction sites exist; the cap showed the first four files and hid gunbc.instruments.fabric_seat_probe and gunbc.instruments.fabric_event_log_probe, which are operator-invoked entry points that NO required lane compiles. The breakage would have surfaced the next time an operator ran a probe, with a type error in a module the author had never opened. The re-run, unfiltered and uncapped, found all six.", + + "THE PLACE IT LANDED IS THE PLACE DESIGN 3 SAYS ENUMERATION IS LOAD-BEARING: 'Outside the required gate the substrate still refuses and nothing asks it to ... so for a root outside the gate, enumerate the consumers by name before you delete.' The rule exists precisely because the compiler is not the backstop there. A capped enumeration removes the only backstop that remained.", + + "THIS IS NOT truncated_local_diagnostics_indistinguishable_from_the_complete_set, and the boundary is worth stating because the two look alike. There, an ORACLE DIED mid-measure and its partial output read as a verdict -- nobody chose the truncation, and the discriminators are out of band (the abort line, the missing receipt, the stack limit). Here the truncation is CHOSEN, by the reader, as a display convenience, on a population the reader is about to act on; there is no abort to notice and no receipt to be missing. Same silence, different cause, different discriminator, different remedy.", + + "THE RULE, SHARPER THAN EITHER STATEMENT THAT PRODUCED IT (reviewer on gunbc#11962, endorsed by the owning manager): PRESERVE THE COMPLETE CONSUMER SET AS THE MIGRATION INPUT, AND CHECK EVERY AFFECTED OUT-OF-GATE ROOT FROM THAT SET; TRUNCATE ONLY ITS DISPLAY. That splits the legitimate use of a cap from the illegitimate one cleanly, which neither `never truncate` nor `do not use head` manages: a cap on what you LOOK AT is fine and is how anyone reads a long list, and a cap on what you ACT FROM is the defect. The input and the view are two things, and the failure is using one as the other.", + + "DISCRIMINATOR, and it is a question about the ENUMERATION rather than about the diff: was the enumeration that justified this deletion or re-signature itself UNBOUNDED? Not 'did you check the consumers' -- the author of this specimen did check them. Whether the check could have shown all of them.", + + "RUNG FOUND AT: mitigatable, by the discipline of not capping a census and by a reviewer re-running it. Nothing refuses a capped enumeration because nothing sees one.", + + "CEILING: mechanically preventable. A re-signature or deletion of a declaration can have its consumer set computed from the namespace tree -- the same Node-tree read DESIGN 3 already relies on for citation checking -- and compared against what the change touched, so an unmigrated consumer outside the gate is a refusal rather than a surprise. DESIGN 3c names the same climb for dangling declarations: the consumer set is a fact the tree carries, not one a shell has to be trusted to report.", + + "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: a change that alters a declaration's signature or removes it is checked against the declaration's full consumer set as derived from the namespace tree, with consumers outside the required gate included by construction. Not 'do not use head' -- a habit is not a wall, and the class would stay exactly as alive under a different paging tool.", + + "CONSUMPTION: the derived gunbc.recurring_failure_mode.roster recurring_failure_mode_roster includes this per-class declaration.", + ], + + evidence: [ + decl_ref(module_path: "product.capacity.pool_events", decl_name: "SeatRequest"), + decl_ref(module_path: "gunbc.instruments.fabric_seat_probe", decl_name: "fabric_seat_probe"), + decl_ref(module_path: "gunbc.instruments.fabric_event_log_probe", decl_name: "probe_root_pool"), + ], +} diff --git a/dag/gunbc/recurring_failure_mode/an_unreached_measurement_renders_as_a_failed_one.dag b/dag/gunbc/recurring_failure_mode/an_unreached_measurement_renders_as_a_failed_one.dag index 548be83c63a..b6f36ea27ad 100644 --- a/dag/gunbc/recurring_failure_mode/an_unreached_measurement_renders_as_a_failed_one.dag +++ b/dag/gunbc/recurring_failure_mode/an_unreached_measurement_renders_as_a_failed_one.dag @@ -17,6 +17,10 @@ data an_unreached_measurement_renders_as_a_failed_one: RecurringFailureMode = Re "SPECIMEN (2026-09-11, gunbc main). Two consecutive main runs on two slots of one host reported required-witnesses-floor FAILURE with standing=measurement_unreached: srv4-04 on run 34570523344 (head d94bcf680) could not read a cargo registry source file mid-compile, and srv4-16 on run 34571176215 (head ec1571e89) could not write a target .rmeta. Both are ENOENT rather than ENOSPC, which is what rules out a full disk and is itself a distinguishing fact worth keeping. THE COST LANDED EXACTLY WHERE THIS CLASS PREDICTS: d94bcf680 IS #11032, the repair for a separate witness-budget defect that had main red, so the one run that could have told its lane whether the repair worked reported red while measuring nothing -- and the natural reading, `still red after the fix`, was unsupported in either direction. Three lanes were downstream of that misreading.", + "SECOND SPECIMEN, ONE LAYER DOWN AND WITH THE DISTINCTION PARTLY PRESENT (2026-09-22, gunbc#12040). `claim_batch` over dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag WITHOUT --wet, on the hermetic route, ended six of nine identities at shell.Mktemp.DirWithTemplate, which declares no mock_response. The line it prints is `FAIL (hermetic route has no arm for DirWithTemplate: operation declares no mock_response -- the claim never reached its subject, so this is a route gap and not a verdict)`. THE HARNESS IS HONEST AND STILL CONFLATES, which is the new fact this receipt carries: the cause is present, correct, and says IN WORDS that this is not a verdict -- and it is carried in PROSE AFTER THE VERDICT TOKEN, so every mechanical reader takes the token and drops the disclaimer. `grep -c ^FAIL` counts six reds, `grep -c ^PASS` reports three of nine, and a reader scanning the verdict column sees a witness that is mostly red. The same nine are 9/9 PASS with --wet over the same tree. THIS IS NOT THE HARNESS CONFLATING A ROUTE GAP WITH A VERDICT, and the distinction decides the remedy. The cause is computed, correct, and printed; what fails is that it is carried UNDER A TOKEN THAT READS AS A VERDICT. So the remedy this specimen argues for is narrower than the first one and is NOT more annotation: the token is the surface, and a route gap needs A DISTINCT TERMINAL of its own rather than a parenthetical attached to FAIL. A reader instructed to check the parenthetical is a mitigation with the same dependency on a human knowing to look that the RUNG note below names.", + + "WHY THAT IS THE SAME CLASS AND NOT A SEPARATE ONE, since the instruments differ: the invalid state is identical -- an unreached subject presented in the position that means `this subject was adjudicated and lost` -- and only the grain moves, from a required lane at the merge surface to one identity in a batch run. The two specimens also bracket the remedy usefully. The first has the distinction typed in a field the deciding surface never reads; the second has it rendered where every reader sees it and no reader can act on it mechanically. Emitting the standing is not sufficient in either, which is what the next-rung trigger below already says.", + "NOT THE SAME AS A FLAKE, and the distinction matters for what to do next: a flake is a measurement that reached its subject and got the wrong answer, so re-running samples the same distribution. An unreached measurement has no answer to sample; re-running is only worth doing if the reason it could not reach is itself transient, and NOTHING IN THE RED SAYS WHETHER IT IS. Treating the two alike is how a broken runner gets re-run indefinitely.", "RUNG: found at 1, mitigatable. The distinction is not lost -- the standing field is typed and present in the log, so a reader who opens it can always recover which case they are in. What is lost is that the DECIDING surface does not carry it, so recovery depends on a human knowing to look, which is exactly the dependency a mitigation has and a guarantee does not.", diff --git a/dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag b/dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag new file mode 100644 index 00000000000..b643ec9e7a9 --- /dev/null +++ b/dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag @@ -0,0 +1,374 @@ +module test.claim.compute.attempt_lifecycle_wet_witness + +import extdeps.shell +import extdeps.filesystem.filesystem_io { Filesystem } +import std.types { Bool, Int, NonEmptyStr, String } +import std.algebra { trim } +import std.measure { kibibyte, kibibyte_count } +import std.durable_compare_and_set { CasGeneration, cas_generation_count, cas_generation_first } +import gunbc.compute.work_provider_local { + ComputeLayout, + AttemptGate, AttemptGateReady, AttemptGateRefused, compute_begin_launch, + AttemptSettlement, AttemptSettled, AttemptNotSettled, AttemptUnsettleable, + compute_settle_attempt, compute_attempt_settlement_wire, attempt_settlement_host_record, + host_record_was_written, +} +import gunbc.compute.work_request { + WorkEnding, WorkEndedSucceeded, WorkEndedFailed, WorkEndedRefusedByInfrastructure, WorkEndedCancelled, WorkEndedOutputMismatch, +} +import gunbc.compute.attempt_lifecycle { + AttemptRecord, AttemptState, AttemptReserved, AttemptLaunching, AttemptTerminal, + AttemptVerdict, AttemptWorkEnded, AttemptRecovered, attempt_verdict_wire, + AttemptSlotReading, AttemptSlotAbsent, AttemptSlotHeld, AttemptSlotUnreadable, attempt_slot_read, + AttemptTransition, AttemptAdvanced, AttemptLostRace, AttemptTransitionRefused, + attempt_open, attempt_begin_launch, attempt_terminate, attempt_transition_advanced, attempt_transition_wire, + attempt_state_wire, attempt_record_wire, attempt_record_decode, compute_pre_launch_ceiling_seconds, + UnitLifecycle, UnitTerminatedSuccess, UnitTerminatedFailure, UnitTerminatedCauseUnknown, + UnitStillRunning, UnitLifecycleUnknown, unit_lifecycle_ended, unit_lifecycle_wire, + RecoveryTrigger, RecoveryMayTerminate, RecoveryTooEarly, RecoveryUnitNotEnded, RecoveryStateNotRecoverable, + recovery_trigger, recovery_trigger_fires, recovery_trigger_wire, +} + +// WET CONTROLS FOR THE ATTEMPT LIFECYCLE. Every transition below is a real compare-and-set against +// a real generation-file store in a real temporary directory. The exclusion being asserted is the +// one the operating system performs on the write, not one this witness arranges. + +fn fresh_root() -> String { + shell.Mktemp.DirWithTemplate(template: "/tmp/gunbc_attempt.XXXXXX").path +} + +fn record_for(reference: String) -> AttemptRecord { + AttemptRecord { + identity: "abcdef0123456789", + reference: reference, + unit: join(["gunbc-compute-abcdef0123456789-", reference], ""), + granted: kibibyte(count: 27262976), + opened_at: 1800, + launch_deadline: 2000, + state: AttemptReserved, + } +} + +fn generation_of(r: AttemptSlotReading) -> Int { + match r { + AttemptSlotHeld { record: _, generation: g } => cas_generation_count(g: g) + AttemptSlotAbsent => 0 + AttemptSlotUnreadable { detail: _ } => 0 - 1 + } +} + +fn state_word_of(r: AttemptSlotReading) -> String { + match r { + AttemptSlotHeld { record: rec, generation: _ } => attempt_state_wire(s: rec.state) + AttemptSlotAbsent => "" + AttemptSlotUnreadable { detail: _ } => "" + } +} + +fn held_record(r: AttemptSlotReading) -> AttemptRecord { + match r { + AttemptSlotHeld { record: rec, generation: _ } => rec + AttemptSlotAbsent => record_for(reference: "") + AttemptSlotUnreadable { detail: _ } => record_for(reference: "") + } +} + +fn lost_race(t: AttemptTransition) -> Bool { + match t { + AttemptLostRace { expected: _, observed: _ } => true + AttemptAdvanced { state: _, generation: _ } => false + AttemptTransitionRefused { detail: _ } => false + } +} + +// CRITERION 3, ORDER ONE: THE TERMINAL TRANSITION WINS AND THE LAUNCH IS REFUSED BEFORE IT SPAWNS. +// +// This is the interleaving that produces an unbacked launch if the two steps are not one: the +// attempt reserves, recovery decides it is dead and terminates it, and THEN the producer -- which +// has been paused somewhere between reserving and spawning -- goes to launch. With a gate, the +// producer's compare-and-set is refused against a generation that has moved, and it learns this +// BEFORE it spawns rather than after. The refusal is the store's, not a check this witness wrote. +test fn a_terminal_transition_refuses_a_launch_that_had_not_spawned_yet() -> Bool { + let root = fresh_root() as NonEmptyStr + let record = record_for(reference: "attempt-terminate-first") + let opened = attempt_open(root: root, record: record) + let after_open = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let terminated = attempt_terminate(root: root, record: record, expected: generation_of(r: after_open), verdict: AttemptRecovered, detail: "the producer never launched") + let after_terminal = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let late_launch = attempt_begin_launch(root: root, record: record, expected: generation_of(r: after_open)) + let final_read = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + attempt_transition_advanced(t: opened) + && generation_of(r: after_open) == 1 + && state_word_of(r: after_open) == "reserved" + && attempt_transition_advanced(t: terminated) + && state_word_of(r: after_terminal) == "terminal:recovered" + && lost_race(t: late_launch) + && state_word_of(r: final_read) == "terminal:recovered" + && generation_of(r: final_read) == 2 +} + +// CRITERION 3, ORDER TWO: THE LAUNCH WINS AND RECOVERY IS REFUSED. +// +// The mirror, and it is the half that keeps the gate from being a one-way wall: a producer that HAS +// advanced to launching owns the attempt, and a recovery arriving afterwards must not be able to +// declare it terminal behind its back -- that is how a live unit's memory gets handed away. Same +// mechanism, opposite winner, and the loser is again refused by precondition rather than by +// noticing. +test fn a_launch_that_won_refuses_a_recovery_arriving_behind_it() -> Bool { + let root = fresh_root() as NonEmptyStr + let record = record_for(reference: "attempt-launch-first") + let opened = attempt_open(root: root, record: record) + let after_open = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let launched = attempt_begin_launch(root: root, record: record, expected: generation_of(r: after_open)) + let after_launch = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let late_recovery = attempt_terminate(root: root, record: record, expected: generation_of(r: after_open), verdict: AttemptRecovered, detail: "arrived after the launch") + let final_read = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + attempt_transition_advanced(t: opened) + && attempt_transition_advanced(t: launched) + && state_word_of(r: after_launch) == "launching" + && lost_race(t: late_recovery) + && state_word_of(r: final_read) == "launching" + && generation_of(r: final_read) == 2 +} + +// CRITERION 2: THE BINDING IS READ, NOT RECONSTRUCTED. The unit name recovery would act on comes +// out of the record the attempt wrote, and it survives the round trip through the store bytes. A +// recovery deriving the name from the identity would be a second authority for the binding, and a +// wrong derivation stops somebody else's unit. +test fn the_unit_binding_is_read_back_from_the_record_the_attempt_wrote() -> Bool { + let root = fresh_root() as NonEmptyStr + let record = record_for(reference: "attempt-binding") + let opened = attempt_open(root: root, record: record) + let read_back = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let recovered = held_record(r: read_back) + attempt_transition_advanced(t: opened) + && recovered.unit == record.unit + && recovered.identity == record.identity + && recovered.reference == record.reference + && kibibyte_count(k: recovered.granted) == 27262976 + && recovered.unit != record.identity +} + +// CRITERION 6: THE TERMINAL GENERATION CARRIES WHY, AND THE EARLIER GENERATIONS STILL EXIST. The +// store is generation-suffixed and append-only, so settling does not erase what it settled -- a +// reader can still see the attempt was reserved and launched before it ended. Recovery that +// overwrote its own evidence would be indistinguishable from an attempt that had never run. +test fn settling_records_why_and_does_not_erase_what_it_settled() -> Bool { + let root = fresh_root() as NonEmptyStr + let record = record_for(reference: "attempt-history") + let opened = attempt_open(root: root, record: record) + let g1 = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let launched = attempt_begin_launch(root: root, record: record, expected: generation_of(r: g1)) + let g2 = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let settled = attempt_terminate(root: root, record: record, expected: generation_of(r: g2), verdict: AttemptWorkEnded { ending: WorkEndedFailed }, detail: "unit terminated-failure, exit 101") + let g3 = attempt_slot_read(root: root, reference: record.reference as NonEmptyStr) + let terminal = held_record(r: g3) + attempt_transition_advanced(t: opened) && attempt_transition_advanced(t: launched) && attempt_transition_advanced(t: settled) + && generation_of(r: g1) == 1 && generation_of(r: g2) == 2 && generation_of(r: g3) == 3 + && (match terminal.state { AttemptTerminal { verdict: v, detail: d } => attempt_verdict_wire(v: v) == "failed" && string_contains(s: d, pattern: "exit 101") AttemptReserved => false AttemptLaunching => false }) + && Filesystem.Read(path: join([root as String, "/", record.reference, ".1"], "")).success + && Filesystem.Read(path: join([root as String, "/", record.reference, ".2"], "")).success + && string_contains(s: Filesystem.Read(path: join([root as String, "/", record.reference, ".1"], "")).content, pattern: "reserved") + && string_contains(s: Filesystem.Read(path: join([root as String, "/", record.reference, ".2"], "")).content, pattern: "launching") +} + +// CRITERION 1: FOUR STATES, AND THE TWO THAT MUST NEVER FREE CAPACITY ARE SEPARATE ARMS CARRYING +// WHY. Still-running and unknown are not one "not ended" bucket: one waits, the other is +// investigated, and a reader told only "could not establish" has nothing to act on. +test fn the_union_keeps_every_arm_either_list_carried_and_each_refuses_as_before() -> Bool { + unit_lifecycle_ended(u: UnitTerminatedSuccess { detail: "exit 0" }) + && unit_lifecycle_ended(u: UnitTerminatedFailure { detail: "exit 101" }) + && unit_lifecycle_ended(u: UnitTerminatedCauseUnknown { detail: "LoadState=not-found" }) + && !unit_lifecycle_ended(u: UnitStillRunning { detail: "populated 1" }) + && !unit_lifecycle_ended(u: UnitLifecycleUnknown { detail: "the manager could not be read" }) + && string_contains(s: unit_lifecycle_wire(u: UnitTerminatedCauseUnknown { detail: "LoadState=not-found" }), pattern: "cause unknown") + && string_contains(s: unit_lifecycle_wire(u: UnitStillRunning { detail: "populated 1" }), pattern: "STILL RUNNING") + && string_contains(s: unit_lifecycle_wire(u: UnitLifecycleUnknown { detail: "the manager could not be read" }), pattern: "the manager could not be read") +} + +// THE RECOVERY TRIGGER, AND THE ROW THAT MATTERS IS THE FIRST ONE. A producer that is alive and has +// simply not reached its launch CAS yet sits in Reserved -- indistinguishable by OBSERVATION from a +// dead one, because in Reserved there is no unit to observe. So recovery must not be able to enter +// the race at all inside the window the producer declared; the gate decides who wins a race, and +// this decides who may start one. Without it an impatient recovery kills a live attempt and the CAS +// makes that outcome look correct. +test fn recovery_cannot_fire_inside_the_window_the_producer_declared() -> Bool { + let record = record_for(reference: "attempt-trigger") + let unobservable = UnitLifecycleUnknown { detail: "no unit exists yet, which is what pre-launch looks like" } + let early = recovery_trigger(record: record, lifecycle: unobservable, now: 1999) + let at_deadline = recovery_trigger(record: record, lifecycle: unobservable, now: 2000) + let late = recovery_trigger(record: record, lifecycle: unobservable, now: 2001) + !recovery_trigger_fires(t: early) + && recovery_trigger_fires(t: at_deadline) + && recovery_trigger_fires(t: late) + && (match early { RecoveryTooEarly { deadline: d, now: n } => d == 2000 && n == 1999 _ => false }) + && string_contains(s: recovery_trigger_wire(t: early), pattern: "not dead") +} + +// AND ONCE LAUNCHED THE TRIGGER IS THE OBSERVATION, WITH CRITERION 4 IN FULL. Only the three ended +// arms may terminate a launched attempt; still-running and unknown keep the charge, and unknown is +// the one that matters because it is what a lost launcher, an unreadable manager and a missing +// cgroup all look like. +test fn a_launched_attempt_is_recovered_only_on_an_ended_unit() -> Bool { + let launched = AttemptRecord { + identity: "abcdef0123456789", reference: "attempt-launched", + unit: "gunbc-compute-abcdef0123456789-attempt-launched", granted: kibibyte(count: 27262976), + opened_at: 1800, launch_deadline: 2000, state: AttemptLaunching, + } + let terminal = AttemptRecord { + identity: "abcdef0123456789", reference: "attempt-done", + unit: "gunbc-compute-abcdef0123456789-attempt-done", granted: kibibyte(count: 27262976), + opened_at: 1800, launch_deadline: 2000, state: AttemptTerminal { verdict: AttemptWorkEnded { ending: WorkEndedSucceeded }, detail: "done" }, + } + recovery_trigger_fires(t: recovery_trigger(record: launched, lifecycle: UnitTerminatedSuccess { detail: "exit 0" }, now: 9999)) + && recovery_trigger_fires(t: recovery_trigger(record: launched, lifecycle: UnitTerminatedFailure { detail: "exit 101" }, now: 9999)) + && recovery_trigger_fires(t: recovery_trigger(record: launched, lifecycle: UnitTerminatedCauseUnknown { detail: "LoadState=not-found" }, now: 9999)) + && !recovery_trigger_fires(t: recovery_trigger(record: launched, lifecycle: UnitStillRunning { detail: "populated 1" }, now: 9999)) + && !recovery_trigger_fires(t: recovery_trigger(record: launched, lifecycle: UnitLifecycleUnknown { detail: "the manager could not be read" }, now: 9999)) + && !recovery_trigger_fires(t: recovery_trigger(record: terminal, lifecycle: UnitTerminatedSuccess { detail: "exit 0" }, now: 9999)) + && string_contains(s: recovery_trigger_wire(t: recovery_trigger(record: terminal, lifecycle: UnitTerminatedSuccess { detail: "exit 0" }, now: 9999)), pattern: "nothing to recover") +} + +// CRITERION 4: A SLOT THAT CANNOT BE READ IS NOT AN EMPTY SLOT. The distinction has opposite +// remedies and opposite hazards -- an unreadable slot read as absent lets a producer open a second +// attempt over a live one, and lets recovery believe there is nothing to terminate. +test fn an_undecodable_slot_is_unreadable_and_never_absent() -> Bool { + let root = fresh_root() as NonEmptyStr + let reference = "attempt-corrupt" + let planted = Filesystem.Write(path: join([root as String, "/", reference, ".1"], ""), content: "this is not a json document at all") + let reading = attempt_slot_read(root: root, reference: reference as NonEmptyStr) + let absent_reading = attempt_slot_read(root: root, reference: "attempt-never-written" as NonEmptyStr) + let negative_instant = attempt_record_decode(text: "{\"identity\":\"abcdef0123456789\",\"reference\":\"attempt-negative\",\"unit\":\"u\",\"granted_kib\":1,\"opened_at\":-5,\"launch_deadline\":100,\"state\":\"reserved\"}") + let negative_grant = attempt_record_decode(text: "{\"identity\":\"abcdef0123456789\",\"reference\":\"attempt-negative\",\"unit\":\"u\",\"granted_kib\":-1,\"opened_at\":5,\"launch_deadline\":100,\"state\":\"reserved\"}") + let well_formed = attempt_record_decode(text: "{\"identity\":\"abcdef0123456789\",\"reference\":\"attempt-fine\",\"unit\":\"u\",\"granted_kib\":1,\"opened_at\":5,\"launch_deadline\":100,\"state\":\"reserved\"}") + planted.success + && (match reading { AttemptSlotUnreadable { detail: d } => string_contains(s: d, pattern: "cannot decode") AttemptSlotHeld { record: _, generation: _ } => false AttemptSlotAbsent => false }) + && (match absent_reading { AttemptSlotAbsent => true AttemptSlotHeld { record: _, generation: _ } => false AttemptSlotUnreadable { detail: _ } => false }) + && (match negative_instant { Absent => true Present { value: _ } => false }) + && (match negative_grant { Absent => true Present { value: _ } => false }) + && (match well_formed { Present { value: r } => kibibyte_count(k: r.granted) == 1 && r.opened_at == 5 Absent => false }) +} + +fn terminal_record_text(verdict_word: String) -> String { + join(["{\"identity\":\"abcdef0123456789\",\"reference\":\"attempt-verdict\",\"unit\":\"u\",\"granted_kib\":1,\"opened_at\":5,\"launch_deadline\":100,\"state\":\"terminal:", verdict_word, "\",\"detail\":\"why\"}"], "") +} + +fn verdict_round_trips(v: AttemptVerdict) -> Bool { + let written = attempt_record_wire(r: AttemptRecord { + identity: "abcdef0123456789", reference: "attempt-verdict", unit: "u", granted: kibibyte(count: 1), + opened_at: 5, launch_deadline: 100, state: AttemptTerminal { verdict: v, detail: "why" }, + }) + match attempt_record_decode(text: written) { + Present { value: r } => + match r.state { + AttemptTerminal { verdict: back, detail: d } => attempt_verdict_wire(v: back) == attempt_verdict_wire(v: v) && d == "why" + AttemptReserved => false + AttemptLaunching => false + } + Absent => false + } +} + +// A TERMINAL VERDICT IS A CLOSED SET AND A WORD OUTSIDE IT IS UNREADABLE, like an unknown state word +// (review 70244). The positive half writes every verdict the two writers can produce through the +// real record wire and reads it back; the RED half hands the real decode a misspelling and the word +// this file itself used to write, "released", which no producer ever wrote -- both must come back +// unreadable rather than as a terminal state some later reader trusts. +test fn a_terminal_verdict_outside_the_closed_set_is_unreadable() -> Bool { + verdict_round_trips(v: AttemptRecovered) + && verdict_round_trips(v: AttemptWorkEnded { ending: WorkEndedSucceeded }) + && verdict_round_trips(v: AttemptWorkEnded { ending: WorkEndedFailed }) + && verdict_round_trips(v: AttemptWorkEnded { ending: WorkEndedRefusedByInfrastructure }) + && verdict_round_trips(v: AttemptWorkEnded { ending: WorkEndedCancelled }) + && verdict_round_trips(v: AttemptWorkEnded { ending: WorkEndedOutputMismatch }) + && (match attempt_record_decode(text: terminal_record_text(verdict_word: "recovered")) { Present { value: _ } => true Absent => false }) + && (match attempt_record_decode(text: terminal_record_text(verdict_word: "recoverd")) { Present { value: _ } => false Absent => true }) + && (match attempt_record_decode(text: terminal_record_text(verdict_word: "released")) { Present { value: _ } => false Absent => true }) + && (match attempt_record_decode(text: terminal_record_text(verdict_word: "")) { Present { value: _ } => false Absent => true }) +} + +// THE SELF-DECLARED BOUND HAS A BOUND, AND AN OVER-LONG DECLARATION REFUSES RATHER THAN BEING +// CLAMPED. The deadline is declared by the party it protects, so nothing in the gate alone stops a +// producer declaring an hour -- and the cost of that does not land on the producer, it lands on +// every other contender as a seat nobody may reclaim. That is DESIGN 5's externalization: an +// accepted risk re-exported to another principal while the contract keeps its name. +// +// CLAMPING WOULD BE THE WIDEN. Admitting the attempt under a bound it did not ask for, and then +// reclaiming its seat mid-checkout, is a safety limit's clothes on a silent narrowing of somebody +// else's window. It refuses, and the refusal names both numbers so the author learns the ceiling +// instead of meeting it as a mysterious reclaim. +test fn an_over_long_pre_launch_declaration_refuses_at_open_and_is_not_clamped() -> Bool { + let root = fresh_root() as NonEmptyStr + let base = record_for(reference: "attempt-greedy") + let greedy = AttemptRecord { + identity: base.identity, reference: base.reference, unit: base.unit, granted: base.granted, + opened_at: 1800, launch_deadline: 1800 + compute_pre_launch_ceiling_seconds + 1, state: AttemptReserved, + } + let at_ceiling = AttemptRecord { + identity: base.identity, reference: "attempt-at-ceiling", unit: base.unit, granted: base.granted, + opened_at: 1800, launch_deadline: 1800 + compute_pre_launch_ceiling_seconds, state: AttemptReserved, + } + let backwards = AttemptRecord { + identity: base.identity, reference: "attempt-backwards", unit: base.unit, granted: base.granted, + opened_at: 1800, launch_deadline: 1799, state: AttemptReserved, + } + let refused = attempt_open(root: root, record: greedy) + let admitted = attempt_open(root: root, record: at_ceiling) + let closed_window = attempt_open(root: root, record: backwards) + let greedy_slot = attempt_slot_read(root: root, reference: greedy.reference as NonEmptyStr) + !attempt_transition_advanced(t: refused) + && attempt_transition_advanced(t: admitted) + && !attempt_transition_advanced(t: closed_window) + && string_contains(s: attempt_transition_wire(t: refused), pattern: "every other contender") + && string_contains(s: attempt_transition_wire(t: refused), pattern: to_string(value: compute_pre_launch_ceiling_seconds)) + && string_contains(s: attempt_transition_wire(t: closed_window), pattern: "already closed") + && (match greedy_slot { AttemptSlotAbsent => true AttemptSlotHeld { record: _, generation: _ } => false AttemptSlotUnreadable { detail: _ } => false }) +} + + +// THE LOSER OF A LAUNCH RACE MAY NOT REPORT THAT IT SETTLED THE SLOT (review 69967). This is the +// reachable path: compute_run_leased returns its gate from compute_begin_launch, so a producer whose +// launch CAS lost carries AttemptGateRefused into compute_settle_attempt, and the string that fold +// produces is written into the operator-facing consumption receipt. Before the third arm existed the +// refusal mapped to HostRecordWritten and the receipt read `attempt: settled in the attempt slot` for +// a producer that settled nothing and observed nothing about the slot's final state. +// +// THE RACE IS REAL AND NOT DESCRIBED. Two producers open against one store; the winner advances the +// generation, so the loser's begin_launch is refused BY THE STORE. The claim then asserts three +// things that a two-armed carrier could not have kept apart: the winner says settled, the loser's +// wire denies it and says who to believe instead, and the loser is NOT reported as a host-record +// LOSS -- because it owed no record, and calling it a loss would manufacture an incident for an +// operator to chase. +fn layout_at(root: String) -> ComputeLayout { + ComputeLayout { + root: root, work_dir: root, checkout: root, out_dir: root, + leases_dir: root, lease_path: root, store_dir: root, target_dir: root, + log_path: root, outcome_path: root, consumption_path: root, + attempts_dir: root, + } +} + +test fn the_loser_of_a_launch_race_never_reports_that_it_settled_the_slot() -> Bool { + let root = fresh_root() + let layout = layout_at(root: root) + let rec = record_for(reference: "attempt-race") + let opened = attempt_open(root: root as NonEmptyStr, record: rec) + let generation = match opened { + AttemptAdvanced { state: _, generation: g } => g + AttemptLostRace { expected: _, observed: _ } => cas_generation_first() + AttemptTransitionRefused { detail: _ } => cas_generation_first() + } + let winner = compute_begin_launch(layout: layout, gate: AttemptGateReady { record: rec, generation: generation }) + let loser = compute_begin_launch(layout: layout, gate: AttemptGateReady { record: rec, generation: generation }) + let winner_settled = compute_settle_attempt(layout: layout, gate: winner, verdict: AttemptWorkEnded { ending: WorkEndedSucceeded }, detail: "the winner closes the slot") + let loser_settled = compute_settle_attempt(layout: layout, gate: loser, verdict: AttemptWorkEnded { ending: WorkEndedSucceeded }, detail: "the loser has no slot to close") + attempt_transition_advanced(t: opened) + && (match winner { AttemptGateReady { record: _, generation: _ } => true AttemptGateRefused { detail: _ } => false }) + && (match loser { AttemptGateReady { record: _, generation: _ } => false AttemptGateRefused { detail: _ } => true }) + && (match winner_settled { AttemptSettled => true AttemptNotSettled { detail: _ } => false AttemptUnsettleable { detail: _ } => false }) + && (match loser_settled { AttemptSettled => false AttemptNotSettled { detail: _ } => false AttemptUnsettleable { detail: _ } => true }) + && compute_attempt_settlement_wire(closed: winner_settled) == "settled in the attempt slot" + && !string_contains(s: compute_attempt_settlement_wire(closed: loser_settled), pattern: "settled in the attempt slot") + && string_contains(s: compute_attempt_settlement_wire(closed: loser_settled), pattern: "NOT SETTLED BY THIS PRODUCER") + && host_record_was_written(h: attempt_settlement_host_record(s: loser_settled)) +} diff --git a/dag/test/claim/compute/host_capacity_wet_witness_test.dag b/dag/test/claim/compute/host_capacity_wet_witness_test.dag index 0140266f9b2..45b15966a17 100644 --- a/dag/test/claim/compute/host_capacity_wet_witness_test.dag +++ b/dag/test/claim/compute/host_capacity_wet_witness_test.dag @@ -11,7 +11,7 @@ import gunbc.compute.host_capacity { compute_capacity_subject, compute_capacity_root, compute_memory_partition, HostMemoryObservation, HostMemoryObserved, HostMemoryUnobserved, observe_host_memory, ComputeReservation, ComputeReserved, ComputeCapacityFull, ComputeHostBelowFloor, ComputeReservationRefused, - compute_reserve_on, compute_reserve_against, compute_release, ComputeRelease, ComputeReleased, ComputeReleaseRefused, + compute_reserve_on, compute_reserve_against, compute_release, ComputeRelease, ComputeNothingToRelease, ComputeReleased, ComputeReleaseRefused, ComputeCapacityStanding, ComputeCapacityStandingRead, ComputeCapacityStandingUnread, compute_capacity_standing_on, } @@ -90,10 +90,27 @@ fn is_ledger_refusal(r: ComputeReservation) -> Bool { fn released(r: ComputeRelease) -> Bool { match r { ComputeReleased { partition: _, reference: _, reason: _ } => true + ComputeNothingToRelease { detail: _ } => false ComputeReleaseRefused { detail: _ } => false } } +fn nothing_to_release(r: ComputeRelease) -> Bool { + match r { + ComputeReleased { partition: _, reference: _, reason: _ } => false + ComputeNothingToRelease { detail: _ } => true + ComputeReleaseRefused { detail: _ } => false + } +} + +fn release_refused(r: ComputeRelease) -> Bool { + match r { + ComputeReleased { partition: _, reference: _, reason: _ } => false + ComputeNothingToRelease { detail: _ } => false + ComputeReleaseRefused { detail: _ } => true + } +} + fn standing_committed(s: ComputeCapacityStanding) -> Int { match s { ComputeCapacityStandingRead { committed: c, ceiling: _, headroom: _, observed_available: _, observed_total: _ } => kibibyte_count(k: c) @@ -248,3 +265,31 @@ test fn the_real_observation_reads_this_machine() -> Bool { } } +// A SECOND RELEASE OF ONE SEAT IS NOT A FAILED RELEASE, and before this arm existed it was reported +// as one. The producer and the recovery door both come back through compute_release, so the seat +// can be returned twice for one reference -- recovery wins past the deadline, returns the seat, and +// the producer reaches its own release afterwards. The pool then answers SeatNotHeld, which a +// CATCH-ALL arm folded into ComputeReleaseRefused: compute_release_landed went false, the record +// fold wrote outcome.json saying the seat was STILL CHARGED, and the stuck-reservation remedy was +// attached to a seat recovery had already returned. +// +// THIS DRIVES THE DOUBLE RELEASE FOR REAL rather than describing it: one reservation against a real +// event log in a temporary directory, released twice. The capacity reading after the second release +// is what rules out the opposite error -- an arm that reported success by releasing the seat AGAIN +// would show the committed figure moving, and it does not. +test fn releasing_one_seat_twice_is_not_a_ledger_failure_and_charges_nothing() -> Bool { + let subject = subject_at(root: fresh_root(), appropriation_kib: one_gibibyte_in_kibibytes * 2, request_kib: one_gibibyte_in_kibibytes) + let held = compute_reserve_on(subject: subject, reference: "wet-double" as NonEmptyStr, term_seconds: 60) + let while_held = compute_capacity_standing_on(subject: subject) + let first = compute_release(reservation: held, reason: "the producer finished" as NonEmptyStr) + let after_first = compute_capacity_standing_on(subject: subject) + let second = compute_release(reservation: held, reason: "recovery got here too" as NonEmptyStr) + let after_second = compute_capacity_standing_on(subject: subject) + reserved_amount(r: held) == one_gibibyte_in_kibibytes + && standing_committed(s: while_held) == one_gibibyte_in_kibibytes + && released(r: first) + && standing_committed(s: after_first) == 0 + && nothing_to_release(r: second) + && !release_refused(r: second) + && standing_committed(s: after_second) == 0 +} diff --git a/dag/test/claim/compute/manager_unaskable_wet_witness_test.dag b/dag/test/claim/compute/manager_unaskable_wet_witness_test.dag new file mode 100644 index 00000000000..bc67237a52a --- /dev/null +++ b/dag/test/claim/compute/manager_unaskable_wet_witness_test.dag @@ -0,0 +1,87 @@ +module test.claim.compute.manager_unaskable_wet_witness + +import extdeps.shell +import std.types { Bool, NonEmptyStr, String } +import gunbc.compute.attempt_lifecycle { UnitLifecycle, UnitTerminatedSuccess, UnitTerminatedFailure, UnitTerminatedCauseUnknown, UnitStillRunning, UnitLifecycleUnknown, unit_lifecycle_ended } +import gunbc.compute.work_provider_local { + UnitTermination, UnitAttemptCompleted, UnitAbsentAuthoritatively, UnitPopulated, UnitTerminationUnavailable, + observe_unit_termination, observe_unit_lifecycle, unit_termination_frees_capacity, compute_unit_name, + UnitPropertyReading, unit_property_from_shell, +} +import extdeps.transports.shell { ShellExited, ShellSpawnRefused } + +// A HOST WITH NO USER MANAGER TO ASK, and the arm the settlement and recovery routes reach there. +// The subject is the boundary between the shell transport and the two readings that consume the +// manager: a spawn that never produced a process must arrive at the fold as a property NOT QUERIED +// (extdeps.transports.shell ShellSpawnRefused, opted into by systemd.Systemctl ShowUserProperty), +// so the fold decides UNAVAILABLE and keeps the charge. Before that opt-in the same host ended the +// evaluation as a shell-spawn-refused runtime error before any fold ran -- which is what this +// witness's mutation control reproduces: remove the opt-in and this cell does not go red, it +// ABORTS, because the arm under test was never reachable. +// +// THE ARM IS OBSERVABLE ONLY WHERE systemctl IS ABSENT, and the claim says which host it is on +// rather than choosing one. It reads the host with an independent probe (shell.PosixCommandV +// Check, a different program) and asserts the relation: where systemctl is absent, both readings +// reach their unavailable arm and nothing frees; where it is present, the claim asserts only that +// the readings RETURNED -- the manager may answer not-found (a transient unit that never existed) +// or refuse the bus (a user with no session), and both are that host's honest answers, not this +// subject. So on the local-repo wet lane (srv1, systemctl present) this cell establishes only +// non-abort; the discriminating half executed on a host without systemctl is the exact-head +// receipt on the change that landed it. A lane without systemctl is the declared gap. +// +// THE UNIT NAME IS FOR AN IDENTITY NO PRODUCER MINTS (all-f), so on a host WITH a manager the +// reading is of a unit that does not exist and nothing is stopped or released. +data unaskable_identity: String = "ffffffffffffffff" + +fn manager_present() -> Bool { + shell.PosixCommandV.Check(command: "systemctl" as NonEmptyStr).exists +} + +fn termination_unavailable(t: UnitTermination) -> Bool { + match t { + UnitTerminationUnavailable { detail: d } => string_contains(s: d, pattern: "could not be queried") + UnitAttemptCompleted { detail: _ } => false + UnitAbsentAuthoritatively { detail: _ } => false + UnitPopulated { detail: _ } => false + } +} + +fn lifecycle_unknown(u: UnitLifecycle) -> Bool { + match u { + UnitLifecycleUnknown { detail: d } => string_contains(s: d, pattern: "could not be queried") + UnitTerminatedSuccess { detail: _ } => false + UnitTerminatedFailure { detail: _ } => false + UnitTerminatedCauseUnknown { detail: _ } => false + UnitStillRunning { detail: _ } => false + } +} + +// THE DISCRIMINATING HALF OF THIS SUBJECT LIVES IN test.claim.compute.work_request_witness, +// NOT HERE, and the reason is this file's own exclusion row. unit_property_from_shell is a pure +// fold, so a claim over it needs no host effect -- but this file is excluded from discovery +// (gunbc.ci.ci_layer_roots excl_manager_unaskable_reason), and an excluded file's identities are +// planned only on a run that CHANGES it. A hermetic claim placed here would execute on the change +// that wrote it and never again, which is the same decoration review 69970 found, one move along. +// So the fold's claim sits in the hermetic witness that is discovered every run, and what stays +// here is the half that genuinely needs the host: the inhabitance claim below. +// +// THE INHABITANCE HALF (DESIGN section 3, the pairing obligation). The claim above supplies the +// boundary's inputs, so something must still establish that the REAL producer emits that shape and +// that the real route runs. On a host WITH a manager this asserts the route reaches a RETURNED +// reading rather than aborting, which is the half the wet lane can honestly carry; on a host +// without one it asserts the unavailable arm end to end. Deleting the ShellOutcome opt-in makes +// this cell ABORT rather than answer, which is the control the file's header describes. +test fn a_host_without_a_user_manager_reaches_the_unavailable_arm_instead_of_aborting() -> Bool { + let present = manager_present() + let termination = observe_unit_termination(identity_hex: unaskable_identity, attempt_completed: false) + let lifecycle = observe_unit_lifecycle(unit: compute_unit_name(identity_hex: unaskable_identity)) + if present { + !unit_termination_frees_capacity(t: termination) + && !unit_lifecycle_ended(u: lifecycle) + } else { + termination_unavailable(t: termination) + && !unit_termination_frees_capacity(t: termination) + && lifecycle_unknown(u: lifecycle) + && !unit_lifecycle_ended(u: lifecycle) + } +} diff --git a/dag/test/claim/compute/work_request_witness_test.dag b/dag/test/claim/compute/work_request_witness_test.dag index c641d411fed..7b517964b66 100644 --- a/dag/test/claim/compute/work_request_witness_test.dag +++ b/dag/test/claim/compute/work_request_witness_test.dag @@ -10,7 +10,17 @@ import gunbc.compute.work_provider_local { provide_result_host_record, provide_result_ending, provide_result_document, host_record_was_written, host_record_wire, compute_with_lost_host_record, provide_result_with_host_record, host_record_join, ComputeLayout, compute_layout, compute_unit_properties, + LeaseDrop, LeaseDropped, LeaseNotDropped, compute_lease_drop_record, compute_stale_lease_note, + compute_stuck_reservation_remedy, + UnitLifecycleObservations, unit_lifecycle_decide, unit_population, + UnitPopulation, PopulationOccupied, PopulationEmpty, PopulationUnknown, compute_kill_mode_property, compute_kill_mode_value, + UnitPropertyReading, unit_property_from_shell, +} +import extdeps.transports.shell { ShellExited, ShellSpawnRefused } +import gunbc.compute.attempt_lifecycle { + UnitLifecycle, UnitTerminatedSuccess, UnitTerminatedFailure, UnitTerminatedCauseUnknown, + UnitStillRunning, UnitLifecycleUnknown, unit_lifecycle_ended, unit_lifecycle_wire, } import std.measure { kibibyte } import gunbc.roadmap_dashboard_instance { srv1_live_dashboard_instance } @@ -161,7 +171,7 @@ test fn the_attempt_completion_fact_is_not_the_works_ending() -> Bool { compute_attempt_completed(outcome: WorkSucceeded { identity: "a", outputs: [], log_path: "/l" }) && compute_attempt_completed(outcome: WorkOutputMismatch { identity: "a", detail: "d" }) && !compute_attempt_completed(outcome: WorkFailed { identity: "a", exit_code: 1, log_path: "/l" }) - && !compute_attempt_completed(outcome: WorkCancelled { identity: "a" }) + && !compute_attempt_completed(outcome: WorkCancelled { identity: "a", detail: "d" }) && !compute_attempt_completed(outcome: WorkRefusedByInfrastructure { identity: "a", cause: HostComputeCapacityFull { wire: "pool-full" } }) } @@ -183,8 +193,8 @@ test fn a_lost_host_record_changes_no_contract_the_next_caller_reads() -> Bool { let settled = ProvideFresh { outcome: succeeded, document: document, host_record: HostRecordWritten } let attached = ProvideAttached { identity: "abc", ending: "succeeded", document: document, host_record: HostRecordWritten } let layout = compute_layout(instance: srv1_live_dashboard_instance(), identity_hex: "abc") - let lost = compute_with_lost_host_record(settled: settled, layout: layout, dropped_ok: false, dropped_error: "EBUSY", error: "ENOSPC") - let lost_attached = compute_with_lost_host_record(settled: attached, layout: layout, dropped_ok: false, dropped_error: "EBUSY", error: "ENOSPC") + let lost = compute_with_lost_host_record(settled: settled, layout: layout, dropped: LeaseNotDropped { detail: "EBUSY" }, error: "ENOSPC") + let lost_attached = compute_with_lost_host_record(settled: attached, layout: layout, dropped: LeaseNotDropped { detail: "EBUSY" }, error: "ENOSPC") provide_result_ending(r: lost) == provide_result_ending(r: settled) && provide_result_document(r: lost) == provide_result_document(r: settled) && provide_result_ending(r: lost) == "succeeded" @@ -239,3 +249,161 @@ test fn a_lost_record_on_a_dependency_survives_a_successful_dependent() -> Bool && string_contains(s: host_record_wire(h: both_lost), pattern: "still held") && string_contains(s: host_record_wire(h: both_lost), pattern: "lost its reading") } + + +fn lifecycle_word(u: UnitLifecycle) -> String { + match u { + UnitTerminatedSuccess { detail: _ } => "terminated-success" + UnitTerminatedFailure { detail: _ } => "terminated-failure" + UnitTerminatedCauseUnknown { detail: _ } => "terminated-cause-unknown" + UnitStillRunning { detail: _ } => "still-running" + UnitLifecycleUnknown { detail: _ } => "unknown" + } +} + +data unqueried: UnitPropertyReading = UnitPropertyReading { queried: false, value: "" } + +fn lifecycle_of(load: UnitPropertyReading, active: UnitPropertyReading, result: UnitPropertyReading, pop: UnitPopulation) -> UnitLifecycle { + unit_lifecycle_decide(o: UnitLifecycleObservations { load_state: load, active_state: active, result: result, population: pop }) +} + +// CRITERION 1: FOUR STATES FROM THE MANAGER'S OWN VOCABULARY, AND UNKNOWN IS AN ARM. +// +// DISCRIMINATING IN FIVE DIRECTIONS AT ONCE, and the last two are the ones that fail open if the +// fold is wrong. An occupied cgroup must outrank LoadState=not-found -- the manager forgetting a +// unit while the kernel still holds processes in its cgroup is precisely the state where freeing +// the seat hands away live memory. And every reading that fails to ESTABLISH an end must answer +// unknown rather than picking the plausible neighbour: an inactive unit whose Result could not be +// read is not a success, and a unit whose Result came back empty is not a verdict. +// +// THE UNKNOWN ARMS ASSERT THEIR REASON RATHER THAN THEIR ARM. A negative control satisfied by any +// unknown would be satisfied by a fold that answered unknown to everything, so each one names the +// fact it could not establish (a refusal witness must assert the reason). +test fn the_lifecycle_verdict_has_four_states_and_unknown_carries_why() -> Bool { + let empty = PopulationEmpty { detail: "cg reports populated 0" } + let occupied = PopulationOccupied { detail: "processes remain in /user.slice/x" } + let unknown_pop = PopulationUnknown { detail: "the cgroup events could not be read" } + + let succeeded = lifecycle_of(load: reading(queried: true, value: "loaded"), active: reading(queried: true, value: "inactive"), result: reading(queried: true, value: "success"), pop: empty) + let failed = lifecycle_of(load: reading(queried: true, value: "loaded"), active: reading(queried: true, value: "failed"), result: reading(queried: true, value: "exit-code"), pop: empty) + let oom = lifecycle_of(load: reading(queried: true, value: "loaded"), active: reading(queried: true, value: "inactive"), result: reading(queried: true, value: "oom-kill"), pop: empty) + let running = lifecycle_of(load: reading(queried: true, value: "loaded"), active: reading(queried: true, value: "active"), result: reading(queried: true, value: "success"), pop: unknown_pop) + let collected = lifecycle_of(load: reading(queried: true, value: "not-found"), active: unqueried, result: unqueried, pop: unknown_pop) + + let occupied_but_forgotten = lifecycle_of(load: reading(queried: true, value: "not-found"), active: unqueried, result: unqueried, pop: occupied) + let no_manager = lifecycle_of(load: unqueried, active: unqueried, result: unqueried, pop: unknown_pop) + let result_unreadable = lifecycle_of(load: reading(queried: true, value: "loaded"), active: reading(queried: true, value: "inactive"), result: unqueried, pop: empty) + let result_empty = lifecycle_of(load: reading(queried: true, value: "loaded"), active: reading(queried: true, value: "inactive"), result: reading(queried: true, value: ""), pop: empty) + + lifecycle_word(u: succeeded) == "terminated-success" + && lifecycle_word(u: failed) == "terminated-failure" + && lifecycle_word(u: oom) == "terminated-failure" + && string_contains(s: unit_lifecycle_wire(u: oom), pattern: "oom-kill") + && lifecycle_word(u: running) == "still-running" + && lifecycle_word(u: collected) == "terminated-cause-unknown" + + && lifecycle_word(u: occupied_but_forgotten) == "still-running" + && lifecycle_word(u: no_manager) == "unknown" + && string_contains(s: unit_lifecycle_wire(u: no_manager), pattern: "load state") + && lifecycle_word(u: result_unreadable) == "unknown" + && string_contains(s: unit_lifecycle_wire(u: result_unreadable), pattern: "Result could not be read") + && lifecycle_word(u: result_empty) == "unknown" + && string_contains(s: unit_lifecycle_wire(u: result_empty), pattern: "not a verdict") + + && unit_lifecycle_ended(u: succeeded) + && unit_lifecycle_ended(u: failed) + && unit_lifecycle_ended(u: collected) + && !unit_lifecycle_ended(u: running) + && !unit_lifecycle_ended(u: occupied_but_forgotten) + && !unit_lifecycle_ended(u: no_manager) + && !unit_lifecycle_ended(u: result_unreadable) + && !unit_lifecycle_ended(u: result_empty) +} + + +// CRITERION 7: ONE CONTRACT FOR AN UNDROPPED LEASE, AND IT IS THE STORED RECORD THAT DECIDES. +// +// The state is: the work ran and its outcome was published, and the producer lease could not be +// removed. Three claims used to be made about it and they cannot all be true -- the caller was +// handed a refusal, the stored document said the run SUCCEEDED, and the note said the next request +// would refuse as ProducerInFlight. The stored record is exactly what the next caller attaches to, +// so it decides: the caller is told what the next caller will read, and the stale name is carried +// as the operational fact it is. +// +// DISCRIMINATING ON THE THREE WAYS THIS GOES WRONG, each of which has been written at least once +// in this change's history. (1) The undropped lease VANISHES -- LeaseNotDropped mapping to +// HostRecordWritten. (2) The undropped lease becomes a VERDICT -- the outcome or the document +// changing because a file could not be deleted. (3) The note tells the operator something the +// contract contradicts: it used to say THE NEXT REQUEST refuses as ProducerInFlight, which is +// false for a published success, because the attach is decided BEFORE the lease is consulted. The +// repair was to SCOPE that sentence, not to delete the word: the note still names ProducerInFlight +// as what a request that must PRODUCE again will meet, which is true. So the assertion here is on +// the two clauses that carry the scope -- a note that drops them and states the refusal +// unconditionally goes red, while the word itself is free to stay. +// +// AND THE REMEDY IS ASSERTED TO NAME A ROUTE THAT EXISTS. A refusal whose remedy names a +// capability nobody built decays into advice; this one names compute_recover_cli, and the +// assertion is here so that deleting the door makes this cell red rather than leaving the text +// pointing at nothing. +test fn an_undropped_lease_is_recorded_and_never_becomes_the_works_verdict() -> Bool { + let layout = compute_layout(instance: srv1_live_dashboard_instance(), identity_hex: "abc") + let succeeded = WorkSucceeded { identity: "abc", outputs: [], log_path: "/l" } + let document = work_outcome_wire(o: succeeded, subject: tree(hex: tree_a), op: work_default_build()) + let settled = ProvideFresh { outcome: succeeded, document: document, host_record: HostRecordWritten } + + let clean = compute_lease_drop_record(dropped: LeaseDropped, layout: layout) + let stuck = compute_lease_drop_record(dropped: LeaseNotDropped { detail: "EBUSY" }, layout: layout) + let carried = provide_result_with_host_record(r: settled, carried: stuck) + + host_record_was_written(h: clean) + && !host_record_was_written(h: stuck) + && string_contains(s: host_record_wire(h: stuck), pattern: "STALE PRODUCER LEASE") + && string_contains(s: host_record_wire(h: stuck), pattern: layout.lease_path) + && string_contains(s: host_record_wire(h: stuck), pattern: "EBUSY") + + && provide_result_ending(r: carried) == "succeeded" + && provide_result_document(r: carried) == document + && !host_record_was_written(h: provide_result_host_record(r: carried)) + + && string_contains(s: compute_stale_lease_note(layout: layout, error: "EBUSY"), pattern: "the attach is decided before this name is consulted") + && string_contains(s: compute_stale_lease_note(layout: layout, error: "EBUSY"), pattern: "matters only to a request that must PRODUCE again") + && string_contains(s: compute_stuck_reservation_remedy, pattern: "compute_recover_cli") +} + +// THE DISCRIMINATING HALF, AND IT RUNS EVERYWHERE (review 69970). The claim below used to be +// `if present { true }`, and the one lane it is enrolled on HAS a manager -- so on the only route +// that executes it, nothing could turn it red and the pre-change behaviour on that host was +// identical. DESIGN 4b: a check whose forbidden state cannot be expressed where the check runs is +// a decoration, permanently green by construction, and worse than absent because it is cited as +// coverage. The subject is the FOLD, which was fused to the effect and is now its own function, so +// both shell outcomes are authorable here and a host without systemctl is no longer required to +// observe the arm. +// +// THE RED THIS GOES TO: map ShellSpawnRefused to a queried reading, or delete the arm, and the +// first conjunct fails. That is the mapping the settlement and recovery routes depend on -- a +// refused spawn is NOT an answer, so it may not arrive as one. +// +// THE INPUT THAT ACTUALLY DISCRIMINATES, and the first attempt at this claim did not carry it. +// Supplying success: false and an empty value alongside the refusal makes the correct arm and a +// WRONG arm that reads the flag instead of the outcome produce the SAME reading, so the claim +// passed against a fold mutated to `ShellSpawnRefused => { queried: success, value: value }`. +// The fold's contract is that the OUTCOME decides: a spawn that produced no process is not a +// reading whatever the transport's other fields say, so the separating input is a refusal +// carrying a successful-looking flag and a value. +test fn a_refused_spawn_is_a_property_not_queried_and_never_a_reading() -> Bool { + let refused = unit_property_from_shell( + outcome: ShellSpawnRefused { program: "systemctl" as NonEmptyStr, cause: "No such file or directory" as NonEmptyStr }, + success: false, value: "") + let refused_with_a_flattering_flag = unit_property_from_shell( + outcome: ShellSpawnRefused { program: "systemctl" as NonEmptyStr, cause: "No such file or directory" as NonEmptyStr }, + success: true, value: "active") + let answered = unit_property_from_shell(outcome: ShellExited, success: true, value: "inactive") + let nonzero = unit_property_from_shell(outcome: ShellExited, success: false, value: "") + !refused.queried + && refused.value == "" + && !refused_with_a_flattering_flag.queried + && refused_with_a_flattering_flag.value == "" + && answered.queried + && answered.value == "inactive" + && !nonzero.queried +} diff --git a/src/v2/test/claim/local_repo_wet_terminal_test.dag b/src/v2/test/claim/local_repo_wet_terminal_test.dag index d52a40bed38..354338f43cc 100644 --- a/src/v2/test/claim/local_repo_wet_terminal_test.dag +++ b/src/v2/test/claim/local_repo_wet_terminal_test.dag @@ -3,7 +3,8 @@ module v2.test.claim.local_repo_wet_terminal_test import v2.std.collection { List } import v2.std.logic { Bool } import v2.std.text { String } -import v2.std.algebra { length, filter } +import v2.std.integer { Int } +import v2.std.algebra { length, filter, count_where } import v2.workflow.floor2_prepared_subject { WitnessIdentity, witness_identity_qualified_name } import v2.workflow.floor_terminal_ledger { ClaimAttemptTerminal, Returned, Panicked, RouteGap, @@ -126,6 +127,30 @@ fn terminal_matching() -> WetTerminalRow { ) } +// THE ROSTER-UNIQUENESS CLAIM BELONGS BESIDE THESE CLAIMS AND IS NOT LANDING IN THIS CHANGE, which is a +// deliberate call rather than an omission, recorded so the next reader does not rediscover the +// same wall and pay for it twice. +// +// WHAT IT GUARDS IS REAL AND NOTHING ELSE GUARDS IT. Two branches appending to this schedule +// conflict textually; the correct resolution is a union, which is right only when the appended +// rows are INDEPENDENT. A duplicated row survives that union silently, and the join cannot see +// it: wet_forward_causes walks SCHEDULED, so a row appearing twice finds the same single terminal +// twice, n == 1 both times, and no refusal is raised. The sibling claims cannot see it either -- +// every_roster_row_spells_its_function_the_same_way_twice reads WITHIN a row, and +// the_local_roster_is_not_empty compares length(identities) to length(schedule), which is a map +// and therefore equal over a roster WITH a duplicate in it. +// +// WHY IT IS NOT HERE: it costs 346735 eval steps against a 72300 new-witness budget, and the +// overage is the pairwise comparison itself. It is not made linear by any construction available +// -- the substrate offers no set and no sort over String -- so the honest routes are a declared +// ceiling or a reduced subject, and BOTH are decisions about a shared budget that belong to their +// own change rather than riding in on a compute-lifecycle PR that is already four rounds deep. +// +// ONE MEASUREMENT WORTH CARRYING, because it falsified the obvious repair: the first version +// rebuilt the roster projection inside the inner predicate, which looked like the cost. Hoisting +// it moved the figure from 343406 to 346735 -- the difference being one row the roster gained, not +// the repair. The rebuilt projection was never the expense. + // THE ROSTER DOES NOT LAND EMPTY. An empty roster would make this lane's coverage claim vacuously // true and leave nothing proving the executor runs anything at all -- permanently green by // construction, which DESIGN 4b calls a decoration rather than a wall. This is the witness that diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index 7a2c557a595..b68fef2e06f 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -1518,8 +1518,82 @@ fn floor_route_gap_expectation_chunk_21() -> List { } } +// test.claim.compute.attempt_lifecycle_wet_witness: these six reach shell.Mktemp.DirWithTemplate, +// which declares no mock_response, so the nominal floor refuses there and each identity is held. +// +// WHY THE ROSTER IS SIX AND NOT THE FILE'S NINE, which is the opposite of how the same file is +// enrolled on the wet lane and is not an inconsistency. An enrolled row whose identity does NOT gap +// is a STALE-ROUTE-GAP and refuses the run in the other direction, so this roster must name exactly +// the identities that gap -- it is an observation of one run, not a policy about a file. The wet +// schedule names all nine because it is a policy about an effect. The six are the ones the floor run +// on gunbc#12040 at 9d9f0747 reported, and a hermetic claim_batch over the same tree reported the +// same six; the CI run at the PREVIOUS head reported five, which is why the wet roster is not scoped +// this way. +// +// THE EXCLUSION ROW DOES NOT COVER THESE, and that is the fact that made the first remedy +// incomplete. gunbc.ci.ci_layer_roots excludes the file from DISCOVERY, which is what keeps the +// file's siblings off the nominal floor -- but a CHANGED witness is selected regardless of discovery +// exclusion, so a PR that edits this file plans its identities anyway. The exclusion holds for every +// run that does not touch the file, and this roster plus the wet terminal is what holds for the run +// that does. +// +// THE SEVENTH ROW IS the_loser_of_a_launch_race..., ADDED BY PREDICTION RATHER THAN BY OBSERVATION, +// which departs from this roster's own rule and is said rather than hidden. The six above were read +// off a floor run; this one was written after that run, so no run has reported it yet. Its first +// statement is `let root = fresh_root()`, which is DirWithTemplate unconditionally, so it cannot +// reach its subject hermetically under any evaluation order. If the floor disagrees it will say so +// as a STALE-ROUTE-GAP naming this identity -- the same self-correcting report the next paragraph +// describes -- and the alternative, leaving it out to be observed, spends a cycle learning what the +// call site already states. THE ROW IS ALSO WHY THIS ROSTER GREW: review 70036 found the claim +// enrolled NOWHERE, and it is the sole executing control for the AttemptUnsettleable arm, so the +// fabricated-settlement finding had been answered with a control that does not run. +// +// WHAT RE-OBSERVES THIS ROSTER, STATED BECAUSE NOTHING ELSE WOULD SAY IT. A six-row observation can +// go stale, and the staleness refuses from the other direction, so the obligation is named here +// rather than left for whoever meets the refusal. It is NARROWER than it first looks and the reason +// is the same exclusion: these identities are planned ONLY on a run that edits this file. An +// ordinary run never observes them, and an enrolled identity that does not execute does not red the +// floor -- the evidence is main itself, which carries ninety-nine wet-witness rows for files that +// are likewise discovery-excluded and is green. So this roster cannot rot quietly between heads. +// +// THE OBLIGATION IS THEREFORE ON THE NEXT CHANGE THAT TOUCHES THIS FILE, and it is one of two +// mechanical repairs, each named by the run that reports it: an identity that gaps and is not +// enrolled arrives as ROUTE-GAP and wants a row added; an identity enrolled here that reaches its +// verdict arrives as STALE-ROUTE-GAP and wants its row deleted. Both are the floor telling the +// author what the current subset is, which is the only authority for it -- the subset is a property +// of evaluation order, and the five-at-one-head against six-at-the-next measured on gunbc#12040 is +// what rules out predicting it. +fn floor_route_gap_expectation_chunk_22() -> List { + Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.a_launch_that_won_refuses_a_recovery_arriving_behind_it", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.a_terminal_transition_refuses_a_launch_that_had_not_spawned_yet", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.an_over_long_pre_launch_declaration_refuses_at_open_and_is_not_clamped", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.an_undecodable_slot_is_unreadable_and_never_absent", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.settling_records_why_and_does_not_erase_what_it_settled", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.the_unit_binding_is_read_back_from_the_record_the_attempt_wrote", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.attempt_lifecycle_wet_witness.the_loser_of_a_launch_race_never_reports_that_it_settled_the_slot", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Empty {} + } } } } } } } +} + +// test.claim.compute.manager_unaskable_wet_witness: its first shell operation on the hermetic route +// is the manager probe shell.PosixCommandV Check, which declares no mock_response, so the nominal +// floor refuses there and the identity is held; the local-repo wet schedule carries it. +fn floor_route_gap_expectation_chunk_23() -> List { + Cons { + head: FloorRouteGapExpectation { identity: "test.claim.compute.manager_unaskable_wet_witness.a_host_without_a_user_manager_reaches_the_unavailable_arm_instead_of_aborting", operation: "Check", ground: NoMockResponse {} }, + tail: Empty {} + } +} + fn floor_route_gap_expectation_chunks() -> List> { - Cons { head: floor_route_gap_expectation_chunk_00(), tail: Cons { head: floor_route_gap_expectation_chunk_01(), tail: Cons { head: floor_route_gap_expectation_chunk_02(), tail: Cons { head: floor_route_gap_expectation_chunk_03(), tail: Cons { head: floor_route_gap_expectation_chunk_04(), tail: Cons { head: floor_route_gap_expectation_chunk_05(), tail: Cons { head: floor_route_gap_expectation_chunk_06(), tail: Cons { head: floor_route_gap_expectation_chunk_07(), tail: Cons { head: floor_route_gap_expectation_chunk_08(), tail: Cons { head: floor_route_gap_expectation_chunk_09(), tail: Cons { head: floor_route_gap_expectation_chunk_10(), tail: Cons { head: floor_route_gap_expectation_chunk_11(), tail: Cons { head: floor_route_gap_expectation_chunk_12(), tail: Cons { head: floor_route_gap_expectation_chunk_13(), tail: Cons { head: floor_route_gap_expectation_chunk_14(), tail: Cons { head: floor_route_gap_expectation_chunk_15(), tail: Cons { head: floor_route_gap_expectation_chunk_16(), tail: Cons { head: floor_route_gap_expectation_chunk_17(), tail: Cons { head: floor_route_gap_expectation_chunk_18(), tail: Cons { head: floor_route_gap_expectation_chunk_19(), tail: Cons { head: floor_route_gap_expectation_chunk_20(), tail: Cons { head: floor_route_gap_expectation_chunk_21(), tail: Empty {} } } } } } } } } } } } } } } } } } } } } } } + Cons { head: floor_route_gap_expectation_chunk_00(), tail: Cons { head: floor_route_gap_expectation_chunk_01(), tail: Cons { head: floor_route_gap_expectation_chunk_02(), tail: Cons { head: floor_route_gap_expectation_chunk_03(), tail: Cons { head: floor_route_gap_expectation_chunk_04(), tail: Cons { head: floor_route_gap_expectation_chunk_05(), tail: Cons { head: floor_route_gap_expectation_chunk_06(), tail: Cons { head: floor_route_gap_expectation_chunk_07(), tail: Cons { head: floor_route_gap_expectation_chunk_08(), tail: Cons { head: floor_route_gap_expectation_chunk_09(), tail: Cons { head: floor_route_gap_expectation_chunk_10(), tail: Cons { head: floor_route_gap_expectation_chunk_11(), tail: Cons { head: floor_route_gap_expectation_chunk_12(), tail: Cons { head: floor_route_gap_expectation_chunk_13(), tail: Cons { head: floor_route_gap_expectation_chunk_14(), tail: Cons { head: floor_route_gap_expectation_chunk_15(), tail: Cons { head: floor_route_gap_expectation_chunk_16(), tail: Cons { head: floor_route_gap_expectation_chunk_17(), tail: Cons { head: floor_route_gap_expectation_chunk_18(), tail: Cons { head: floor_route_gap_expectation_chunk_19(), tail: Cons { head: floor_route_gap_expectation_chunk_20(), tail: Cons { head: floor_route_gap_expectation_chunk_21(), tail: Cons { head: floor_route_gap_expectation_chunk_22(), tail: Cons { head: floor_route_gap_expectation_chunk_23(), tail: Empty {} } } } } } } } } } } } } } } } } } } } } } } } } } fn floor_route_gap_expectations() -> List { diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index c59f66e7174..7db00b7ee15 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -242,6 +242,29 @@ fn local_repo_wet_requirement(candidate: String) -> WetEvidenceRequirement { // bin-witness wet class, whose standing excl_bin_wet_reason carries. Measured wet through // `gunbc run --claim-run` over this tree before enrollment: all ten held, and every metacharacter // probe failed without output rather than running its payload. +// THE ATTEMPT-LIFECYCLE MEMBERS ARE EVERY TEST FN IN THAT FILE (2026-09-22, gunbc#12040), and the +// membership is stated as that RULE rather than as a count. It said NINE until review 70036, by +// which time the file held ten: the claim added for the fabricated-settlement finding was written, +// executed by hand, and enrolled NOWHERE -- and it was the sole executing control for the +// AttemptUnsettleable arm, so the finding was answered with a control that does not run. A count +// asserting completeness over a population that grows underneath it is what hid that, which is the +// same defect in the other direction from the one this file's route-gap sibling avoids by being an +// observation rather than a policy. Here the policy is the honest form: the admitting property is +// the EFFECT, every function in the file has it, so no member can be added without being covered. +// +// Same admitted effect as the seven host_capacity members directly below, and enrolled the same way: a real compare-and-set against a +// real generation-file store inside a directory the witness creates with shell.Mktemp.DirWithTemplate +// and removes -- no repository, no network, no cargo, no remote host, no install media. The floor +// PLANNED all nine and the hermetic route reached no subject for most of them: the #12040 run named +// five (cause route_gap, 'the hermetic route has no arm for DirWithTemplate'), and a hermetic +// claim_batch over this tree ended six that way with three verdicts. A changed witness ending in a +// route gap is admitted only when a wet terminal joins it. The whole file is enrolled rather than +// the gapped subset, and the two measurements disagreeing on which subset is itself the reason: a +// claim reaches a verdict hermetically only by not touching the directory on that path, which is a +// property of the evaluation order and not of the claim, and it moves under an edit. The file's exclusion row is gunbc.ci.ci_layer_roots +// excl_local_repo_wet_tempdir_write_reason, and it retires on the same mock coverage as its +// neighbours. Measured wet over this tree before enrollment: every member held -- 9/9 at the time +// the first nine were enrolled, and the tenth PASS with its mutation RED when it was added. fn local_repo_wet_schedule() -> List { [ WetScheduledClaim { @@ -286,6 +309,84 @@ fn local_repo_wet_schedule() -> List { function: "two_instances_on_one_host_resolve_to_one_pool_at_one_root", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.manager_unaskable_wet_witness", function: "a_host_without_a_user_manager_reaches_the_unavailable_arm_instead_of_aborting" }, + entry: "dag/test/claim/compute/manager_unaskable_wet_witness_test.dag", + function: "a_host_without_a_user_manager_reaches_the_unavailable_arm_instead_of_aborting", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "releasing_one_seat_twice_is_not_a_ledger_failure_and_charges_nothing" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "releasing_one_seat_twice_is_not_a_ledger_failure_and_charges_nothing", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "a_terminal_transition_refuses_a_launch_that_had_not_spawned_yet" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "a_terminal_transition_refuses_a_launch_that_had_not_spawned_yet", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "a_launch_that_won_refuses_a_recovery_arriving_behind_it" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "a_launch_that_won_refuses_a_recovery_arriving_behind_it", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "the_unit_binding_is_read_back_from_the_record_the_attempt_wrote" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "the_unit_binding_is_read_back_from_the_record_the_attempt_wrote", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "settling_records_why_and_does_not_erase_what_it_settled" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "settling_records_why_and_does_not_erase_what_it_settled", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "the_union_keeps_every_arm_either_list_carried_and_each_refuses_as_before" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "the_union_keeps_every_arm_either_list_carried_and_each_refuses_as_before", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "recovery_cannot_fire_inside_the_window_the_producer_declared" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "recovery_cannot_fire_inside_the_window_the_producer_declared", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "a_launched_attempt_is_recovered_only_on_an_ended_unit" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "a_launched_attempt_is_recovered_only_on_an_ended_unit", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "an_undecodable_slot_is_unreadable_and_never_absent" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "an_undecodable_slot_is_unreadable_and_never_absent", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "a_terminal_verdict_outside_the_closed_set_is_unreadable" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "a_terminal_verdict_outside_the_closed_set_is_unreadable", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "an_over_long_pre_launch_declaration_refuses_at_open_and_is_not_clamped" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "an_over_long_pre_launch_declaration_refuses_at_open_and_is_not_clamped", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.attempt_lifecycle_wet_witness", function: "the_loser_of_a_launch_race_never_reports_that_it_settled_the_slot" }, + entry: "dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag", + function: "the_loser_of_a_launch_race_never_reports_that_it_settled_the_slot", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.effect_plan_bash_materialize_real_execution_witness", function: "effect_plan_bash_two_declared_operations_execute" }, entry: "dag/test/claim/effect_plan_bash_materialize_real_execution_witness_test.dag",