docs: custody-schema contract revision 7 (sol r6 F15: within-cycle blocking retry preserves the one-cycle orphan bound under lock contention)
ci/woodpecker/pr/ci Pipeline failed
ci/woodpecker/pr/ci Pipeline failed
This commit is contained in:
@@ -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
|
grants to one ceasing grantee are attributable to their exact rows
|
||||||
and subjects, witnessed with a two-subject case (F12).
|
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
|
This contract binds the profile-category registry (§2), the custody
|
||||||
placement rule (§3), the pointer schema (§4), the consent schema and its
|
placement rule (§3), the pointer schema (§4), the consent schema and its
|
||||||
evaluation (§5), mode application (§6), witnesses (§7), and disclosed
|
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.
|
at most one cycle, and repair performs no database content write.
|
||||||
Per-pointer repair runs under the §3.7 locator lock: before
|
Per-pointer repair runs under the §3.7 locator lock: before
|
||||||
observing content absence for a pointer, reconciliation acquires
|
observing content absence for a pointer, reconciliation acquires
|
||||||
the pointer's locator lock (a try-acquire is permitted — a
|
the pointer's locator lock, holds it across the observation and
|
||||||
locator whose lock is held is skipped and repaired on the next
|
the DELETE, and releases it after. The sweep pass MAY use a
|
||||||
cycle, so the sweep never blocks behind a writer), holds it
|
try-acquire so it never blocks mid-pass behind a writer, but a
|
||||||
across the observation and the DELETE, and releases it after.
|
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
|
The repair DELETE is additionally token-conditioned like §4.7
|
||||||
step 2: it records the row's `id` and `generation` when it
|
step 2: it records the row's `id` and `generation` when it
|
||||||
observes the content absent and conditions the DELETE on BOTH —
|
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
|
observation and content removal inside the writer's
|
||||||
step-1-to-step-2 gap and asserts the witness DETECTS the
|
step-1-to-step-2 gap and asserts the witness DETECTS the
|
||||||
resulting acknowledged-write loss, establishing that the lock is
|
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
|
static control asserts the deletion implementation conditions on
|
||||||
BOTH the recorded row `id` and `generation` — not 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
|
static control asserts the managed-deletion and
|
||||||
reconciliation-repair implementations each acquire the §3.7
|
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
|
11. **Default-deny and granularity witnesses:** an agent grantee with
|
||||||
no active row is refused; with a `granted` row for category A
|
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
|
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
|
per-locator advisory lock spanning both steps — held, per
|
||||||
revision 6, by EVERY blob/pointer mutator for the locator:
|
revision 6, by EVERY blob/pointer mutator for the locator:
|
||||||
ordinary writers, managed deletion, and reconciliation repair
|
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,
|
are excluded by one serialization protocol (§3.7, §4.5, §4.7,
|
||||||
§7.16).
|
§7.16).
|
||||||
17. The compare-and-delete managed-deletion step: deletion step 2 is
|
17. The compare-and-delete managed-deletion step: deletion step 2 is
|
||||||
|
|||||||
Reference in New Issue
Block a user