diff --git a/dag/extdeps/realization/materialization_store_local.dag b/dag/extdeps/realization/materialization_store_local.dag index 9551444a2ec..69c9b474502 100644 --- a/dag/extdeps/realization/materialization_store_local.dag +++ b/dag/extdeps/realization/materialization_store_local.dag @@ -81,6 +81,7 @@ import gunbc.durable_cas_file_store { CasWindowReclamation, CasReclamationNotCommitted, CasAttemptAdmission, cas_window_generations, CasWindowGenerations, CasWindowGenerationsListed, CasWindowGenerationsUnlisted, cas_reclaim_below, CasGenerationWindow, + cas_verify_named_window_head, NamedWindowHeadCurrent, NamedWindowHeadMoved, } import std.durable_exclusive_hold { DurableHoldOwnerRef, DurableHoldReleaseRef, DurableHoldHolderReport, DurableHoldReleaseRefusal, DurableHoldRecoveryRefusal, @@ -91,10 +92,10 @@ import std.durable_exclusive_hold { import gunbc.durable_exclusive_hold_file_store { file_hold_acquire_windowed, FileHoldAcquireOutcome, FileHoldAcquired, FileHoldOccupied, FileHoldAcquireLost, FileHoldAcquireStoreUnavailable, FileHoldSlotUndecodable, FileHoldKeyNotSlotAddressable, - file_hold_release_assess_windowed, FileHoldReleasePlanned, FileHoldReleaseNotEligible, + file_hold_release_assess_windowed_at, FileHoldWindowedReleasePlanned, FileHoldWindowedReleaseNotEligible, FileHoldWindowedReleaseNamedHeadMoved, file_hold_release_commit, FileHoldReleased, FileHoldReleaseLost, FileHoldReleaseStoreUnavailable, FileHoldReleaseKeyNotSlotAddressable, - file_hold_recovery_assess_windowed, FileHoldRecoveryPlanned, FileHoldRecoveryNotEligible, - observe_file_hold_windowed, + file_hold_recovery_assess_windowed, FileHoldWindowedRecoveryPlanned, FileHoldWindowedRecoveryNotEligible, FileHoldWindowedRecoveryNamedHeadMoved, + hold_observation_of_cas, } import gunbc.process_hold_identity { process_hold_text, process_hold_marker, process_hold_decode, ProcessHoldHolder, @@ -907,6 +908,7 @@ type LocalStoreIndexRefusal | LocalStoreIndexContended { attempts: Int } | LocalStoreIndexUnsettled { settlement: LocalStoreSlotSettlement } | LocalStoreIndexHoldStale { observed: DurableHoldObservation } + | LocalStoreIndexHoldNamedWindowHeadMoved { named: CasGeneration } fn local_store_index_refusal_text(refusal: LocalStoreIndexRefusal) -> String { match refusal { @@ -927,6 +929,7 @@ fn local_store_index_refusal_text(refusal: LocalStoreIndexRefusal) -> String { LocalStoreIndexContended { attempts: n } => concat("the occupancy index kept moving under concurrent writers past the attempt bound: ", n as String) LocalStoreIndexUnsettled { settlement: st } => concat("the occupancy index cannot advance: ", local_store_settlement_text(s: st)) LocalStoreIndexHoldStale { observed: _ } => "the occupancy index write was attempted under a hold that is no longer live" + LocalStoreIndexHoldNamedWindowHeadMoved { named: _ } => "the occupancy index write was attempted after the named window head moved" } } @@ -974,6 +977,7 @@ fn local_store_write_index(held: LocalStoreFamilyHeld, expected: CasExpectation, { match local_store_hold_check(held: held) { LocalStoreHoldNotCurrent { observed: o } => LocalStoreIndexWriteRefused { refusal: LocalStoreIndexHoldStale { observed: o } } + LocalStoreHoldNamedWindowMoved { named: n } => LocalStoreIndexWriteRefused { refusal: LocalStoreIndexHoldNamedWindowHeadMoved { named: n } } LocalStoreHoldCurrent => local_store_write_index_current(held: held, expected: expected, index: index) } } @@ -1033,6 +1037,20 @@ fn local_store_write_index_settled(held: LocalStoreFamilyHeld, expected: CasExpe // on this host, and only a holder observed dead is recovered through file_hold_recovery_assess. An // unobservable holder stays held -- a family that cannot be shown free is not written. The hold slot // is windowed like the occupancy index (k = 2), so its bookkeeping does not grow with commits. +// +// HOLD CHECK AND RELEASE READ THE SLOT BY NAME. The windowed verify step is: generation G present +// and G+1 absent. LocalStoreFamilyHeld already names G, so those two reads are cas_file_slot_path +// Filesystem.Read -- O(1) in the number of objects in the store root. That two-read proof is sound +// only while a surviving eligible prefix cannot have holes: cas_reclaim_below deletes in generation +// order and stops at the first host refusal, so it cannot remove G+1 while G stays. A successor +// present still means the slot moved; an absent G is not this hold. Unknown-head observation +// (acquire, index) still lists, as DESIGN §3b states for a window whose generation is not named. +// +// ACQUIRE STILL LISTS. Windowed presence is not a prefix: generations at or below head-k are +// deleted, so a named gallop from generation 1 would read NotFound and treat a live head at 100 as +// an empty slot, then create-new generation 1 beside it. Listing the root to discover this key's +// generation files is the unknown-head observation cas_observe_window already uses. A held session +// pays that list once, not once per commit. data local_store_hold_owner_prefix: String = "materialization-store" @@ -1056,6 +1074,7 @@ type LocalStoreHoldRefusal | LocalStoreHoldWindowTooNarrow { k: Int } | LocalStoreHoldUnsettled { settlement: LocalStoreSlotSettlement } | LocalStoreHoldStale { observed: DurableHoldObservation } + | LocalStoreHoldNamedWindowHeadMoved { named: CasGeneration } | LocalStoreHoldWrongFamily { held: ArtifactKindId, requested: ArtifactKindId } fn local_store_hold_refusal_text(refusal: LocalStoreHoldRefusal) -> String { @@ -1071,6 +1090,7 @@ fn local_store_hold_refusal_text(refusal: LocalStoreHoldRefusal) -> String { LocalStoreHoldWindowTooNarrow { k: k } => concat("the family hold window is narrower than its floor: k = ", k as String) LocalStoreHoldUnsettled { settlement: st } => concat("the family hold slot cannot advance: ", local_store_settlement_text(s: st)) LocalStoreHoldStale { observed: _ } => "the hold this write was given is no longer the family's live hold" + LocalStoreHoldNamedWindowHeadMoved { named: _ } => "the named window head moved; this hold is no longer the family's live hold" LocalStoreHoldWrongFamily { held: h, requested: r } => concat(concat("the hold is for family ", h as String), concat(", the write is for ", r as String)) } } @@ -1163,8 +1183,9 @@ fn local_store_hold_occupied(binding: LocalStoreBinding, family: ArtifactKindId, LocalStoreHoldRefused { refusal: LocalStoreHoldContended } } else { match file_hold_recovery_assess_windowed(root: root_path as NonEmptyStr, slot_key: key, report: DurableHoldHolderReport { holder: holder, generation: generation, liveness: liveness }, released_by: local_store_hold_recovery_ref, window: window) { - FileHoldRecoveryNotEligible { slot_key: _, refusal: r } => LocalStoreHoldRefused { refusal: LocalStoreHoldRecoveryRefused { refusal: r } } - FileHoldRecoveryPlanned { plan: pl, dead_holder: _, evidence: _ } => + FileHoldWindowedRecoveryNotEligible { slot_key: _, refusal: r } => LocalStoreHoldRefused { refusal: LocalStoreHoldRecoveryRefused { refusal: r } } + FileHoldWindowedRecoveryNamedHeadMoved { slot_key: _, named: n } => LocalStoreHoldRefused { refusal: LocalStoreHoldNamedWindowHeadMoved { named: n } } + FileHoldWindowedRecoveryPlanned { plan: pl, dead_holder: _, evidence: _ } => match file_hold_release_commit(plan: pl) { FileHoldReleased { slot_key: _, generation: _ } => local_store_acquire_family_hold(binding: binding, family: family, recovered: true) FileHoldReleaseLost { slot_key: _ } => LocalStoreHoldRefused { refusal: LocalStoreHoldContended } @@ -1186,6 +1207,7 @@ fn local_store_hold_occupied(binding: LocalStoreBinding, family: ArtifactKindId, type LocalStoreHoldCheck = LocalStoreHoldCurrent | LocalStoreHoldNotCurrent { observed: DurableHoldObservation } + | LocalStoreHoldNamedWindowMoved { named: CasGeneration } fn local_store_hold_check(held: LocalStoreFamilyHeld) -> LocalStoreHoldCheck admit_callers: [ @@ -1196,10 +1218,25 @@ fn local_store_hold_check(held: LocalStoreFamilyHeld) -> LocalStoreHoldCheck decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_commit_verified"), ] { - let observed = observe_file_hold_windowed(root: materialization_store_root_path(root: held.binding.root) as NonEmptyStr, key: local_store_hold_key(family: held.family), window: held.window) + match cas_verify_named_window_head(root: materialization_store_root_path(root: held.binding.root) as NonEmptyStr, key: local_store_hold_key(family: held.family), generation: held.generation) { + NamedWindowHeadMoved { named_generation: n } => LocalStoreHoldNamedWindowMoved { named: n } + NamedWindowHeadCurrent { observation: o } => + local_store_hold_from_current_observation(held: held, observed: hold_observation_of_cas(observed: o)) + } +} + +fn local_store_hold_from_current_observation(held: LocalStoreFamilyHeld, observed: DurableHoldObservation) -> LocalStoreHoldCheck + admit_callers: [ + decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_hold_check"), + ] +{ match observed { - HoldSlotHeld { generation: g, owner: o } => - if cas_generation_count(g: g) == cas_generation_count(g: held.generation) && durable_hold_owner_equal(left: o, right: held.owner) { LocalStoreHoldCurrent } else { LocalStoreHoldNotCurrent { observed: observed } } + HoldSlotHeld { generation: g, owner: owner } => + if cas_generation_count(g: g) == cas_generation_count(g: held.generation) && durable_hold_owner_equal(left: owner, right: held.owner) { + LocalStoreHoldCurrent + } else { + LocalStoreHoldNotCurrent { observed: observed } + } HoldSlotAbsent => LocalStoreHoldNotCurrent { observed: observed } HoldSlotFree { generation: _, released_by: _ } => LocalStoreHoldNotCurrent { observed: observed } HoldSlotUndecodable { generation: _, detail: _ } => LocalStoreHoldNotCurrent { observed: observed } @@ -1223,6 +1260,7 @@ fn local_store_with_family_of(binding: LocalStoreBinding, family: ArtifactKin admit_callers: [ decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_with_family"), decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_record_recency"), + decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_held_session"), ] { match local_store_acquire_family_hold(binding: binding, family: family, recovered: false) { @@ -1234,11 +1272,36 @@ fn local_store_with_family_of(binding: LocalStoreBinding, family: ArtifactKin } } +// A HELD SESSION: acquire the family once, run many lookups and commits under LocalStoreFamilyHeld, +// release once. Distinct from local_store_commit, which still brackets every write; this operation +// does not change that signature. +// Consumed now by test.claim.materialization_store_local_wet_witness +// n_commits_under_one_held_session_acquire_the_hold_once_by_real_execution (inhabitance). +// Named later consumer: v2.compiler.compile, when its typecheck writes leave per-commit +// local_store_commit (the host typed_module_cache still does) and take one session around the +// family's writes; that change adds an admit_callers row here. Until then this is not a second +// name for local_store_with_family_of -- it is the sealed session operation. +// +// DEADLINE AND RENEWAL follow std.durable_exclusive_hold, not a clock. That protocol recovers a +// hold only when its holder is OBSERVED dead -- there is no timestamp, duration or silent expiry. +// This process is the holder (gunbc.process_hold_identity). Renewal is the named re-observation +// local_store_hold_check performs before every mutation: the slot must still be held at the +// generation and by the owner the session recorded, or the mutation refuses as stale. A session +// whose process has died is recovered by the next writer's liveness observation, never by age. +fn local_store_held_session(capability: LocalStoreCapability, family: ArtifactKindId, run: fn(LocalStoreFamilyHeld) -> T) -> LocalStoreBracket + admit_callers: [ + decl_ref(module_path: "test.claim.materialization_store_local_wet_witness", decl_name: "n_commits_under_one_held_session_acquire_the_hold_once_by_real_execution"), + ] +{ + local_store_with_family_of(binding: capability.binding, family: family, run: run) +} + // The release is reported, never fatal to the write it closes: a hold that could not be freed stays // held by this process, and once this process is gone the next writer recovers it by observation. type LocalStoreHoldRelease = LocalStoreHoldReleased | LocalStoreHoldReleaseNotEligible { refusal: DurableHoldReleaseRefusal } + | LocalStoreHoldReleaseNamedWindowHeadMoved { named: CasGeneration } | LocalStoreHoldReleaseLost | LocalStoreHoldReleaseStoreUnavailable { cause: CasStoreFailure } | LocalStoreHoldReleaseKeyNotAddressable @@ -1250,9 +1313,10 @@ fn local_store_release_family_hold(held: LocalStoreFamilyHeld) -> LocalStoreHold decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_acquire_all"), ] { - match file_hold_release_assess_windowed(root: materialization_store_root_path(root: held.binding.root) as NonEmptyStr, slot_key: local_store_hold_key(family: held.family), owner: held.owner, acquired_generation: held.generation, released_by: local_store_hold_release_ref, window: held.window) { - FileHoldReleaseNotEligible { slot_key: _, refusal: r } => LocalStoreHoldReleaseNotEligible { refusal: r } - FileHoldReleasePlanned { plan: pl } => + match file_hold_release_assess_windowed_at(root: materialization_store_root_path(root: held.binding.root) as NonEmptyStr, slot_key: local_store_hold_key(family: held.family), owner: held.owner, acquired_generation: held.generation, released_by: local_store_hold_release_ref, window: held.window) { + FileHoldWindowedReleaseNotEligible { slot_key: _, refusal: r } => LocalStoreHoldReleaseNotEligible { refusal: r } + FileHoldWindowedReleaseNamedHeadMoved { slot_key: _, named: n } => LocalStoreHoldReleaseNamedWindowHeadMoved { named: n } + FileHoldWindowedReleasePlanned { plan: pl } => match file_hold_release_commit(plan: pl) { FileHoldReleased { slot_key: _, generation: _ } => LocalStoreHoldReleased FileHoldReleaseLost { slot_key: _ } => LocalStoreHoldReleaseLost @@ -1644,6 +1708,7 @@ fn local_store_sweep_held(all: LocalStoreAllFamiliesHeld) -> LocalStoreSweep Absent => match local_store_hold_check(held: h) { LocalStoreHoldCurrent => none LocalStoreHoldNotCurrent { observed: o } => Present { value: LocalStoreSweepHoldRefused { family: h.family, refusal: LocalStoreHoldStale { observed: o }, released: [] } } + LocalStoreHoldNamedWindowMoved { named: n } => Present { value: LocalStoreSweepHoldRefused { family: h.family, refusal: LocalStoreHoldNamedWindowHeadMoved { named: n }, released: [] } } } }) match stale { @@ -1724,6 +1789,7 @@ fn local_store_record_recency_held(held: LocalStoreFamilyHeld, served: List LocalStoreRecencyHoldRefused { family: family, refusal: LocalStoreHoldStale { observed: o } } + LocalStoreHoldNamedWindowMoved { named: n } => LocalStoreRecencyHoldRefused { family: family, refusal: LocalStoreHoldNamedWindowHeadMoved { named: n } } LocalStoreHoldCurrent => local_store_record_recency_current(held: held, served: served) } } @@ -1984,6 +2050,7 @@ fn local_store_commit_verified( let root_path = materialization_store_root_path(root: root) match local_store_hold_check(held: held) { LocalStoreHoldNotCurrent { observed: o } => local_store_commit_hold_refused(key: key, refusal: LocalStoreHoldStale { observed: o }) + LocalStoreHoldNamedWindowMoved { named: n } => local_store_commit_hold_refused(key: key, refusal: LocalStoreHoldNamedWindowHeadMoved { named: n }) LocalStoreHoldCurrent => local_store_commit_refused(commit: store_commit_settle( store: held.binding.store, @@ -2250,6 +2317,7 @@ fn local_store_commit_under( } else { match local_store_hold_check(held: held) { LocalStoreHoldNotCurrent { observed: o } => local_store_commit_hold_refused(key: request_key(req: req), refusal: LocalStoreHoldStale { observed: o }) + LocalStoreHoldNamedWindowMoved { named: n } => local_store_commit_hold_refused(key: request_key(req: req), refusal: LocalStoreHoldNamedWindowHeadMoved { named: n }) LocalStoreHoldCurrent => { let staged = parts |> map(p => local_store_read_part(id: p.id, path: p.staged)) match local_store_first_unreadable(readings: staged) { diff --git a/dag/gunbc/ci/ci_layer_roots.dag b/dag/gunbc/ci/ci_layer_roots.dag index 78617e3ebb5..4fcef9efa6d 100644 --- a/dag/gunbc/ci/ci_layer_roots.dag +++ b/dag/gunbc/ci/ci_layer_roots.dag @@ -321,6 +321,10 @@ data excl_bin_wet_reason: String = "bin-execution witness class: fns run compile data excl_bin_wet_dissolve: DissolutionCondition = unbound_dissolution(description: "the file migrates under the execution-corpus scope prefix and enrolls as ExecutionWitnessKind rows in gunbc.commit_workflow; then this row and the roster entries delete (bin_witness_wet_note)") +data excl_immutable_pin_no_ci_wet_lane_reason: String = "ioctl-set IMMUTABLE leaked-hold composition (test.claim.materialization_store_local_immutable_pin_wet_witness): pin G, second acquire/release, reuse leaked G. Needs CAP_LINUX_IMMUTABLE. No required wet lane grants that cap, so the file is BinWitnessWet and named in gunbc.rung_drop.edited_bin_witness_wet_rows_not_executed_by_ci_population: a changed identity is DeclinedNoCiWetLane, not PlannedAsChangedWitness without a terminal. The executing floor wall for the no-hole reclaim half is reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution on the LocalRepoWetLane sibling file." + +data excl_immutable_pin_no_ci_wet_lane_dissolve: DissolutionCondition = unbound_dissolution(description: "a required wet lane grants CAP_LINUX_IMMUTABLE, or an unlink-refusal construction that needs none; then this file re-enrolls on local_repo_wet_schedule as ExpectedToHold, this exclusion flips to LocalRepoWetLane or deletes, and the pattern leaves edited_bin_witness_wet_rows_not_executed_by_ci_population") + data excl_run_verdict_exit_status_reason: String = "SUBSTANTIATED per-row (found 2026-08-16, PR #8286 CI red, run 31922786399, batch 3 discovery-corpus, 3 of 9782): every fn in this file invokes the compiled `gunbc` seed as a SUBPROCESS and reads the status of that process, so the hermetic envelope refuses them — 'no mock_response for operation Run' and 'for operation IsExecutable', the class excl_install_media_reason names. The refusal is correct and the file cannot be made hermetic: the subject IS the process exit status, which no in-process assertion can observe, and mocking the invocation would let the witness pass against a fabricated status — precisely the defect it exists to detect. The file was authored into dag/test/claim/ and so was swept into unshrunk hermetic discovery by path; the witnesses were right and the enrolment was wrong. Per DESIGN 'witness cost derives from purpose', this row alone would only remove them from hermetic discovery, which is NOT an executing consumer — so all three fns are ALSO enrolled in bin_witness_wet_entries below, which is their real per-PR executing consumer under WitnessHasExecutingConsumer standing. Size is derived, not chosen: three subprocess invocations of a three-constructor fixture, one per arm of the driver's verdict map." data excl_run_verdict_exit_status_dissolve: DissolutionCondition = unbound_dissolution(description: "the driver's exit-status seam becomes observable without a subprocess — i.e. the verdict boundary migrates under the execution-corpus scope prefix and enrolls as ExecutionWitnessKind rows in gunbc.commit_workflow, the same terminal excl_bin_wet_dissolve names; then this row and the three roster entries delete together. Publishing a mock_response for Run/IsExecutable does NOT discharge it: a mocked status is authored data, so the assertions would be re-checked against the fixture rather than against the seam, which is the vacuous pass this file's refusal-polarity note already records once.") @@ -1110,6 +1114,11 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_tempdir_write_reason, dissolution: excl_local_repo_wet_dissolve}, + WitnessExclusionRow { + pattern: "materialization_store_local_immutable_pin_wet_witness_test.dag", + classification: BinWitnessWet, + reason: excl_immutable_pin_no_ci_wet_lane_reason, + dissolution: excl_immutable_pin_no_ci_wet_lane_dissolve}, WitnessExclusionRow { pattern: "host_capacity_wet_witness_test.dag", classification: LocalRepoWetLane, @@ -1728,7 +1737,8 @@ data bin_witness_wet_entries: List = [ bin_wet(entry: "dag/test/claim/push_event_witness_wet_test.dag", f: "witness_push_before_payload_read_refused_on_missing_path"), bin_wet(entry: "dag/test/claim/host/host_cli_dependency_wet_witness_test.dag", f: "observe_echo_wet_posix_command_v_check_does_not_crash"), bin_wet(entry: "dag/test/claim/host/host_cli_dependency_wet_witness_test.dag", f: "observe_npm_wet_posix_command_v_check_does_not_crash"), - bin_wet(entry: "dag/test/claim/stage0_rust_maintenance_census_report_live_witness_test.dag", f: "maintenance_census_report_positive_control_derives_from_current_head") + bin_wet(entry: "dag/test/claim/stage0_rust_maintenance_census_report_live_witness_test.dag", f: "maintenance_census_report_positive_control_derives_from_current_head"), + bin_wet(entry: "dag/test/claim/materialization_store_local_immutable_pin_wet_witness_test.dag", f: "a_leaked_hold_stays_stale_when_reclaim_cannot_remove_its_generation_by_real_execution") ] data bin_witness_wet_per_row_wall_budget_seconds: Int = 60 diff --git a/dag/gunbc/durable_cas_file_store.dag b/dag/gunbc/durable_cas_file_store.dag index 29889384b6d..99b3ec830c2 100644 --- a/dag/gunbc/durable_cas_file_store.dag +++ b/dag/gunbc/durable_cas_file_store.dag @@ -5,7 +5,7 @@ import std.algebra { trim } import std.decimal { decimal_digits_only } import std.list { distinct_by_key } import std.content_hash { ContentHash, content_hash_of_value, compare_content_hash, ContentHashEqual, ContentHashDifferent, ContentHashCrossFamilyIncomparable } -import std.durable_compare_and_set { CasAttempt, cas_attempt, CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, CasGeneration, CasSlotVersion, CasReadableAbsent, CasReadablePresent, CasSlotObservation, CasObservedReadable, CasObservedUnreadable, CasUnreadableMalformed, CasUnreadableReadRefused, CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, cas_generation_exhausted, cas_generation_first, cas_generation_count, cas_generation_successor, CasSuccessorGeneration, CasSuccessorExhausted } +import std.durable_compare_and_set { CasAttempt, cas_attempt, CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, CasGeneration, CasSlotVersion, CasReadableAbsent, CasReadablePresent, CasSlotObservation, CasObservedReadable, CasObservedUnreadable, CasUnreadableMalformed, CasUnreadableReadRefused, CasUnreadableObservationBoundExceeded, CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, cas_generation_exhausted, cas_generation_first, cas_generation_count, cas_generation_successor, CasSuccessorGeneration, CasSuccessorExhausted } import std.checked_arithmetic { int_inclusive_max } import v2.std.algebra { skip } import extdeps.access.posix { FileMode, file_mode_bits } @@ -456,9 +456,6 @@ type CasSlotRetention = KeepAllGenerations | KeepGenerationWindow { window: CasGenerationWindow } -// A window read that keeps observing a moving head stops here and refuses with the attempt count. -data cas_window_observation_attempt_bound: Int = 8 - // "" -> the generation it names; none for anything else, for zero, and for a value past the // Int maximum. The multiplication is pre-checked (std.checked_arithmetic: check before, never after). fn cas_generation_of_digits(s: String) -> CasGeneration? { @@ -491,7 +488,7 @@ fn cas_key_generation_of_name(key: NonEmptyStr, name: String) -> CasGeneration? fn cas_window_generations(root: NonEmptyStr, key: NonEmptyStr) -> CasWindowGenerations admit_callers: [ decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_settle_slot"), - decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_observe_window"), + decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_observe_window_once"), decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_reclaim_below"), ] { @@ -516,37 +513,54 @@ fn cas_window_max_generation(generations: List) -> CasGeneration? }) } -fn cas_observe_window(root: NonEmptyStr, key: NonEmptyStr, attempt: Int) -> CasSlotProbe +// THE ONE AUTHORITY FOR THE WINDOWED OBSERVATION BOUND: the roster is the bound. Exhaustion +// reports CasUnreadableObservationBoundExceeded { bound: count(cas_window_observation_attempts) }. +data cas_window_observation_attempts: List = [1, 2, 3, 4, 5, 6, 7, 8] + +// ONE LIST-AND-VERIFY PASS. Recursion here was the unbounded arm: a window whose listed max is +// strictly below a generation that still reads present (stale listing, or a TCO lowering that does +// not increment `attempt`) re-entered cas_observe_window forever, re-reading G and G+1 with no +// further List. A fold over a finite attempt roster cannot fail to stop. +fn cas_observe_window_once(root: NonEmptyStr, key: NonEmptyStr) -> CasSlotProbe? admit_callers: [ - decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_observe_retained_slot"), decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_observe_window"), ] { - if attempt > cas_window_observation_attempt_bound { - ProbedWindowHeadUnsettled { attempts: cas_window_observation_attempt_bound } - } else { - match cas_window_generations(root: root, key: key) { - CasWindowGenerationsUnlisted { cause: c } => ProbedAbsenceUnestablished { cause: c } - CasWindowGenerationsListed { generations: gs } => - match cas_window_max_generation(generations: gs) { - Absent => ProbedAbsent - Present { value: head } => - match cas_read_generation(root: root, key: key, generation: head) { - GenerationRefused { probe: p } => p - GenerationAbsent => cas_observe_window(root: root, key: key, attempt: attempt + 1) - GenerationPresent { content: c } => - match cas_generation_successor(g: head) { - CasSuccessorExhausted { head: _ } => ProbedHead { generation: head, value: c } - CasSuccessorGeneration { generation: next } => - match cas_read_generation(root: root, key: key, generation: next) { - GenerationRefused { probe: p } => p - GenerationAbsent => ProbedHead { generation: head, value: c } - GenerationPresent { content: _ } => cas_observe_window(root: root, key: key, attempt: attempt + 1) - } - } - } - } - } + match cas_window_generations(root: root, key: key) { + CasWindowGenerationsUnlisted { cause: c } => Present { value: ProbedAbsenceUnestablished { cause: c } } + CasWindowGenerationsListed { generations: gs } => + match cas_window_max_generation(generations: gs) { + Absent => Present { value: ProbedAbsent } + Present { value: head } => + match cas_read_generation(root: root, key: key, generation: head) { + GenerationRefused { probe: p } => Present { value: p } + GenerationAbsent => none + GenerationPresent { content: c } => + match cas_generation_successor(g: head) { + CasSuccessorExhausted { head: _ } => Present { value: ProbedHead { generation: head, value: c } } + CasSuccessorGeneration { generation: next } => + match cas_read_generation(root: root, key: key, generation: next) { + GenerationRefused { probe: p } => Present { value: p } + GenerationAbsent => Present { value: ProbedHead { generation: head, value: c } } + GenerationPresent { content: _ } => none + } + } + } + } + } +} + +fn cas_observe_window(root: NonEmptyStr, key: NonEmptyStr) -> CasSlotProbe + admit_callers: [ + decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_observe_retained_slot"), + ] +{ + match fold(cas_window_observation_attempts, init: none, f: (acc, _) => match acc { + Present { value: p } => Present { value: p } + Absent => cas_observe_window_once(root: root, key: key) + }) { + Present { value: p } => p + Absent => ProbedWindowHeadUnsettled { attempts: count(cas_window_observation_attempts) } } } @@ -560,14 +574,12 @@ fn cas_observe_retained_slot(root: NonEmptyStr, key: NonEmptyStr, retention: Cas { match retention { KeepAllGenerations => cas_observe_slot(root: root, key: key) - KeepGenerationWindow { window: _ } => cas_observe_window(root: root, key: key, attempt: 1) + KeepGenerationWindow { window: _ } => cas_observe_window(root: root, key: key) } } fn cas_window_head_unsettled(attempts: Int) -> CasUnreadableSlot { - CasUnreadableReadRefused { - detail: concat(concat("the window head moved during ", attempts as String), " observations and was not settled; a head is never guessed") as NonEmptyStr - } + CasUnreadableObservationBoundExceeded { bound: attempts } } // THE PROJECTION TAKES A HEAD, NOT A PROBE, AND THE DELETED ARM IS THE REPAIR. @@ -677,11 +689,62 @@ fn observe_cas_slot_state_windowed(root: NonEmptyStr, key: NonEmptyStr, window: admit_callers: [ decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_read_index"), decl_ref(module_path: "test.claim.durable_cas_file_store_wet_witness", decl_name: "a_window_slot_holds_at_most_k_plus_one_generations_by_real_execution"), + decl_ref(module_path: "test.claim.durable_cas_file_store_wet_witness", decl_name: "a_window_observation_at_generation_1500_terminates_by_real_execution"), ] { observe_cas_slot_state_retained(root: root, key: key, retention: KeepGenerationWindow { window: window }) } +// A WINDOWED HEAD READ BY CONSTRUCTED NAME, NOT BY LISTING THE SLOT ROOT. +// +// cas_observe_window finds the head by listing every name under the store root and keeping this +// key's generation files. That is the correct discovery when the generation is unknown, because a +// windowed slot is NOT a presence prefix: generations at or below head-k are deleted, so galloping +// from generation 1 would read NotFound and report an empty slot while the live head sat at 100. +// Listing is therefore retained for unknown-head observation (cas_observe_window). +// +// When the caller already names the generation it believes is head -- a hold it just acquired, a +// release at the generation the protocol recorded -- the existing correctness argument does not +// need the listing. The windowed contract's verify step is: the named generation reads present and +// its successor reads absent. Those two reads are Filesystem.Read of cas_file_slot_path, O(1) in +// the store's object count. A successor that is present means the head moved; an absent named +// generation is not this head. The observation is never guessed. +// Realization-private: named verify is not CasSlotProbe and not DurableHoldObservation. G+1 present +// is a moved head, not eight-pass BoundExceeded. Consumers are the windowed hold check and the +// windowed release assessment; they match HeadMoved directly. +type CasNamedWindowVerify + = NamedWindowHeadCurrent { observation: CasSlotObservation } + | NamedWindowHeadMoved { named_generation: CasGeneration } + +fn cas_verify_named_window_head(root: NonEmptyStr, key: NonEmptyStr, generation: CasGeneration) -> CasNamedWindowVerify + admit_callers: [ + decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_hold_check"), + decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_release_assess_windowed_at"), + decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_recovery_assess_windowed"), + ] +{ + if !cas_key_is_slot_addressable(key: key) { + NamedWindowHeadCurrent { observation: CasObservedUnreadable { cause: CasUnreadableReadRefused { detail: cas_key_not_slot_addressable_detail } } } + } else { + match cas_read_generation(root: root, key: key, generation: generation) { + GenerationRefused { probe: p } => NamedWindowHeadCurrent { observation: cas_probe_as_observation(probe: p) } + GenerationAbsent => NamedWindowHeadCurrent { observation: cas_probe_as_observation(probe: ProbedAbsent) } + GenerationPresent { content: c } => + match cas_generation_successor(g: generation) { + CasSuccessorExhausted { head: _ } => + NamedWindowHeadCurrent { observation: cas_probe_as_observation(probe: ProbedHead { generation: generation, value: c }) } + CasSuccessorGeneration { generation: next } => + match cas_read_generation(root: root, key: key, generation: next) { + GenerationRefused { probe: p } => NamedWindowHeadCurrent { observation: cas_probe_as_observation(probe: p) } + GenerationAbsent => + NamedWindowHeadCurrent { observation: cas_probe_as_observation(probe: ProbedHead { generation: generation, value: c }) } + GenerationPresent { content: _ } => NamedWindowHeadMoved { named_generation: generation } + } + } + } + } +} + data cas_key_not_slot_addressable_detail: NonEmptyStr = "key is not slot-addressable: it carries a path separator" @@ -1035,23 +1098,42 @@ type CasFileWrite { reclamation: CasWindowReclamation } +type CasReclaimProgress { + removed: List + failed: List +} + +// ASCENDING, AND STOP AT THE FIRST HOST REFUSAL. Independent deletes of every generation at or +// below the floor could remove G+1 while G survived, which punches a hole: named window verify +// (G present and G+1 absent) would then report G as head while a later generation was live. +// One sort_by of the eligible set, then one walk that leaves every later generation in place when +// a delete fails, keeps that prefix contiguous without a min-and-filter per step. fn cas_reclaim_below(root: NonEmptyStr, key: NonEmptyStr, window: CasGenerationWindow, head: CasGeneration) -> CasWindowReclamation admit_callers: [ decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "file_compare_and_set_retained"), decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_settle_slot"), + decl_ref(module_path: "test.claim.durable_cas_file_store_wet_witness", decl_name: "reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution"), ] { match cas_window_generations(root: root, key: key) { CasWindowGenerationsUnlisted { cause: c } => CasReclamationUnlisted { cause: c } CasWindowGenerationsListed { generations: gs } => { let floor = cas_generation_count(g: head) - window.k - let attempts = gs |> filter(g => cas_generation_count(g: g) <= floor) |> map(g => { - let d = Filesystem.Delete(path: cas_file_slot_path(root: root, key: key, generation: g)) - CasGenerationDeleteAttempt { generation: g, success: d.success, error: d.error } - }) - let removed = attempts |> filter(t => t.success) |> map(t => t.generation) - let failed = attempts |> filter(t => !t.success) |> map(t => CasGenerationReclaimFailure { generation: t.generation, host_error: t.error }) - if count(failed) == 0 { CasReclaimed { removed: removed } } else { CasReclamationIncomplete { removed: removed, failed: failed } } + let ordered = gs |> filter(g => cas_generation_count(g: g) <= floor) |> sort_by(g => cas_generation_count(g: g)) + let walk = fold(ordered, init: CasReclaimProgress { removed: [], failed: [] }, f: (acc, g) => + if count(acc.failed) != 0 { acc } else { + let d = Filesystem.Delete(path: cas_file_slot_path(root: root, key: key, generation: g)) + if d.success { + CasReclaimProgress { removed: acc.removed |> list_push(g), failed: acc.failed } + } else { + CasReclaimProgress { + removed: acc.removed, + failed: [CasGenerationReclaimFailure { generation: g, host_error: d.error }], + } + } + } + ) + if count(walk.failed) == 0 { CasReclaimed { removed: walk.removed } } else { CasReclamationIncomplete { removed: walk.removed, failed: walk.failed } } } } } diff --git a/dag/gunbc/durable_exclusive_hold_file_store.dag b/dag/gunbc/durable_exclusive_hold_file_store.dag index fa5efa93c9d..1b1f6f35ba9 100644 --- a/dag/gunbc/durable_exclusive_hold_file_store.dag +++ b/dag/gunbc/durable_exclusive_hold_file_store.dag @@ -37,14 +37,16 @@ import std.durable_exclusive_hold { HoldSlotUndecodable, HoldObservationUnavailable, DurableHoldAcquireRefusal, HoldAcquireEligible, HoldAcquireRefused, HoldAcquireOccupied, HoldAcquireSlotUndecodable, HoldAcquireObservationUnavailable, - HoldReleaseEligible, HoldReleaseRefused, DurableHoldReleaseRefusal, + HoldReleaseEligible, HoldReleaseRefused, DurableHoldReleaseAssessment, DurableHoldReleaseRefusal, durable_hold_acquire_assess, durable_hold_release_assess, - DurableHoldHolderReport, DurableHoldRecoveryRefusal, HoldRecoveryEligible, HoldRecoveryRefused, + DurableHoldHolderReport, DurableHoldRecoveryRefusal, DurableHoldRecoveryAssessment, HoldRecoveryEligible, HoldRecoveryRefused, durable_hold_recovery_assess, } -import gunbc.durable_cas_file_store { KeepAllGenerations, CasSlotRetention, - DefaultAccessCreateOnly, DerivedPayloadAdmitted, DerivedPayloadKeyNotSlotAddressable, - admit_cas_attempt_for_derived_payload, file_compare_and_set, observe_cas_slot_state, +import gunbc.durable_cas_file_store { KeepAllGenerations, KeepGenerationWindow, CasSlotRetention, + CasGenerationWindow, DefaultAccessCreateOnly, DerivedPayloadAdmitted, DerivedPayloadKeyNotSlotAddressable, + admit_cas_attempt_for_derived_payload, file_compare_and_set, file_compare_and_set_retained, + observe_cas_slot_state, observe_cas_slot_state_retained, + cas_verify_named_window_head, CasNamedWindowVerify, NamedWindowHeadCurrent, NamedWindowHeadMoved, } // THE TAGS ARE NAMED ONCE AND THE BODY IS DERIVED FROM THE TAG THAT MATCHED. @@ -142,7 +144,6 @@ fn hold_observation_of_cas(observed: CasSlotObservation) -> Durable fn observe_file_hold_retained(root: NonEmptyStr, key: NonEmptyStr, retention: CasSlotRetention) -> DurableHoldObservation admit_callers: [ decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "observe_file_hold"), - decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "observe_file_hold_windowed"), decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_acquire_prepare_retained"), decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_release_assess_retained"), decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_recovery_assess_retained"), @@ -155,12 +156,54 @@ fn observe_file_hold(root: NonEmptyStr, key: NonEmptyStr) -> DurableHoldObservat observe_file_hold_retained(root: root, key: key, retention: KeepAllGenerations) } -fn observe_file_hold_windowed(root: NonEmptyStr, key: NonEmptyStr, window: CasGenerationWindow) -> DurableHoldObservation +// Named-window head movement is a file/window realization outcome, not a +// protocol refusal. Keep-all consumers of DurableHoldReleaseAssessment never +// see it; only windowed named verify mints these arms. +type WindowedHoldReleaseFromVerify + = WindowedHoldReleaseProtocol { assessment: DurableHoldReleaseAssessment } + | WindowedHoldReleaseNamedHeadMoved { named: CasGeneration } + +type WindowedHoldRecoveryFromVerify + = WindowedHoldRecoveryProtocol { assessment: DurableHoldRecoveryAssessment } + | WindowedHoldRecoveryNamedHeadMoved { named: CasGeneration } + +fn windowed_hold_release_from_verify( + verify: CasNamedWindowVerify, + owner: DurableHoldOwnerRef, + acquired_generation: CasGeneration, +) -> WindowedHoldReleaseFromVerify admit_callers: [ - decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_hold_check"), + decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_release_assess_windowed_at"), + decl_ref(module_path: "test.claim.durable_exclusive_hold_witness", decl_name: "named_window_head_moved_release_does_not_claim_an_observed_current_generation"), + ] +{ + match verify { + NamedWindowHeadMoved { named_generation: n } => + WindowedHoldReleaseNamedHeadMoved { named: n } + NamedWindowHeadCurrent { observation: o } => + WindowedHoldReleaseProtocol { + assessment: durable_hold_release_assess(observed: hold_observation_of_cas(observed: o), owner: owner, acquired_generation: acquired_generation), + } + } +} + +fn windowed_hold_recovery_from_verify( + verify: CasNamedWindowVerify, + report: DurableHoldHolderReport, +) -> WindowedHoldRecoveryFromVerify + admit_callers: [ + decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_recovery_assess_windowed"), + decl_ref(module_path: "test.claim.durable_exclusive_hold_witness", decl_name: "named_window_head_moved_recovery_does_not_claim_an_observed_current_generation"), ] { - observe_file_hold_retained(root: root, key: key, retention: KeepGenerationWindow { window: window }) + match verify { + NamedWindowHeadMoved { named_generation: n } => + WindowedHoldRecoveryNamedHeadMoved { named: n } + NamedWindowHeadCurrent { observation: o } => + WindowedHoldRecoveryProtocol { + assessment: durable_hold_recovery_assess(observed: hold_observation_of_cas(observed: o), report: report), + } + } } // EVERY EFFECTFUL HOLD WRITE IS LIVE READ -> SEALED PLAN -> CAS COMMIT, AND NO @@ -325,6 +368,11 @@ type FileHoldReleaseAssessment = FileHoldReleasePlanned { plan: FileHoldReleasePlan } | FileHoldReleaseNotEligible { slot_key: NonEmptyStr, refusal: DurableHoldReleaseRefusal } +type FileHoldWindowedReleaseAssessment + = FileHoldWindowedReleasePlanned { plan: FileHoldReleasePlan } + | FileHoldWindowedReleaseNotEligible { slot_key: NonEmptyStr, refusal: DurableHoldReleaseRefusal } + | FileHoldWindowedReleaseNamedHeadMoved { slot_key: NonEmptyStr, named: CasGeneration } + // THE ONLY MINT OF A RELEASE PLAN READS THE SLOT ITSELF. There is deliberately // no variant over a supplied observation: a synthetic "held by A at N" handed to // such a mint would produce a plan that frees a real hold of B's at N, and the @@ -340,7 +388,6 @@ fn file_hold_release_assess_retained( ) -> FileHoldReleaseAssessment admit_callers: [ decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_release_assess"), - decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_release_assess_windowed"), ] { match durable_hold_release_assess( @@ -367,12 +414,34 @@ fn file_hold_release_assess(root: NonEmptyStr, slot_key: NonEmptyStr, owner: Dur file_hold_release_assess_retained(root: root, slot_key: slot_key, owner: owner, acquired_generation: acquired_generation, released_by: released_by, retention: KeepAllGenerations) } -fn file_hold_release_assess_windowed(root: NonEmptyStr, slot_key: NonEmptyStr, owner: DurableHoldOwnerRef, acquired_generation: CasGeneration, released_by: DurableHoldReleaseRef, window: CasGenerationWindow) -> FileHoldReleaseAssessment +fn file_hold_release_assess_windowed_at(root: NonEmptyStr, slot_key: NonEmptyStr, owner: DurableHoldOwnerRef, acquired_generation: CasGeneration, released_by: DurableHoldReleaseRef, window: CasGenerationWindow) -> FileHoldWindowedReleaseAssessment admit_callers: [ decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_release_family_hold"), ] { - file_hold_release_assess_retained(root: root, slot_key: slot_key, owner: owner, acquired_generation: acquired_generation, released_by: released_by, retention: KeepGenerationWindow { window: window }) + match windowed_hold_release_from_verify( + verify: cas_verify_named_window_head(root: root, key: slot_key, generation: acquired_generation), + owner: owner, + acquired_generation: acquired_generation, + ) { + WindowedHoldReleaseNamedHeadMoved { named: n } => + FileHoldWindowedReleaseNamedHeadMoved { slot_key: slot_key, named: n } + WindowedHoldReleaseProtocol { assessment: a } => + match a { + HoldReleaseRefused { refusal: r } => FileHoldWindowedReleaseNotEligible { slot_key: slot_key, refusal: r } + HoldReleaseEligible { generation: g } => + FileHoldWindowedReleasePlanned { + plan: FileHoldReleasePlan { + root: root, + slot_key: slot_key, + owner: owner, + generation: g, + free_payload: hold_slot_payload(state: DurableHoldFree { released_by: released_by }), + retention: KeepGenerationWindow { window: window }, + }, + } + } + } } // The commit still tells a lost race from an unavailable store. A release @@ -416,6 +485,11 @@ type FileHoldRecoveryAssessment = FileHoldRecoveryPlanned { plan: FileHoldReleasePlan, dead_holder: DurableHoldOwnerRef, evidence: NonEmptyStr } | FileHoldRecoveryNotEligible { slot_key: NonEmptyStr, refusal: DurableHoldRecoveryRefusal } +type FileHoldWindowedRecoveryAssessment + = FileHoldWindowedRecoveryPlanned { plan: FileHoldReleasePlan, dead_holder: DurableHoldOwnerRef, evidence: NonEmptyStr } + | FileHoldWindowedRecoveryNotEligible { slot_key: NonEmptyStr, refusal: DurableHoldRecoveryRefusal } + | FileHoldWindowedRecoveryNamedHeadMoved { slot_key: NonEmptyStr, named: CasGeneration } + fn file_hold_recovery_assess_retained( root: NonEmptyStr, slot_key: NonEmptyStr, @@ -425,7 +499,6 @@ fn file_hold_recovery_assess_retained( ) -> FileHoldRecoveryAssessment admit_callers: [ decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_recovery_assess"), - decl_ref(module_path: "gunbc.durable_exclusive_hold_file_store", decl_name: "file_hold_recovery_assess_windowed"), ] { match durable_hold_recovery_assess(observed: observe_file_hold_retained(root: root, key: slot_key, retention: retention), report: report) { @@ -454,10 +527,33 @@ fn file_hold_recovery_assess(root: NonEmptyStr, slot_key: NonEmptyStr, report: D file_hold_recovery_assess_retained(root: root, slot_key: slot_key, report: report, released_by: released_by, retention: KeepAllGenerations) } -fn file_hold_recovery_assess_windowed(root: NonEmptyStr, slot_key: NonEmptyStr, report: DurableHoldHolderReport, released_by: DurableHoldReleaseRef, window: CasGenerationWindow) -> FileHoldRecoveryAssessment +fn file_hold_recovery_assess_windowed(root: NonEmptyStr, slot_key: NonEmptyStr, report: DurableHoldHolderReport, released_by: DurableHoldReleaseRef, window: CasGenerationWindow) -> FileHoldWindowedRecoveryAssessment admit_callers: [ decl_ref(module_path: "extdeps.realization.materialization_store_local", decl_name: "local_store_hold_occupied"), ] { - file_hold_recovery_assess_retained(root: root, slot_key: slot_key, report: report, released_by: released_by, retention: KeepGenerationWindow { window: window }) + match windowed_hold_recovery_from_verify( + verify: cas_verify_named_window_head(root: root, key: slot_key, generation: report.generation), + report: report, + ) { + WindowedHoldRecoveryNamedHeadMoved { named: n } => + FileHoldWindowedRecoveryNamedHeadMoved { slot_key: slot_key, named: n } + WindowedHoldRecoveryProtocol { assessment: a } => + match a { + HoldRecoveryRefused { refusal: r } => FileHoldWindowedRecoveryNotEligible { slot_key: slot_key, refusal: r } + HoldRecoveryEligible { generation: g, dead_holder: h, evidence: e } => + FileHoldWindowedRecoveryPlanned { + plan: FileHoldReleasePlan { + root: root, + slot_key: slot_key, + owner: h, + generation: g, + free_payload: hold_slot_payload(state: DurableHoldFree { released_by: released_by }), + retention: KeepGenerationWindow { window: window }, + }, + dead_holder: h, + evidence: e, + } + } + } } diff --git a/dag/gunbc/rung_drop/edited_bin_witness_wet_rows_not_executed_by_ci.dag b/dag/gunbc/rung_drop/edited_bin_witness_wet_rows_not_executed_by_ci.dag index cfdddbed893..0740a1bfcdf 100644 --- a/dag/gunbc/rung_drop/edited_bin_witness_wet_rows_not_executed_by_ci.dag +++ b/dag/gunbc/rung_drop/edited_bin_witness_wet_rows_not_executed_by_ci.dag @@ -69,6 +69,7 @@ data edited_bin_witness_wet_rows_not_executed_by_ci_population: List = [ "repo_local_git_config_real_execution_witness_test.dag", "transport_script_stdin_byte_fidelity_witness_test.dag", "push_event_witness_wet_test.dag", + "materialization_store_local_immutable_pin_wet_witness_test.dag", ] data edited_bin_witness_wet_rows_not_executed_by_ci: RungDrop = RungDrop { diff --git a/dag/std/durable_compare_and_set.dag b/dag/std/durable_compare_and_set.dag index 04e02b7ca70..ddf8da11619 100644 --- a/dag/std/durable_compare_and_set.dag +++ b/dag/std/durable_compare_and_set.dag @@ -129,10 +129,12 @@ type CasSlotObservation // // THE PLACEMENT WAS PUT TO REVIEW AND RULED ON, and the ruling also corrected the NAME, which is the // part worth keeping. The arm stays here: an interface outcome need not be producible by every -// realization, it needs a real producer and a stable caller-visible meaning, and a realization that -// must discover its head under a budget supplies both (gunbc.fabric.durable_cas_fabric_storage does; the -// file store no longer does, because its head search is total over the generation line). Moving it into the realization would either erase the typed remedy or force the whole -// store-failure carrier to become realization-specific. +// realization, it needs a real producer and a stable caller-visible meaning. Two producers supply +// both: gunbc.fabric.durable_cas_fabric_storage (generation-gallop budget) and +// gunbc.durable_cas_file_store cas_observe_window (windowed list-and-verify attempt roster). A +// named-generation verify that finds G+1 present is not this arm -- that is a moved head, not an +// exhausted observation budget. Moving BoundExceeded into a realization would either erase the +// typed remedy or force the whole store-failure carrier to become realization-specific. // // But the first spelling was `CasUnreadableBeyondProbeBound`, and PROBE IS THE FILE REALIZATION'S // DISCOVERY METHOD while EXHAUSTED OBSERVATION CAPACITY IS THE INTERFACE FACT. Naming the interface @@ -140,6 +142,10 @@ type CasSlotObservation // as an instruction to every other realization to describe itself in terms of scanning. What is NOT // claimed is that every CAS realization can produce this: most cannot, and one that never has to // discover a head should never construct it. +// `bound` is the exhausted observation-attempt budget (pass count), never a +// generation. A windowed list that ran eight verifies against a live head at +// generation 1500 reports bound 8. Rendering it as a generation is a meaning +// fork of the field and a fabricated diagnostic. type CasUnreadableSlot = CasUnreadableMalformed { detail: NonEmptyStr } | CasUnreadableContentMissing { referenced: ContentHash } @@ -155,7 +161,7 @@ fn cas_unreadable_slot_detail(cause: CasUnreadableSlot) -> String { CasUnreadableMalformed { detail: d } => concat("malformed: ", d as String) CasUnreadableContentMissing { referenced: h } => concat("content missing: ", serialize_content_hash(hash: h)) CasUnreadableReadRefused { detail: d } => concat("read refused: ", d as String) - CasUnreadableObservationBoundExceeded { bound: b } => concat("observation bound exceeded at generation ", to_string(b)) + CasUnreadableObservationBoundExceeded { bound: b } => concat("observation bound exceeded: ", to_string(b)) } } diff --git a/dag/test/claim/durable_cas_file_store_wet_witness_test.dag b/dag/test/claim/durable_cas_file_store_wet_witness_test.dag index b0e73e9924d..3a8ca38f843 100644 --- a/dag/test/claim/durable_cas_file_store_wet_witness_test.dag +++ b/dag/test/claim/durable_cas_file_store_wet_witness_test.dag @@ -9,6 +9,7 @@ import std.durable_compare_and_set { CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasReadableAbsent, CasReadablePresent, CasObservedReadable, CasObservedUnreadable, CasGenerationPublicationRefused, + CasGeneration, cas_generation_count, } import std.checked_arithmetic { int_inclusive_max } @@ -17,7 +18,8 @@ import gunbc.durable_cas_file_store { admit_cas_attempt, file_compare_and_set, DefaultAccessCreateOnly, observe_cas_slot_state, cas_file_slot_path, file_compare_and_set_windowed, observe_cas_slot_state_windowed, CasGenerationWindow, cas_generation_window, CasGenerationWindowAdmitted, CasGenerationWindowTooNarrow, - CasSlotProbe, ProbedHead, cas_probe_gallop, + CasSlotProbe, ProbedHead, cas_probe_gallop, cas_reclaim_below, + CasReclaimed, CasReclamationIncomplete, CasReclamationUnlisted, CasReclamationNotDeclared, CasReclamationNotCommitted, } // Wet controls for the file-backed CAS provider. Hermetic mint and classification @@ -291,6 +293,66 @@ test fn a_racing_writer_under_a_window_retries_and_loses_no_commit_by_real_execu && removed.success } +fn plant_generation(root: NonEmptyStr, key: NonEmptyStr, generation: CasGeneration, payload: String) -> Bool { + Filesystem.WriteCreateNew(path: cas_file_slot_path(root: root, key: key, generation: generation), content: payload).success +} + +// TERMINATION REGRESSION, NOT THE HANG'S RED. Measured against main's recursive +// cas_observe_window this two-file plant is GREEN (listed max 1501, successor 1502 absent, retry +// arm never runs): BuildBuddy invocation 492a33d7-ff9a-4fcf-8007-4fd7029aa139. It does not +// reproduce the production hang at hold-typed_module.1507/.1508. It asserts that a fold over eight +// cas_observe_window_once passes cannot fail to return. Persistent List-omits-true-max is a +// frontier measured by gunbc#13482 after this lands; ProbedWindowHeadUnsettled there is a counted +// store Unavailable, not a kill. +test fn a_window_observation_at_generation_1500_terminates_by_real_execution() -> Bool { + let root_path = fresh_root() + let root = root_path as NonEmptyStr + let w = window_of(k: 2) + let planted = plant_generation(root: root, key: "hold-typed_module", generation: 1500, payload: "g1500") + && plant_generation(root: root, key: "hold-typed_module", generation: 1501, payload: "g1501") + let observed = match w { + Absent => false + Present { value: win } => match observe_cas_slot_state_windowed(root: root, key: "hold-typed_module", window: win) { + CasObservedReadable { readable: r } => match r { + CasReadablePresent { version: v } => v.value == "g1501" && cas_generation_count(g: v.generation) == 1501 + CasReadableAbsent => false + } + CasObservedUnreadable { cause: _ } => true + } + } + let removed = shell.Remove.RecursiveForce(path: root_path) + planted && observed && removed.success +} + +// A DELETE THAT FAILS MUST NOT PUNCH A HOLE. Independent reclaim of every generation at or below +// the floor could remove G+1 while G stayed, so named window verify would report G as head. This +// plants G as a nonempty directory (unlink refuses) and G+1 as a file, then reclaims at head 4 +// with k=2. The later eligible generation must still read present. +test fn reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution() -> Bool { + let root_path = fresh_root() + let root = root_path as NonEmptyStr + let key = "hold-typed_module" as NonEmptyStr + let path1 = cas_file_slot_path(root: root, key: key, generation: 1) + let planted = shell.Mkdir.NewOwnerOnly(path: path1).success + && Filesystem.WriteCreateNew(path: concat(path1, "/stuck"), content: "x").success + && plant_generation(root: root, key: key, generation: 2, payload: "g2") + && plant_generation(root: root, key: key, generation: 3, payload: "g3") + && plant_generation(root: root, key: key, generation: 4, payload: "g4") + let reclaimed = match window_of(k: 2) { + Absent => false + Present { value: w } => match cas_reclaim_below(root: root, key: key, window: w, head: 4) { + CasReclamationIncomplete { removed: _, failed: f } => count(f) == 1 + CasReclaimed { removed: _ } => false + CasReclamationUnlisted { cause: _ } => false + CasReclamationNotDeclared => false + CasReclamationNotCommitted => false + } + } + let successor_still_there = Filesystem.Read(path: cas_file_slot_path(root: root, key: key, generation: 2)).success + let removed = shell.Remove.RecursiveForce(path: root_path) + planted && reclaimed && successor_still_there && removed.success +} + // The window's floor is construction: k < 2 has no admitted window. test fn a_window_narrower_than_two_is_not_admitted() -> Bool { match cas_generation_window(k: 1) { diff --git a/dag/test/claim/durable_compare_and_set_witness_test.dag b/dag/test/claim/durable_compare_and_set_witness_test.dag index 60709fa44d5..03178a6dba7 100644 --- a/dag/test/claim/durable_compare_and_set_witness_test.dag +++ b/dag/test/claim/durable_compare_and_set_witness_test.dag @@ -161,6 +161,8 @@ test fn an_unreadable_slot_is_a_store_refusal_not_a_lost_race() -> Bool { && is_store_refusal(outcome: missing) && is_store_refusal(outcome: refused) && is_store_refusal(outcome: beyond) + && cas_unreadable_slot_detail(cause: CasUnreadableObservationBoundExceeded { bound: 8 }) + == "observation bound exceeded: 8" } fn is_store_refusal(outcome: CasOutcome) -> Bool { diff --git a/dag/test/claim/durable_exclusive_hold_witness_test.dag b/dag/test/claim/durable_exclusive_hold_witness_test.dag index fc2efbd5b7f..58463c7747c 100644 --- a/dag/test/claim/durable_exclusive_hold_witness_test.dag +++ b/dag/test/claim/durable_exclusive_hold_witness_test.dag @@ -30,7 +30,11 @@ import std.durable_exclusive_hold { import gunbc.durable_exclusive_hold_file_store { HoldPayloadDecode, HoldPayloadDecoded, HoldPayloadUndecodable, hold_slot_payload, decode_hold_slot_payload, hold_observation_of_cas, + windowed_hold_release_from_verify, windowed_hold_recovery_from_verify, + WindowedHoldReleaseNamedHeadMoved, WindowedHoldReleaseProtocol, + WindowedHoldRecoveryNamedHeadMoved, WindowedHoldRecoveryProtocol, } +import gunbc.durable_cas_file_store { NamedWindowHeadMoved } // THE PURE HALF OF THE HOLD PROTOCOL AND ITS CODEC. Every row here decides // from a supplied observation over the PURE assessments; nothing reaches a @@ -367,3 +371,26 @@ test fn a_dead_verdict_recovers_only_the_hold_it_was_taken_of() -> Bool { _ => false }) } + +test fn named_window_head_moved_release_does_not_claim_an_observed_current_generation() -> Bool { + match windowed_hold_release_from_verify( + verify: NamedWindowHeadMoved { named_generation: 3 }, + owner: eh_owner(text: "demand-7|offer-1"), + acquired_generation: 3, + ) { + WindowedHoldReleaseNamedHeadMoved { named: n } => + cas_generation_count(g: n) == 3 + WindowedHoldReleaseProtocol { assessment: _ } => false + _ => false + } +} + +test fn named_window_head_moved_recovery_does_not_claim_an_observed_current_generation() -> Bool { + let dead = eh_report(holder: "mtcollins1-boot:4242", generation: 3, dead: 1) + match windowed_hold_recovery_from_verify(verify: NamedWindowHeadMoved { named_generation: 3 }, report: dead) { + WindowedHoldRecoveryNamedHeadMoved { named: n } => + cas_generation_count(g: n) == 3 + WindowedHoldRecoveryProtocol { assessment: _ } => false + _ => false + } +} diff --git a/dag/test/claim/materialization_store_local_immutable_pin_wet_witness_test.dag b/dag/test/claim/materialization_store_local_immutable_pin_wet_witness_test.dag new file mode 100644 index 00000000000..6940a163ce4 --- /dev/null +++ b/dag/test/claim/materialization_store_local_immutable_pin_wet_witness_test.dag @@ -0,0 +1,158 @@ +module test.claim.materialization_store_local_immutable_pin_wet_witness + +import extdeps.shell +import extdeps.filesystem.filesystem_io { Filesystem } +import std.types { Bool, List, String, NonEmptyStr } +import std.content_hash { Fnv1a64Structural, content_hash_atom } +import std.materialization_provider { + ArtifactRequest, NativeModuleVerdictBundleRequest, NativeModuleVerdictBundleSubject, + evaluation_store_address, evaluation_store_admitted_address, + output_module_test_verdicts, output_module_preparation_diagnostics, +} +import std.materialization_store_grant { MaterializationStoreRoot, WitnessScratchRoot } +import std.materialization_object { + ArtifactPayload, + StoreCommit, + store_object_name, + store_lookup_is_miss, + store_commit_refusal_tag, +} +import extdeps.realization.materialization_store_local { + LocalStoreCapability, + LocalStoreOpened, LocalStoreUnavailable, + LocalStoreInitialization, LocalStoreInitialized, LocalStoreInitializationRefused, + local_store_initialize, local_store_lookup, store_path, + LocalStoreFamilyBudget, + local_store_with_family, LocalStoreBracket, LocalStoreBracketRan, LocalStoreBracketRefused, local_store_commit_under, + LocalStoreHoldStale, LocalStoreHoldNamedWindowHeadMoved, LocalStoreHoldWrongFamily, + local_store_hold_key, + LocalStoreHoldRefusal, LocalStoreFamilyBusy, + LocalStoreHolderUnobservable, LocalStoreHoldRecoveryRefused, LocalStoreHoldContended, LocalStoreHoldStoreUnavailable, + LocalStoreHoldSlotUndecodable, LocalStoreHoldKeyNotAddressable, LocalStoreHoldSelfUnidentified, LocalStoreHoldWindowTooNarrow, LocalStoreHoldUnsettled, +} +import gunbc.durable_cas_file_store { cas_file_slot_path } +import std.cache_identity { native_module_verdict_bundle_artifact_kind, typed_module_artifact_kind } +import std.measure { byte_size } + +// PARTIAL RECLAIM MUST NOT RE-AUTHORIZE A LEAKED HOLD. Independent deletes could remove G+1 while +// G survived, so named verify would treat leaked G as head. Pin G against unlink, run another +// acquire/release (the reclaim that used to punch that hole), then reuse G. commit_under observes +// the hold first: named verify must answer NamedWindowHeadMoved (G present, G+1 still there). +// +// DECLARED NO-CI-WET-LANE DEBT. ioctl-set IMMUTABLE needs CAP_LINUX_IMMUTABLE; no required wet +// lane grants it. This file is BinWitnessWet in gunbc.ci_layer_roots and named in +// gunbc.rung_drop.edited_bin_witness_wet_rows_not_executed_by_ci_population, so a changed +// identity is DeclinedNoCiWetLane rather than PlannedAsChangedWitness without a terminal. +// Restoration: a wet lane that grants CAP_LINUX_IMMUTABLE, or an unlink-refusal construction +// that needs none. Floor wall for the invariant: +// reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution. +// Integration evidence (not CI): invocation bbdf835a-b6fa-4a51-a93b-26b140398306, FAIL then PASS +// with reclaim-stop reverted. + +data witness_family_budgets: List = [ + LocalStoreFamilyBudget { family: native_module_verdict_bundle_artifact_kind, budget: byte_size(count: 4096) }, + LocalStoreFamilyBudget { family: typed_module_artifact_kind, budget: byte_size(count: 4096) }, +] + +fn h(v: String) -> Fnv1a64Structural { + content_hash_atom(value: v as NonEmptyStr) +} + +fn bundle_req(module: String) -> ArtifactRequest { + NativeModuleVerdictBundleRequest(NativeModuleVerdictBundleSubject { + route_binary_identity: h(v: "route-binary-1"), + module_identity: h(v: module), + canonical_module_import_closure_identity: h(v: "closure-1"), + ordered_test_identity_population: h(v: "t1,t2"), + eval_interpretation_identity: h(v: "eval-1") + }) +} + +fn verdicts(text: String) -> List { + [ + ArtifactPayload { id: output_module_test_verdicts, content: text }, + ArtifactPayload { id: output_module_preparation_diagnostics, content: "" }, + ] +} + +fn object_path(root_path: String, req: ArtifactRequest) -> String { + match evaluation_store_admitted_address(admission: evaluation_store_address(req: req)) { + Absent => "" + Present { value: addr } => store_path(root_path: root_path, name: store_object_name(address: addr)) + } +} + +fn commit_tag(c: StoreCommit) -> String { + store_commit_refusal_tag(c: c) +} + +fn fresh_root_path() -> String { + shell.Mktemp.DirWithTemplate(template: "/tmp/gunbc_matstore.XXXXXX").path +} + +fn opened(root: MaterializationStoreRoot) -> LocalStoreCapability? { + match local_store_initialize(root: root, instance_label: "wet-witness", budgets: witness_family_budgets) { + LocalStoreInitialized { opening: o } => match o { + LocalStoreOpened { capability: c, durability: _ } => Present { value: c } + LocalStoreUnavailable { root_path: _, cause: _ } => none + } + LocalStoreInitializationRefused { root_path: _, cause: _ } => none + } +} + +fn hold_refusal_is_named_window_head_moved(r: LocalStoreHoldRefusal?) -> Bool { + match r { + Present { value: x } => match x { + LocalStoreHoldNamedWindowHeadMoved { named: _ } => true + LocalStoreHoldStale { observed: _ } => false + LocalStoreFamilyBusy { holder: _, evidence: _ } => false + LocalStoreHolderUnobservable { holder: _, cause: _ } => false + LocalStoreHoldRecoveryRefused { refusal: _ } => false + LocalStoreHoldContended => false + LocalStoreHoldStoreUnavailable { cause: _ } => false + LocalStoreHoldSlotUndecodable { detail: _ } => false + LocalStoreHoldKeyNotAddressable => false + LocalStoreHoldSelfUnidentified { cause: _ } => false + LocalStoreHoldWindowTooNarrow { k: _ } => false + LocalStoreHoldUnsettled { settlement: _ } => false + LocalStoreHoldWrongFamily { held: _, requested: _ } => false + } + Absent => false + } +} + +data pin_ext2_immutable_script: String = "import fcntl, os, struct, sys\nGET = 0x80086601\nSET = 0x40086602\nIMM = 0x10\npath = sys.argv[1]\non = sys.argv[2] == \"1\"\nfd = os.open(path, os.O_RDONLY)\ncur = struct.unpack(\"I\", fcntl.ioctl(fd, GET, struct.pack(\"I\", 0)))[0]\nfcntl.ioctl(fd, SET, struct.pack(\"I\", (cur | IMM) if on else (cur & ~IMM)))\nos.close(fd)\n" + +fn pin_generation_unlink(path: String, on: Bool) -> Bool { + shell.Exec.RunArgv(program: "python3", arguments: ["-c", pin_ext2_immutable_script, path, if on { "1" } else { "0" }]).exit_code == 0 +} + +test fn a_leaked_hold_stays_stale_when_reclaim_cannot_remove_its_generation_by_real_execution() -> Bool { + let root_path = fresh_root_path() + let root = WitnessScratchRoot { root: root_path } + let rs = bundle_req(module: "s") + let verdict = match opened(root: root) { + Absent => false + Present { value: store } => + match local_store_with_family(capability: store, of: rs, run: h => h) { + LocalStoreBracketRefused { refusal: _ } => false + LocalStoreBracketRan { value: leaked, hold_release: _ } => { + let pinned = cas_file_slot_path(root: root_path as NonEmptyStr, key: local_store_hold_key(family: leaked.family), generation: leaked.generation) + let immutable = pin_generation_unlink(path: pinned, on: true) + let advanced = match local_store_with_family(capability: store, of: rs, run: _ => true) { + LocalStoreBracketRefused { refusal: _ } => false + LocalStoreBracketRan { value: ok, hold_release: _ } => ok + } + let c = local_store_commit_under(held: leaked, req: rs, payloads: verdicts(text: "s pass"), parts: []) + let _unlock = pin_generation_unlink(path: pinned, on: false) + immutable && advanced + && commit_tag(c: c.commit) == "occupancy_unavailable" + && hold_refusal_is_named_window_head_moved(r: c.hold_refusal) + && !Filesystem.Read(path: object_path(root_path: root_path, req: rs)).success + && store_lookup_is_miss(l: local_store_lookup(capability: store, req: rs)) + } + } + } + let removed = shell.Remove.RecursiveForce(path: root_path) + verdict && removed.success +} diff --git a/dag/test/claim/materialization_store_local_seal_witness_test.dag b/dag/test/claim/materialization_store_local_seal_witness_test.dag index d8411bace7a..1ce58e244b0 100644 --- a/dag/test/claim/materialization_store_local_seal_witness_test.dag +++ b/dag/test/claim/materialization_store_local_seal_witness_test.dag @@ -142,3 +142,15 @@ test fn a_direct_raw_observe_call_is_an_admission_refusal() -> Bool { test fn a_direct_raw_reclaim_call_is_an_admission_refusal() -> Bool { admission_refusals(source: direct_raw_reclaim_source, callee: "cas_reclaim_below") == 1 } + +data direct_held_session_source: String = "module probe_direct_held_session\nimport std.cache_identity { ArtifactKindId }\nimport extdeps.realization.materialization_store_local { LocalStoreCapability, LocalStoreFamilyHeld, LocalStoreBracket, local_store_held_session }\nfn direct(c: LocalStoreCapability, f: ArtifactKindId) -> LocalStoreBracket {\n local_store_held_session(capability: c, family: f, run: h => h)\n}\n" + +data direct_named_window_observe_source: String = "module probe_direct_named_window_observe\nimport std.types { NonEmptyStr }\nimport std.durable_compare_and_set { CasGeneration }\nimport gunbc.durable_cas_file_store { cas_verify_named_window_head, CasNamedWindowVerify }\nfn direct(r: NonEmptyStr, k: NonEmptyStr, g: CasGeneration) -> CasNamedWindowVerify {\n cas_verify_named_window_head(root: r, key: k, generation: g)\n}\n" + +test fn a_direct_held_session_call_is_an_admission_refusal() -> Bool { + admission_refusals(source: direct_held_session_source, callee: "local_store_held_session") == 1 +} + +test fn a_direct_named_window_observe_call_is_an_admission_refusal() -> Bool { + admission_refusals(source: direct_named_window_observe_source, callee: "cas_verify_named_window_head") == 1 +} diff --git a/dag/test/claim/materialization_store_local_wet_witness_test.dag b/dag/test/claim/materialization_store_local_wet_witness_test.dag index 3390043414a..04c22fa8321 100644 --- a/dag/test/claim/materialization_store_local_wet_witness_test.dag +++ b/dag/test/claim/materialization_store_local_wet_witness_test.dag @@ -39,19 +39,21 @@ import extdeps.realization.materialization_store_local { local_store_record_recency, local_store_is_object_name, local_store_is_store_file_name, local_store_object_bytes, local_store_family_budget, LocalStoreFamilyBudget, local_store_budget_sum, LocalStoreRecencyHoldRefused, LocalStoreRecencyReceipt, - local_store_with_family, LocalStoreBracket, LocalStoreBracketRan, LocalStoreBracketRefused, local_store_commit_under, LocalStoreHoldStale, LocalStoreHoldWrongFamily, + local_store_with_family, LocalStoreBracket, LocalStoreBracketRan, LocalStoreBracketRefused, local_store_commit_under, local_store_held_session, LocalStoreHoldStale, LocalStoreHoldNamedWindowHeadMoved, LocalStoreHoldWrongFamily, local_store_hold_key, local_store_hold_owner_prefix, LocalStoreHoldAcquisition, LocalStoreHoldAcquired, LocalStoreHoldRefused, LocalStoreHoldRefusal, LocalStoreFamilyBusy, LocalStoreHolderUnobservable, LocalStoreHoldRecoveryRefused, LocalStoreHoldContended, LocalStoreHoldStoreUnavailable, LocalStoreHoldSlotUndecodable, LocalStoreHoldKeyNotAddressable, LocalStoreHoldSelfUnidentified, LocalStoreHoldWindowTooNarrow, LocalStoreHoldUnsettled, LocalStoreCatalogMismatch, LocalStoreCatalogInadmissible, LocalStoreSweepIncomplete, LocalStoreUnavailableCause, - local_store_index_window, + local_store_index_window, local_store_digits_int, LocalStoreRecordDeleteAttempt, LocalStoreRecordGone, LocalStoreRecordFileRefused, LocalStoreRecordPartsRefused, LocalStoreRecordPartsUnlisted, LocalStoreStagedPart, LocalStorePartsLookup, local_store_lookup_parts, local_store_part_name, } import gunbc.process_hold_identity { self_process_identity, SelfIdentified, SelfUnidentified, process_hold_text } import gunbc.build_cache_instance { ProcessIdentity } import gunbc.durable_exclusive_hold_file_store { file_hold_acquire_windowed, FileHoldAcquired, FileHoldOccupied, FileHoldAcquireLost, FileHoldAcquireStoreUnavailable, FileHoldSlotUndecodable, FileHoldKeyNotSlotAddressable } -import std.durable_exclusive_hold { DurableHoldOwnerRef } +import std.durable_exclusive_hold { + DurableHoldOwnerRef, +} import std.fabric_blob { fabric_blob_reading_path } import std.cache_identity { native_module_verdict_bundle_artifact_kind, typed_module_artifact_kind } import gunbc.materialization_store_budgets { @@ -627,6 +629,7 @@ fn hold_refusal_is_busy(r: LocalStoreHoldRefusal?) -> Bool { LocalStoreHoldWindowTooNarrow { k: _ } => false LocalStoreHoldUnsettled { settlement: _ } => false LocalStoreHoldStale { observed: _ } => false + LocalStoreHoldNamedWindowHeadMoved { named: _ } => false LocalStoreHoldWrongFamily { held: _, requested: _ } => false } Absent => false @@ -661,10 +664,11 @@ test fn a_commit_while_the_family_is_held_refuses_and_writes_nothing_by_real_exe verdict && removed.success } -fn hold_refusal_is_stale(r: LocalStoreHoldRefusal?) -> Bool { +fn hold_refusal_is_named_window_head_moved(r: LocalStoreHoldRefusal?) -> Bool { match r { Present { value: x } => match x { - LocalStoreHoldStale { observed: _ } => true + LocalStoreHoldNamedWindowHeadMoved { named: _ } => true + LocalStoreHoldStale { observed: _ } => false LocalStoreFamilyBusy { holder: _, evidence: _ } => false LocalStoreHolderUnobservable { holder: _, cause: _ } => false LocalStoreHoldRecoveryRefused { refusal: _ } => false @@ -682,8 +686,9 @@ fn hold_refusal_is_stale(r: LocalStoreHoldRefusal?) -> Bool { } // RELEASE-THEN-MUTATE REFUSES. A bracket body returns the held value it was given, so it outlives its -// release. Committing under that leaked value re-observes the family's hold slot, finds it no longer -// held at that generation by that owner, and refuses as a stale hold; nothing is written. +// release. Committing under that leaked value named-verifies G with G+1 present (the free successor +// the release published) and refuses as NamedWindowHeadMoved; nothing is written. The listing path +// used to decode the new free head as LocalStoreHoldStale; named verify does not observe that head. test fn a_hold_leaked_out_of_its_bracket_is_refused_as_stale_by_real_execution() -> Bool { let root_path = fresh_root_path() let root = WitnessScratchRoot { root: root_path } @@ -695,7 +700,7 @@ test fn a_hold_leaked_out_of_its_bracket_is_refused_as_stale_by_real_execution() LocalStoreBracketRan { value: leaked, hold_release: _ } => { let rs = bundle_req(module: "s") let c = local_store_commit_under(held: leaked, req: rs, payloads: verdicts(text: "s pass"), parts: []) - commit_tag(c: c.commit) == "occupancy_unavailable" && hold_refusal_is_stale(r: c.hold_refusal) + commit_tag(c: c.commit) == "occupancy_unavailable" && hold_refusal_is_named_window_head_moved(r: c.hold_refusal) && !Filesystem.Read(path: object_path(root_path: root_path, req: rs)).success && store_lookup_is_miss(l: local_store_lookup(capability: store, req: rs)) } @@ -1339,3 +1344,66 @@ test fn a_leftover_copy_that_cannot_be_removed_leaves_the_store_unwritable_by_re let removed = shell.Remove.RecursiveForce(path: root_path) verdict && removed.success } + +fn hold_slot_head_generation(root_path: String) -> Int { + let prefix = concat(local_store_hold_key(family: native_module_verdict_bundle_artifact_kind) as String, ".") + let listing = Filesystem.List(path: root_path) + match filesystem_listing_observation(directory: root_path, success: listing.success, entries: listing.entries, error: listing.error) { + FilesystemDirectoryListed(listed) => + fold(filesystem_listing_entry_names(listing: listed), init: 0, f: (best, n) => + if !starts_with(s: n, prefix: prefix) { best } else { + match local_store_digits_int(s: substring(s: n, start: string_length(s: prefix), end: string_length(s: n))) { + Absent => best + Present { value: g } => if g > best { g } else { best } + } + } + ) + FilesystemDirectoryListingRefused { directory: _, error: _ } => 0 + FilesystemDirectorySubjectRefused { directory: _, cause: _ } => 0 + } +} + +fn session_commit_ok(c: LocalStoreCommit) -> Bool { + commit_tag(c: c.commit) == "committed" +} + +// N COMMITS UNDER ONE SESSION ACQUIRE THE HOLD ONCE. Open already takes and releases the family +// hold (the sweep), so the discriminator is the DELTA after open: one session acquire+release +// advances the slot by 2; N per-commit brackets advance it by 2N. If the session were secretly +// the per-commit path, the two deltas would match and this claim would fail. Lookups run under +// the same session. This measures hold-acquire count, not root-List count: occupancy writes still +// list the store. +test fn n_commits_under_one_held_session_acquire_the_hold_once_by_real_execution() -> Bool { + let n = 6 + let session_root_path = fresh_root_path() + let bracket_root_path = fresh_root_path() + let session_root = WitnessScratchRoot { root: session_root_path } + let bracket_root = WitnessScratchRoot { root: bracket_root_path } + let session_ok = match opened(root: session_root) { + Absent => false + Present { value: store } => { + let before = hold_slot_head_generation(root_path: session_root_path) + match local_store_held_session(capability: store, family: native_module_verdict_bundle_artifact_kind, run: h => { + let writes = [1, 2, 3, 4, 5, 6] |> map(i => local_store_commit_under(held: h, req: bundle_req(module: concat("s", i as String)), payloads: verdicts(text: "s pass"), parts: [])) + let hits = [1, 2, 3, 4, 5, 6] |> map(i => store_lookup_is_hit(l: local_store_lookup(capability: store, req: bundle_req(module: concat("s", i as String))))) + writes |> all(c => session_commit_ok(c: c)) && hits |> all(x => x) + }) { + LocalStoreBracketRefused { refusal: _ } => false + LocalStoreBracketRan { value: body_ok, hold_release: _ } => + body_ok && (hold_slot_head_generation(root_path: session_root_path) - before) == 2 + } + } + } + let bracket_ok = match opened(root: bracket_root) { + Absent => false + Present { value: store } => { + let before = hold_slot_head_generation(root_path: bracket_root_path) + let writes = [1, 2, 3, 4, 5, 6] |> map(i => local_store_commit(capability: store, req: bundle_req(module: concat("b", i as String)), payloads: verdicts(text: "b pass"), parts: [])) + writes |> all(c => session_commit_ok(c: c)) && (hold_slot_head_generation(root_path: bracket_root_path) - before) == (2 * n) + } + } + let removed_s = shell.Remove.RecursiveForce(path: session_root_path) + let removed_b = shell.Remove.RecursiveForce(path: bracket_root_path) + session_ok && bracket_ok && removed_s.success && removed_b.success +} + diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 49916065be5..0ba3dbadb4e 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -112,7 +112,7 @@ Transitive determinism reachability over the fn-arrow call graph: RUNG DROP, mec ### an edited witness file classified BinWitnessWet in gunbc.ci_layer_roots witness_exclusion_frontier: the required floor's changed-witness sublane declines it as DeclinedNoCiWetLane instead of blocking, and no CI lane executes it — declared 2026-09-30 -an edited witness file classified BinWitnessWet in gunbc.ci_layer_roots witness_exclusion_frontier: the required floor's changed-witness sublane declines it as DeclinedNoCiWetLane instead of blocking, and no CI lane executes it: RUNG DROP, mechanically preventable -> mitigatable (lost as a passenger of the per-PR bin-witness wet batch, deleted with the floor cut of 2026-08-15, and .github/workflows/falsifier.yml, deleted at 611fd02770 (gunbc#8283)). Population: self_host_artifact_materialization_real_execution_witness_test.dag, stage0_regen_convergence_real_execution_witness_test.dag, typed_witness_invocation_test.dag, namespace_structural_root_exposure_generated_witness_test.dag, emit_host_typed_smoke_test.dag, build_artifact_corruption_probe_witness_test.dag, dag_collect_fingerprint_witness_test.dag, dag_compile_clean_perturb_receipts_test.dag, test/claim/diagnostics_test.dag, effects_rest_transport_parse_witness_test.dag, test/claim/parse_test.dag, v1_dag_parse_witness_test.dag, auth_declared_but_unwired_witness_test.dag, test/claim/bootstrap_test.dag, infer_semantics_witness_test.dag, dag_compile_clean_shard_a_witness_test.dag, dag_compile_clean_shard_totality_witness_test.dag, dag_compile_clean_seam_witness_test.dag, run_verdict_exit_status_witness_test.dag, http_client_get_real_execution_witness_test.dag, roadmap_belt_actuate_witness_test.dag, roadmap_closing_contract_execution_witness_test.dag, host_build_cache_provision_real_execution_witness_test.dag, materialized_ssh_key_file_real_execution_witness_test.dag, proc_self_cgroup_real_execution_witness_test.dag, repo_local_git_config_real_execution_witness_test.dag, transport_script_stdin_byte_fidelity_witness_test.dag, push_event_witness_wet_test.dag. Restored when: a REQUIRED lane executes changed BinWitnessWet rows for the same pull_request or merge_group -- builds their witness binaries and runs the edited entries to a terminal verdict on a host that admits their effects -- so the changed-witness sublane can plan them instead of declining; sufficient for deleting DeclinedNoCiWetLane and this row together. +an edited witness file classified BinWitnessWet in gunbc.ci_layer_roots witness_exclusion_frontier: the required floor's changed-witness sublane declines it as DeclinedNoCiWetLane instead of blocking, and no CI lane executes it: RUNG DROP, mechanically preventable -> mitigatable (lost as a passenger of the per-PR bin-witness wet batch, deleted with the floor cut of 2026-08-15, and .github/workflows/falsifier.yml, deleted at 611fd02770 (gunbc#8283)). Population: self_host_artifact_materialization_real_execution_witness_test.dag, stage0_regen_convergence_real_execution_witness_test.dag, typed_witness_invocation_test.dag, namespace_structural_root_exposure_generated_witness_test.dag, emit_host_typed_smoke_test.dag, build_artifact_corruption_probe_witness_test.dag, dag_collect_fingerprint_witness_test.dag, dag_compile_clean_perturb_receipts_test.dag, test/claim/diagnostics_test.dag, effects_rest_transport_parse_witness_test.dag, test/claim/parse_test.dag, v1_dag_parse_witness_test.dag, auth_declared_but_unwired_witness_test.dag, test/claim/bootstrap_test.dag, infer_semantics_witness_test.dag, dag_compile_clean_shard_a_witness_test.dag, dag_compile_clean_shard_totality_witness_test.dag, dag_compile_clean_seam_witness_test.dag, run_verdict_exit_status_witness_test.dag, http_client_get_real_execution_witness_test.dag, roadmap_belt_actuate_witness_test.dag, roadmap_closing_contract_execution_witness_test.dag, host_build_cache_provision_real_execution_witness_test.dag, materialized_ssh_key_file_real_execution_witness_test.dag, proc_self_cgroup_real_execution_witness_test.dag, repo_local_git_config_real_execution_witness_test.dag, transport_script_stdin_byte_fidelity_witness_test.dag, push_event_witness_wet_test.dag, materialization_store_local_immutable_pin_wet_witness_test.dag. Restored when: a REQUIRED lane executes changed BinWitnessWet rows for the same pull_request or merge_group -- builds their witness binaries and runs the edited entries to a terminal verdict on a host that admits their effects -- so the changed-witness sublane can plan them instead of declining; sufficient for deleting DeclinedNoCiWetLane and this row together. ### The EMIT-COST-QUAL-0 wet battery's only sanctioned executing consumer — declared 2026-09-04 diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index dbd2cd7655a..f36dbee41b0 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -1149,6 +1149,8 @@ fn floor_route_gap_expectation_chunk_09() -> List { head: FloorRouteGapExpectation { identity: "test.claim.materialization_store_local_wet_witness.a_refused_part_publish_leaves_no_temporary_copy_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.materialization_store_local_wet_witness.a_leftover_copy_that_cannot_be_removed_leaves_the_store_unwritable_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.materialization_store_local_wet_witness.n_commits_under_one_held_session_acquire_the_hold_once_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Empty {} } } @@ -1180,6 +1182,7 @@ fn floor_route_gap_expectation_chunk_09() -> List { } } } + } } } } @@ -1292,6 +1295,10 @@ fn floor_route_gap_expectation_chunk_12() -> List { tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.a_racing_writer_under_a_window_retries_and_loses_no_commit_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.a_window_observation_at_generation_1500_terminates_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.filesystem_link_create_new_wet_witness.a_link_publishes_the_source_bytes_and_keeps_the_source_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.filesystem_link_create_new_wet_witness.an_existing_target_refuses_as_occupied_and_is_unchanged_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, @@ -1307,6 +1314,8 @@ fn floor_route_gap_expectation_chunk_12() -> List { } } } + } + } } } } diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index 536251cec66..3c77955c0f6 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -1875,6 +1875,18 @@ fn local_repo_wet_schedule() -> List { function: "a_racing_writer_under_a_window_retries_and_loses_no_commit_by_real_execution", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.durable_cas_file_store_wet_witness", function: "a_window_observation_at_generation_1500_terminates_by_real_execution" }, + entry: "dag/test/claim/durable_cas_file_store_wet_witness_test.dag", + function: "a_window_observation_at_generation_1500_terminates_by_real_execution", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.durable_cas_file_store_wet_witness", function: "reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution" }, + entry: "dag/test/claim/durable_cas_file_store_wet_witness_test.dag", + function: "reclaim_stops_before_a_later_generation_when_an_earlier_delete_fails_by_real_execution", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.filesystem_link_create_new_wet_witness", function: "a_link_publishes_the_source_bytes_and_keeps_the_source_by_real_execution" }, entry: "dag/test/claim/filesystem_link_create_new_wet_witness_test.dag", @@ -2217,6 +2229,12 @@ fn local_repo_wet_schedule() -> List { function: "a_leftover_copy_that_cannot_be_removed_leaves_the_store_unwritable_by_real_execution", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.materialization_store_local_wet_witness", function: "n_commits_under_one_held_session_acquire_the_hold_once_by_real_execution" }, + entry: "dag/test/claim/materialization_store_local_wet_witness_test.dag", + function: "n_commits_under_one_held_session_acquire_the_hold_once_by_real_execution", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.pre_os_capture_replay_witness", function: "w_early_exit_refuses_absence_on_real_bytes" }, entry: "dag/test/claim/machine_intake/pre_os_capture_replay_witness_test.dag",