diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index f0516fd9..164ce4f8 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -133,6 +133,27 @@ repeated-contention variant, and a third static control failing an implementation that defers a skipped locator to a later cycle (F15). +Revision 8 (sol r7 residual F15): the one-cycle bound gains its +missing termination proof. §3.7 adds two liveness rules for the +locator lock: a declared finite HOLD DEADLINE, enforced with +session-level timeout mechanisms on every lock-holding path — a +live holder that stalls past the deadline is terminated, session +end releases the lock, and the stalled-holder schedule collapses +into the already-harmless crash window — and an arrival-order +GRANT rule, so a blocked waiter's wait is bounded by the current +holder and the waiters already ahead, never by later arrivals. +§4.5's blocking retry therefore terminates within a wall-clock +bound fixed when it starts waiting, and the implementing PR +derives and declares a maximum cycle duration whose exceedance is +surfaced as an error, never a silent hang. §7.10 adds the +hold-deadline control (a non-cooperating stalled holder is +terminated at the deadline and the orphan is still deleted before +cycle completion), the grant-order control (a stream of later +contenders cannot starve the queued repair, and the declared +cycle-duration limit is exercised as a checked bound), and a +fourth static control failing any lock-holding path without the +declared deadline (F15). + This contract binds the profile-category registry (§2), the custody placement rule (§3), the pointer schema (§4), the consent schema and its evaluation (§5), mode application (§6), witnesses (§7), and disclosed @@ -328,7 +349,27 @@ with contract 6 (`mode-conversion.md`), identity with slot) (e.g. a session-scoped `pg_advisory_lock` on a stable hash of the triple), held until step 2 commits or the writer's session ends (session end releases it automatically, so a crashed holder - never wedges the locator). Writers to one locator are therefore + never wedges the locator). Two liveness rules bound this + exclusion. **Hold deadline:** every session that acquires a + locator lock — ordinary writer, managed deleter (§4.7), + reconciliation repair (§4.5) — runs under a declared finite hold + deadline: the implementing PR declares the value and enforces it + with the database's session-level timeout mechanisms (statement + timeout and idle-in-transaction timeout, plus an application + deadline covering step 1's brain commit), so a holder that + stalls past the deadline has its session TERMINATED — session + end then releases the lock automatically per the rule above, and + the terminated holder's partial protocol is exactly the crash + window the tokens already make harmless (§4.5, §4.7). No holder + — live, stalled, or crashed — holds a locator lock longer than + the declared deadline. **Grant order:** conflicting waiters on + one locator lock are granted in arrival order — a requester that + starts waiting after another never acquires before it (the + queue-order grant of the pinned advisory-lock mechanism, + witnessed §7.10) — so a blocked waiter's wait is bounded by the + current holder's remaining deadline plus the deadline-bounded + holds of the waiters already ahead of it, never by later + arrivals. Writers to one locator are therefore totally ordered; writes to distinct locators do not contend. Because no two same-locator writes interleave, a completed write always leaves the pointer's `content_hash` describing the blob @@ -446,12 +487,23 @@ with contract 6 (`mode-conversion.md`), identity with in-scope pointer has been processed under its locator lock; deferral moves work to the end of the cycle, never into a later one, so the one-cycle bound above holds unconditionally on lock - contention. The blocking retry terminates: every §3.7 hold is - transaction- or session-scoped and session end releases the lock - automatically (§3.7), so no holder — live or crashed — can hold - a locator past its session; a cycle whose retry is still blocked - has not completed, and the orphan is deleted the moment the lock - becomes available, before the cycle reports completion. + contention. The blocking retry terminates within a WALL-CLOCK + BOUND, not merely eventually: every holder is subject to the + §3.7 hold deadline (a stalled live session is terminated at the + deadline and session end releases the lock — voluntary release + is not assumed), and grants follow §3.7 arrival order (no later + requester overtakes the queued retry), so once the retry blocks + it acquires within the current holder's remaining deadline plus + the deadline-bounded holds of the waiters already queued ahead — + a finite quantity fixed when the retry starts waiting, + independent of how many contenders arrive later. Cycle + completion is therefore itself bounded: the implementing PR + derives and declares a maximum cycle duration from the declared + hold deadline, the sweep scope, and the retry queue, and a cycle + exceeding its declared maximum is surfaced as an error — never a + silent hang. A cycle whose retry is still blocked has not + completed, and the orphan is deleted before the cycle reports + completion, within the declared bound. The repair DELETE is additionally token-conditioned like §4.7 step 2: it records the row's `id` and `generation` when it observes the content absent and conditions the DELETE on BOTH — @@ -891,7 +943,22 @@ declared profile table" means `profile_answers` (§3.5). releases and asserts the queued locator is retried until acquired — the orphan is still deleted by cycle completion once the last holder releases, never dropped after one failed - attempt. A + attempt. A **hold-deadline control** starts from a pre-existing + orphan, has a live holder acquire the orphan's locator lock and + stall past the declared §3.7 hold deadline WITHOUT ending its + session (idle transaction kept open), and asserts the holder's + session is terminated at the deadline, the lock releases + without any voluntary action by the holder, and the queued + blocking retry then deletes the orphan under the recorded + token before the cycle reports completion — proving termination + does not depend on a cooperative holder. A **grant-order + control** blocks the end-of-cycle retry behind a holder, keeps + a stream of later contenders requesting the same locator lock + while the retry waits, and asserts the retry acquires before + every later contender and the cycle completes within its + declared maximum duration — proving later arrivals cannot + starve the queued repair, and exercising the declared + cycle-duration limit as a checked bound rather than prose. A static control asserts the deletion implementation conditions on BOTH the recorded row `id` and `generation` — not on `content_hash` and not on `generation` alone — a second @@ -902,7 +969,11 @@ declared profile table" means `profile_answers` (§3.5). queues a failed try-acquire for a within-cycle blocking retry — an implementation that defers a skipped locator to a later cycle, or that reports cycle completion with a queued locator - unprocessed, FAILS. + unprocessed, FAILS. A fourth static control asserts every + lock-holding path (ordinary write §3.7, managed deletion §4.7, + reconciliation repair §4.5) is configured with the declared + §3.7 hold deadline — an implementation with any unbounded + lock-holding path FAILS. 11. **Default-deny and granularity witnesses:** an agent grantee with no active row is refused; with a `granted` row for category A only, category B is refused; with agent X granted, agent Y of the @@ -1082,9 +1153,12 @@ UPDATE` as the first statement of its transaction, and the ordinary writers, managed deletion, and reconciliation repair (try-acquire with the revision-7 within-cycle blocking retry, so a failed try-acquire defers repair to the end of the cycle, - never past it), so live interleavings between any two mutators - are excluded by one serialization protocol (§3.7, §4.5, §4.7, - §7.16). + never past it; per revision 8 every hold runs under a declared + finite hold deadline with arrival-order grants, so the deferred + repair — and with it cycle completion — is wall-clock bounded, + not merely eventual), so live interleavings between any two + mutators are excluded by one serialization protocol (§3.7, + §4.5, §4.7, §7.16). 17. The compare-and-delete managed-deletion step: deletion step 2 is conditioned on the PAIR of the target row's uuid `id` (the immutable row-incarnation identity) and its monotonic