diff --git a/docs/requirements/custody-schema.md b/docs/requirements/custody-schema.md index ca9c8b36..f0516fd9 100644 --- a/docs/requirements/custody-schema.md +++ b/docs/requirements/custody-schema.md @@ -116,6 +116,23 @@ consent row's `id` and its `user_id`, so events from two subjects' grants to one ceasing grantee are attributable to their exact rows and subjects, witnessed with a two-subject case (F12). +Revision 7 (sol r6 F15): the reconciliation try-acquire no longer +discharges a locator for the cycle — a failed try-acquire QUEUES the +locator within the same cycle, and before the cycle completes the +sweep revisits every queued locator with a blocking acquire, running +the same locked observation and token-conditioned repair. A +triggered reconciliation cycle is complete only when every in-scope +pointer has been processed under its locator lock, so the §4.5 +one-cycle orphan bound holds unconditionally on lock contention; +the retry terminates because every §3.7 hold is transaction- or +session-scoped and session end releases the lock automatically. +§7.10 adds the lock-held contention control (sweep pass skips +without blocking; cycle completion waits for the queued repair; +the orphan is deleted before the cycle reports completion), its +repeated-contention variant, and a third static control failing an +implementation that defers a skipped locator to a later cycle +(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 @@ -417,10 +434,24 @@ with contract 6 (`mode-conversion.md`), identity with at most one cycle, and repair performs no database content write. Per-pointer repair runs under the §3.7 locator lock: before observing content absence for a pointer, reconciliation acquires - the pointer's locator lock (a try-acquire is permitted — a - locator whose lock is held is skipped and repaired on the next - cycle, so the sweep never blocks behind a writer), holds it - across the observation and the DELETE, and releases it after. + the pointer's locator lock, holds it across the observation and + the DELETE, and releases it after. The sweep pass MAY use a + try-acquire so it never blocks mid-pass behind a writer, but a + failed try-acquire defers the locator, never discharges it: the + skipped locator is queued within the SAME cycle, and before the + cycle completes the sweep revisits every queued locator with a + blocking acquire and runs the same locked observation and + token-conditioned repair, retrying until the lock is acquired. A + triggered reconciliation cycle is COMPLETE only when every + 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. 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 — @@ -845,13 +876,33 @@ declared profile table" means `profile_answers` (§3.5). observation and content removal inside the writer's step-1-to-step-2 gap and asserts the witness DETECTS the resulting acknowledged-write loss, establishing that the lock is - what excludes it. A + what excludes it. **Lock-held contention control (one-cycle + bound):** starting from a PRE-EXISTING orphan, a §3.7 writer + session holds the orphan's locator lock while the triggered + reconciliation's sweep pass runs. The witness asserts the pass + completes without blocking and without repairing the held + locator (the try-acquire skip), that the cycle does NOT report + completion while the lock is held, and that after the holder + releases, the queued blocking retry deletes the orphan under + the recorded (`id`, `generation`) token BEFORE the cycle + reports completion — the orphan is gone by cycle completion, + proving the §4.5 bound under contention. A repeated-contention + variant hands the lock to a second holder the moment the first + 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 static control asserts the deletion implementation conditions on BOTH the recorded row `id` and `generation` — not on - `content_hash` and not on `generation` alone — and a second + `content_hash` and not on `generation` alone — a second static control asserts the managed-deletion and reconciliation-repair implementations each acquire the §3.7 - locator lock before their observation reads (§4.5, §4.7). + locator lock before their observation reads (§4.5, §4.7), and a + third static control asserts the reconciliation implementation + 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. 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 @@ -1029,7 +1080,9 @@ UPDATE` as the first statement of its transaction, and the per-locator advisory lock spanning both steps — held, per revision 6, by EVERY blob/pointer mutator for the locator: ordinary writers, managed deletion, and reconciliation repair - (try-acquire), so live interleavings between any two mutators + (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). 17. The compare-and-delete managed-deletion step: deletion step 2 is