custody contract revision 11: acquisition-token guard on the fence-advance (sol r10 F16 residual, F18)
ci/woodpecker/pr/ci Pipeline was successful
ci/woodpecker/pr/ci Pipeline was successful
The fence-advance is itself fenced against an older acquisition: a per-locator acquisition token minted by the lock authority at every lock grant, carried unchanged across the acquisition's brain operations and swap-loop retries, compared and recorded by the brain store atomically with every brain mutation (advance included). A superseded acquisition's delayed advance is refused, mints nothing, and yields no usable fence (mandatory abort-release-surface, expected on deadline supersession). The 'refused unconditionally' claim is precisified to the exact linearization boundary; the pre-step-1 interruption predicates are restated over exact content/database state, expressly permitting the advance's epoch/token change (F18). New §7.10 stale-advance refusal and pre-advance linearization controls; token invariants added to the fence static controls (§7.10, §7.16); §8 item 16 and preamble extended.
This commit is contained in:
@@ -214,6 +214,39 @@ repair-observation variant, and a static fence-epoch-invariant
|
|||||||
control; §7.16's static fenced-commit control is restated over the
|
control; §7.16's static fenced-commit control is restated over the
|
||||||
epoch (F16, F17).
|
epoch (F16, F17).
|
||||||
|
|
||||||
|
Revision 11 (sol r10 residual F16 + new F18): the fence-advance
|
||||||
|
itself is fenced against an older acquisition. §3.7 adds a
|
||||||
|
per-locator ACQUISITION TOKEN minted by the lock authority at every
|
||||||
|
lock grant — fresh, strictly increasing, existing before the
|
||||||
|
holder's first brain operation and carried unchanged through every
|
||||||
|
brain operation and swap-loop retry of that acquisition — and the
|
||||||
|
brain store records the greatest accepted token atomically with the
|
||||||
|
locator's epoch and content state, refusing any brain mutation,
|
||||||
|
the fence-advance included, that carries an older token. The
|
||||||
|
advance's acceptance condition is exactly this comparison (an epoch
|
||||||
|
condition would be circular, an unconditional mint would let a
|
||||||
|
terminated holder's delayed advance supersede a later holder's); a
|
||||||
|
refused advance mints nothing and returns no usable fence, with a
|
||||||
|
mandatory abort-release-surface transition that is an EXPECTED
|
||||||
|
outcome after deadline supersession, not a defect. Revision 10's
|
||||||
|
"refused unconditionally" claim is precisified to an exact
|
||||||
|
boundary: after the newer holder's advance linearizes, every
|
||||||
|
older-acquisition operation — its delayed advance included — is
|
||||||
|
refused; a stale content mutation linearizing BEFORE that advance
|
||||||
|
serializes entirely before anything the new holder relies on (the
|
||||||
|
advance preserves the content state it finds and mints after it),
|
||||||
|
indistinguishable from completion before the previous holder's
|
||||||
|
lock release — the defined legal outcome. The pre-step-1
|
||||||
|
interruption predicates in §3.7, §4.7, and the §7.16 fault
|
||||||
|
injection are restated exactly — content presence, content bytes,
|
||||||
|
and database rows unchanged, the advance's epoch mint and token
|
||||||
|
recording expressly permitted — resolving their contradiction with
|
||||||
|
the mandatory advance (F18). §7.10 adds a stale-advance refusal
|
||||||
|
control (fresh-writer and repair-observation variants) and a
|
||||||
|
pre-advance linearization control, and extends the fence-invariant
|
||||||
|
static control with the token invariants; §7.16's static
|
||||||
|
fenced-commit control carries the token (F16, F18).
|
||||||
|
|
||||||
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
|
||||||
@@ -466,8 +499,17 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
**Brain fence.** Deadline termination releases the lock while an
|
**Brain fence.** Deadline termination releases the lock while an
|
||||||
external brain operation started by the terminated holder may
|
external brain operation started by the terminated holder may
|
||||||
still be in flight; lock release is therefore not, by itself, a
|
still be in flight; lock release is therefore not, by itself, a
|
||||||
fence for the external store. The fence is a per-locator **fence
|
fence for the external store. Two per-locator values fence it:
|
||||||
epoch**: a value stored in the brain store, atomically readable
|
an **acquisition token** ordering holders and a **fence epoch**
|
||||||
|
ordering mutations. The acquisition token is minted by the lock
|
||||||
|
authority at EVERY grant of the locator lock: a fresh, strictly
|
||||||
|
increasing per-locator value handed to the holder with the
|
||||||
|
grant — it therefore exists before the holder's first brain
|
||||||
|
operation, independently of any brain state — and carried
|
||||||
|
UNCHANGED through every brain operation of that acquisition,
|
||||||
|
including every retry of a swap loop; a holder never re-mints
|
||||||
|
or refreshes its token. The fence epoch is a per-locator value
|
||||||
|
stored in the brain store, atomically readable
|
||||||
and comparable together with the locator's content state, whose
|
and comparable together with the locator's content state, whose
|
||||||
defining property is that every change to it MINTS a fresh value
|
defining property is that every change to it MINTS a fresh value
|
||||||
never before used at that locator. A per-locator monotonic
|
never before used at that locator. A per-locator monotonic
|
||||||
@@ -476,11 +518,18 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
byte-identical states at different times are distinct epochs —
|
byte-identical states at different times are distinct epochs —
|
||||||
and ABSENCE is itself an epoch-bearing state, recorded as a
|
and ABSENCE is itself an epoch-bearing state, recorded as a
|
||||||
unique tombstone, never a bare missing path whose "value" can
|
unique tombstone, never a bare missing path whose "value" can
|
||||||
recur. Two rules bind the epoch. **Minting:** every successful
|
recur. Three rules bind them. **Minting:** every successful
|
||||||
brain mutation under a locator lock — a content commit, a
|
brain mutation under a locator lock — a content commit, a
|
||||||
byte-identical recommit, a content deletion (transition to
|
byte-identical recommit, a content deletion (transition to
|
||||||
absence) — advances the locator's epoch to a fresh never-reused
|
absence) — advances the locator's epoch to a fresh never-reused
|
||||||
value, atomically with the mutation. **Fence-advance at
|
value, atomically with the mutation. **Token recording:** the
|
||||||
|
brain store records, per locator and atomically with the
|
||||||
|
locator's epoch and content state, the greatest acquisition
|
||||||
|
token it has accepted; EVERY brain mutation under a locator
|
||||||
|
lock — the fence-advance below included — presents its holder's
|
||||||
|
acquisition token, is REFUSED atomically when that token is
|
||||||
|
less than the recorded value, and records it on acceptance.
|
||||||
|
**Fence-advance at
|
||||||
acquisition:** immediately after acquiring the locator lock,
|
acquisition:** immediately after acquiring the locator lock,
|
||||||
before its first brain observation or mutation at the locator,
|
before its first brain observation or mutation at the locator,
|
||||||
the holder performs a fence-advance — an atomic epoch mint that
|
the holder performs a fence-advance — an atomic epoch mint that
|
||||||
@@ -488,37 +537,74 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
records the resulting epoch as its **fence value**; the advance
|
records the resulting epoch as its **fence value**; the advance
|
||||||
invalidates every fence recorded by any earlier holder before
|
invalidates every fence recorded by any earlier holder before
|
||||||
the new holder relies on anything it reads or on its
|
the new holder relies on anything it reads or on its
|
||||||
exclusivity. Every brain mutation performed under a locator
|
exclusivity. The advance's OWN acceptance condition is exactly
|
||||||
|
the token comparison — not the epoch (no fence exists for the
|
||||||
|
acquisition until the advance returns, so an epoch condition
|
||||||
|
would be circular) and not nothing (an unconditional mint would
|
||||||
|
let a terminated holder's delayed advance supersede a later
|
||||||
|
holder's): the token is minted at lock grant, so it exists
|
||||||
|
before the advance, and grants for one locator are totally
|
||||||
|
ordered, so the comparison encodes acquisition order. A refused
|
||||||
|
advance returns NO usable fence: the holder MUST NOT perform
|
||||||
|
any brain observation or mutation, MUST abort its protocol run
|
||||||
|
before any later step, release the lock if it still holds it,
|
||||||
|
and surface the error — and this refusal is an EXPECTED outcome
|
||||||
|
for an acquisition whose lock was deadline-released and
|
||||||
|
re-granted before its delayed advance applied, not a defect.
|
||||||
|
Every other brain mutation performed under a locator
|
||||||
lock — an ordinary write's step-1 content commit (below), a
|
lock — an ordinary write's step-1 content commit (below), a
|
||||||
managed deletion's step-1 content deletion (§4.7) — is applied
|
managed deletion's step-1 content deletion (§4.7) — is applied
|
||||||
conditionally: the brain store applies it only if the locator's
|
conditionally: the brain store applies it only if the locator's
|
||||||
epoch at application time still equals the holder's recorded
|
epoch at application time still equals the holder's recorded
|
||||||
fence value, with the check and the application atomic with
|
fence value AND the token-recording comparison accepts, with
|
||||||
|
the checks and the application atomic with
|
||||||
respect to other brain mutations (compare-and-swap semantics; an
|
respect to other brain mutations (compare-and-swap semantics; an
|
||||||
atomic ref update in a git-backed store satisfies this, with the
|
atomic ref update in a git-backed store satisfies this, with the
|
||||||
per-locator epoch condition re-validated inside the swap loop
|
per-locator conditions re-validated inside the swap loop
|
||||||
when the swap is taken on a coarser head). A stale operation —
|
when the swap is taken on a coarser head). A stale operation —
|
||||||
one whose session was terminated and whose lock has passed to a
|
one whose session was terminated and whose lock has passed to a
|
||||||
newer holder — is REFUSED unconditionally: its recorded epoch
|
newer holder — is refused at an exact boundary. Once the newer
|
||||||
predates the next holder's fence-advance, so the condition fails
|
holder's fence-advance has linearized, EVERY operation of the
|
||||||
whether the intervening history changed the bytes, recommitted
|
older acquisition is refused: its epoch condition fails (the
|
||||||
byte-identical content, returned the locator to absence, or
|
advance consumed its epoch, and no sequence of mutations can
|
||||||
consists of the advance alone — refusal does not wait for the
|
re-present a consumed one — whether the intervening history
|
||||||
new holder's first mutation, and no sequence of mutations can
|
changed the bytes, recommitted byte-identical content, returned
|
||||||
re-present a consumed epoch. It cannot remove or replace content
|
the locator to absence, or consists of the advance alone), its
|
||||||
committed by any later holder, whether it resumes microseconds
|
token comparison fails, and its own delayed fence-advance is
|
||||||
|
refused by the token comparison, minting nothing — a superseded
|
||||||
|
acquisition cannot manufacture a fresh fence. Before the newer
|
||||||
|
advance linearizes, a stale content mutation whose conditions
|
||||||
|
still hold MAY linearize first: the advance then finds the
|
||||||
|
post-mutation state, expressly preserves the content presence
|
||||||
|
and bytes it finds, mints its epoch after that mutation, and
|
||||||
|
the new holder's first relied-on observation follows its own
|
||||||
|
advance — so the stale effect serializes entirely before
|
||||||
|
anything the new holder relies on, indistinguishable from the
|
||||||
|
same operation completing before the previous holder's lock
|
||||||
|
release, an outcome the protocol already defines as legal (its
|
||||||
|
database half remains governed by the (`id`, `generation`)
|
||||||
|
pair, §4.5, §4.7). These are the only two outcomes: a stale
|
||||||
|
operation either serializes wholly before the new holder's
|
||||||
|
advance or is refused; it never applies after the advance, and
|
||||||
|
it cannot remove or replace content committed by any later
|
||||||
|
holder, whether it resumes microseconds
|
||||||
or hours after the termination. A live holder's own fenced
|
or hours after the termination. A live holder's own fenced
|
||||||
mutation cannot fail its condition — not because it holds the
|
mutation cannot fail its conditions — not because it holds the
|
||||||
lock, but because handoff invalidation plus minting mean the
|
lock, but because handoff invalidation plus minting mean the
|
||||||
only epochs minted since its fence-advance are its own; a
|
only epochs minted since its fence-advance are its own, and
|
||||||
|
because lock grants are serialized by the lock itself, no
|
||||||
|
greater acquisition token can be recorded while it holds the
|
||||||
|
lock; a
|
||||||
holder whose fenced mutation is nonetheless refused (reachable
|
holder whose fenced mutation is nonetheless refused (reachable
|
||||||
only under a defect breaching these invariants) MUST abort its
|
only under a defect breaching these invariants) MUST abort its
|
||||||
protocol run, release the lock, and surface the error — it
|
protocol run, release the lock, and surface the error — it
|
||||||
never retries the mutation under its stale fence. Every
|
never retries the mutation under its stale fence. Every
|
||||||
brain-mutation path carries the fence, and every brain-RELYING
|
brain-mutation path carries the fence and the acquisition
|
||||||
|
token, and every brain-RELYING
|
||||||
observation path (reconciliation repair's absence observation,
|
observation path (reconciliation repair's absence observation,
|
||||||
§4.5) performs its fence-advance before the observation it
|
§4.5) performs its fence-advance before the observation it
|
||||||
relies on; a path applying an unfenced brain mutation fails the
|
relies on; a path applying an unfenced or token-free brain
|
||||||
|
mutation fails the
|
||||||
§7.10 and §7.16 static controls.
|
§7.10 and §7.16 static controls.
|
||||||
|
|
||||||
**Steps.** Step 1 commits the content to the owning user's brain
|
**Steps.** Step 1 commits the content to the owning user's brain
|
||||||
@@ -528,8 +614,11 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
existing row for that (user, category, brain_ref), incrementing
|
existing row for that (user, category, brain_ref), incrementing
|
||||||
`generation` per §4.1) in its own database transaction inside the
|
`generation` per §4.1) in its own database transaction inside the
|
||||||
§2.6 fence. The write is acknowledged to the caller only after
|
§2.6 fence. The write is acknowledged to the caller only after
|
||||||
step 2 commits. Interruption before step 1 leaves both stores
|
step 2 commits. Interruption before step 1 leaves content
|
||||||
unchanged. Interruption between the steps leaves committed brain
|
presence, content bytes, and every database row unchanged — the
|
||||||
|
post-acquisition fence-advance may already have minted an epoch
|
||||||
|
and recorded an acquisition token, the only brain change the
|
||||||
|
protocol permits before step 1. Interruption between the steps leaves committed brain
|
||||||
content with no pointer: unpointed content is inert — it lives in
|
content with no pointer: unpointed content is inert — it lives in
|
||||||
the correct custody store, no read path serves it (reads resolve
|
the correct custody store, no read path serves it (reads resolve
|
||||||
through pointers only), and nothing dangles in the database.
|
through pointers only), and nothing dangles in the database.
|
||||||
@@ -623,10 +712,13 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
and repair performs no database content write.
|
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, performs the §3.7 fence-advance —
|
the pointer's locator lock, performs the §3.7 fence-advance
|
||||||
|
under repair's own acquisition token —
|
||||||
invalidating any stale in-flight operation's fence BEFORE the
|
invalidating any stale in-flight operation's fence BEFORE the
|
||||||
observation repair relies on, so no terminated holder's resuming
|
observation repair relies on, so no terminated holder's resuming
|
||||||
mutation can change the locator between repair's observation and
|
mutation — its delayed fence-advance included, refused by the
|
||||||
|
§3.7 token comparison — can change the locator between repair's
|
||||||
|
observation and
|
||||||
its DELETE — holds the lock across the observation and the
|
its DELETE — holds the lock across the observation and the
|
||||||
DELETE, and releases it after. The sweep pass MAY use a
|
DELETE, and releases it after. The sweep pass MAY use a
|
||||||
try-acquire so it never blocks mid-pass behind a writer, but a
|
try-acquire so it never blocks mid-pass behind a writer, but a
|
||||||
@@ -725,6 +817,7 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
commits the content deletion to the user's brain repository as
|
commits the content deletion to the user's brain repository as
|
||||||
a FENCED mutation (§3.7 Brain fence — conditioned on the fence
|
a FENCED mutation (§3.7 Brain fence — conditioned on the fence
|
||||||
epoch recorded at the deleter's post-acquisition fence-advance,
|
epoch recorded at the deleter's post-acquisition fence-advance,
|
||||||
|
carrying the deleter's acquisition token,
|
||||||
and itself minting the locator's unique absence tombstone
|
and itself minting the locator's unique absence tombstone
|
||||||
epoch), recording the target row's
|
epoch), recording the target row's
|
||||||
`id` AND `generation` as read after
|
`id` AND `generation` as read after
|
||||||
@@ -759,7 +852,11 @@ with contract 6 (`mode-conversion.md`), identity with
|
|||||||
committed and acknowledged after the termination cannot be
|
committed and acknowledged after the termination cannot be
|
||||||
destroyed by the terminated deleter's resuming operation
|
destroyed by the terminated deleter's resuming operation
|
||||||
(witness §7.10). Interruption before step 1
|
(witness §7.10). Interruption before step 1
|
||||||
commits leaves both stores unchanged. Interruption between the
|
commits leaves content presence, content bytes, and every
|
||||||
|
database row unchanged — the deleter's post-acquisition
|
||||||
|
fence-advance may already have minted an epoch and recorded an
|
||||||
|
acquisition token, the only brain change the protocol permits
|
||||||
|
before step 1. Interruption between the
|
||||||
steps leaves a dangling pointer, which §4.5 repairs toward
|
steps leaves a dangling pointer, which §4.5 repairs toward
|
||||||
deletion within one reconciliation cycle. At no point does any
|
deletion within one reconciliation cycle. At no point does any
|
||||||
compensation write content into the database (witness §7.10,
|
compensation write content into the database (witness §7.10,
|
||||||
@@ -1210,7 +1307,39 @@ declared profile table" means `profile_answers` (§3.5).
|
|||||||
observes content absence, and the stale writer resuming before
|
observes content absence, and the stale writer resuming before
|
||||||
repair's DELETE is asserted refused — the DELETE then
|
repair's DELETE is asserted refused — the DELETE then
|
||||||
completes under its recorded (`id`, `generation`) token and
|
completes under its recorded (`id`, `generation`) token and
|
||||||
NO unpointed content is resurrected at the locator. An **exceedance control** contrives a
|
NO unpointed content is resurrected at the locator. A
|
||||||
|
**stale-advance refusal control** exercises the §3.7 token
|
||||||
|
guard on the advance itself: writer W1 acquires the locator
|
||||||
|
lock and its mandatory fence-advance is suspended BEFORE its
|
||||||
|
atomic application; the independent supervisor terminates W1's
|
||||||
|
session at the deadline and the lock releases; the next holder
|
||||||
|
acquires the lock (receiving a greater acquisition token) and
|
||||||
|
completes its own fence-advance; W1's suspended advance is
|
||||||
|
then RESUMED and asserted REFUSED by the token comparison —
|
||||||
|
it mints no epoch and returns no usable fence — and W1's
|
||||||
|
protocol run is asserted to abort with the error surfaced,
|
||||||
|
performing no further brain observation or mutation, while
|
||||||
|
the next holder's fence remains valid and its subsequent
|
||||||
|
fenced mutation is asserted to succeed. A fresh-writer
|
||||||
|
variant runs the next holder as an ordinary §3.7 writer
|
||||||
|
through a full acknowledged write; a repair-observation
|
||||||
|
variant runs it as §4.5 reconciliation — repair advances,
|
||||||
|
observes content absence, W1's late advance resumed before
|
||||||
|
the DELETE is asserted refused and fenceless, and the DELETE
|
||||||
|
completes under its recorded (`id`, `generation`) token with
|
||||||
|
no unpointed content resurrected. A **pre-advance
|
||||||
|
linearization control** exercises the §3.7 legal-outcome
|
||||||
|
boundary: a terminated holder's stale content mutation is
|
||||||
|
scheduled to linearize immediately BEFORE the next holder's
|
||||||
|
fence-advance swap; the control asserts the store serializes
|
||||||
|
the stale mutation first, the advance preserves the
|
||||||
|
post-mutation content presence and bytes and mints its epoch
|
||||||
|
after it, the new holder's first relied-on observation
|
||||||
|
reflects the committed stale effect, and the end state is
|
||||||
|
consistent — equivalent to the stale operation having
|
||||||
|
completed before the previous holder's lock release — with
|
||||||
|
the stale operation's database half still governed by the
|
||||||
|
(`id`, `generation`) pair. An **exceedance control** contrives a
|
||||||
cycle that cannot finish within its computed `M` (an injected
|
cycle that cannot finish within its computed `M` (an injected
|
||||||
sequence of deadline-length holders on a reserved locator) and
|
sequence of deadline-length holders on a reserved locator) and
|
||||||
asserts the cycle reports FAILURE — never completion —
|
asserts the cycle reports FAILURE — never completion —
|
||||||
@@ -1254,7 +1383,18 @@ declared profile table" means `profile_answers` (§3.5).
|
|||||||
value, and no path represents the fence by content bytes,
|
value, and no path represents the fence by content bytes,
|
||||||
content hash, or bare path absence — an implementation whose
|
content hash, or bare path absence — an implementation whose
|
||||||
fence value can recur, or that observes before advancing,
|
fence value can recur, or that observes before advancing,
|
||||||
FAILS.
|
FAILS. The same control asserts the §3.7 acquisition-token
|
||||||
|
invariants: the lock authority mints a fresh, strictly
|
||||||
|
increasing per-locator token at every lock grant; every
|
||||||
|
brain-mutation path — the fence-advance included — presents
|
||||||
|
its holder's token unchanged across every swap-loop retry;
|
||||||
|
the brain store's token comparison and recording are atomic
|
||||||
|
with the mutation they guard; the advance is refused when its
|
||||||
|
token is less than the recorded value; and a refused advance
|
||||||
|
yields no usable fence — an implementation whose advance
|
||||||
|
applies unconditionally, that re-mints or refreshes a token
|
||||||
|
within an acquisition, or whose holder proceeds to any brain
|
||||||
|
observation or mutation after a refused advance, 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
|
||||||
@@ -1326,7 +1466,10 @@ declared profile table" means `profile_answers` (§3.5).
|
|||||||
violates the §6.3 singleton constraint.
|
violates the §6.3 singleton constraint.
|
||||||
16. **Ordered-write protocol witnesses:** the §3.7 protocol is
|
16. **Ordered-write protocol witnesses:** the §3.7 protocol is
|
||||||
fault-injected at its interruption points: killed before the
|
fault-injected at its interruption points: killed before the
|
||||||
brain commit, both stores are unchanged and the caller receives
|
brain commit, content presence, content bytes, and every
|
||||||
|
database row are unchanged — the post-acquisition
|
||||||
|
fence-advance's epoch mint and token recording are the only
|
||||||
|
permitted brain change — and the caller receives
|
||||||
no acknowledgment; killed between the brain commit and the
|
no acknowledgment; killed between the brain commit and the
|
||||||
pointer upsert, the brain holds unpointed content, no pointer row
|
pointer upsert, the brain holds unpointed content, no pointer row
|
||||||
exists, no read surface serves the content, and the caller
|
exists, no read surface serves the content, and the caller
|
||||||
@@ -1364,8 +1507,9 @@ declared profile table" means `profile_answers` (§3.5).
|
|||||||
enumerated sensitive-write route applies its step-1 brain
|
enumerated sensitive-write route applies its step-1 brain
|
||||||
commit as a fenced mutation conditioned on the recorded §3.7
|
commit as a fenced mutation conditioned on the recorded §3.7
|
||||||
fence epoch — recorded at the route's post-acquisition
|
fence epoch — recorded at the route's post-acquisition
|
||||||
fence-advance, the commit itself minting a fresh epoch — an
|
fence-advance, the commit itself minting a fresh epoch and
|
||||||
unfenced brain-commit path FAILS.
|
carrying the route's §3.7 acquisition token — an
|
||||||
|
unfenced or token-free brain-commit path FAILS.
|
||||||
|
|
||||||
## 8. Drafting additions (PRD §12.1 disclosure)
|
## 8. Drafting additions (PRD §12.1 disclosure)
|
||||||
|
|
||||||
@@ -1458,7 +1602,19 @@ UPDATE` as the first statement of its transaction, and the
|
|||||||
included, and advanced by every new holder immediately after
|
included, and advanced by every new holder immediately after
|
||||||
acquisition, before it relies on brain state — so a stale
|
acquisition, before it relies on brain state — so a stale
|
||||||
tail is refused even when bytes or absence recur and even
|
tail is refused even when bytes or absence recur and even
|
||||||
before the new holder's first mutation), so live interleavings
|
before the new holder's first mutation; per revision 11 the
|
||||||
|
fence-advance itself is guarded by an acquisition token —
|
||||||
|
minted fresh and strictly increasing by the lock authority at
|
||||||
|
every lock grant, carried unchanged across an acquisition's
|
||||||
|
brain operations and swap-loop retries, compared and recorded
|
||||||
|
by the brain store atomically with every brain mutation, the
|
||||||
|
advance included — so a superseded acquisition's delayed
|
||||||
|
advance is refused and mints nothing, a refused advance
|
||||||
|
yields no usable fence with a mandatory
|
||||||
|
abort-release-surface transition, and a stale operation
|
||||||
|
either serializes wholly before the new holder's advance —
|
||||||
|
the defined legal pre-release-completion-equivalent outcome —
|
||||||
|
or is refused), so live interleavings
|
||||||
between any two mutators are excluded by one serialization
|
between any two mutators are excluded by one serialization
|
||||||
protocol, and stale external tails are excluded by the fence
|
protocol, and stale external tails are excluded by the fence
|
||||||
(§3.7, §4.5, §4.7, §7.16).
|
(§3.7, §4.5, §4.7, §7.16).
|
||||||
|
|||||||
Reference in New Issue
Block a user