Contract-suite wake row (task suite-wake-rows): wake_receiver_shapes — the wake contract's pinnable core, tolerance-bounded to state outcomes (never delivery counts or latencies): a pre-attached listener receives a wake after a committed notify on its channel through all three recv forms (recv/try_recv/recv_timeout), every wake's channel field matching the listened channel (the one piece of semantic content a wake carries, ADR-008 §3); a three-notify burst floors at one wake — never an exact per-notify count (coalescing the documented engine asymmetry: SQLite's 1-slot feed vs pg per-notify, the row pins the floor not the shape); a listener attached after a commit never sees that commit's notify — recv_timeout idles a 400 ms absence window (a 300 ms pre-settle sleep closes SQLite's watcher baseline race: the last_version baseline is store-open-captured, so an unconsumed commit's version change would fire one late tick at the new subscriber indistinguishable from replay; pg's gap-commit no-replay hole and SQLite's burst coalescing both legal under the pin); and the channel-scoped leg — a foreign-channel notify never surfaces a wake naming it (SQLite's same-commit overtrigger may deliver but carries only the listened channel; the pg LISTEN fanout skips foreign channels; the reserved reconnect straggler tolerated), with a same-channel positive control proving the silence is scoping not a dead listener. The failure-surface close arms (SQLite watcher-death recv()->None, pg synthetic reconnect-wake) stay pinned engine-side and in receiver_close_and_save_arms's disposal leg — cross-referenced in the doc comment, not re-pinned. Stamped ADR-006 + ADR-008 §3. Wired into both engines' suite targets (SQLite tokio test, pg harness_row!), 24 rows per column up from 23. Dispositions in Notes: the backlog row stays in core-contract.md's inventory (flushes at review-wave-5's stable gate, like the other discharged rows), the absence windows are single recv_timeout calls (the documented Ok(None) idle arm as the bounded wait), and the scoping leg's observable is the channel field not absence (SQLite overtrigger makes an absence-only pin vacuous there). Verified: SQLite column green server-less, pg column green vs harness (postgres/poc@:15432), 3 solo re-runs of the row per engine (determinism), cargo test -p alkstore-sqlite -p alkstore-postgres green (SQLite 189+24, pg 121+24+9), workspace cargo test green (12 binaries), clippy -D warnings, fmt clean
This commit is contained in:
1 parent
98de4a49cd
commit
2a2ad7e11f
5 files changed
+302
-6
No files matched your search
@@ -1,7 +1,7 @@
|
||||
---
|
||||
id: suite-wake-rows
|
||||
name: Contract-suite row — wake semantics under the pinned WakeReceiver shapes
|
||||
status: pending
|
||||
status: completed
|
||||
depends_on: []
|
||||
scope: narrow
|
||||
risk: low
|
||||
@@ -66,8 +66,55 @@ doc comment).
|
||||
|
||||
## Notes
|
||||
|
||||
> To be filled by implementation agent
|
||||
> Dispositions of record:
|
||||
|
||||
- **The no-replay leg's pre-settle sleep is load-bearing on SQLite**:
|
||||
the substrate watcher's `last_version` baseline is captured at store
|
||||
open, so a commit landing between the watcher's last poll and the
|
||||
late `listen()` fires one late tick at the new subscriber —
|
||||
indistinguishable from a replay. The 300 ms settle (bounded far above
|
||||
the 1 ms default poll cadence) closes the race: the pin starts at
|
||||
the attach, and a past-window spurious wake arriving before it is
|
||||
the documented overtrigger.
|
||||
- **The channel-scoped leg's observable is the wake's `channel`
|
||||
field, not absence**: on SQLite the watcher fires on *any* commit,
|
||||
so a foreign-channel notify (may) deliver a wake — but its field
|
||||
carries only the *listened* channel (cloned at listen). The row
|
||||
asserts: no wake naming a foreign consumer channel ever surfaces
|
||||
(`scope-a` and the reserved reconnect name are the two admitted
|
||||
carriers), and a same-channel positive control still delivers — the
|
||||
silence is scoping, not a dead listener. On pg the same window is
|
||||
structurally empty (LISTEN is channel-scoped) — the vacuous column
|
||||
is itself the scoping proof.
|
||||
- **The reserved reconnect-wake is admitted as a tolerated straggler**
|
||||
in both absence windows (a reconnect coincident with a window is a
|
||||
legal engine arm) — the arms themselves stay pinned engine-side and
|
||||
in `receiver_close_and_save_arms`, cross-referenced in the row's doc
|
||||
comment as the task requires.
|
||||
- **Absence windows are single `recv_timeout` calls** (400 ms / 400 ms)
|
||||
— the documented `Ok(None)` idle arm doubles as the bounded wait;
|
||||
no timing-value assertions, single-task drive, no two-task race
|
||||
windows.
|
||||
- **The core-contract backlog row stays in the inventory** — same
|
||||
posture as the other discharged rows (locks, streams, depth): the
|
||||
backlog list flushes at the review-wave-5 gate that flips the engine
|
||||
specs to stable.
|
||||
|
||||
## Summary
|
||||
|
||||
> To be filled on completion
|
||||
> Landed the `wake_receiver_shapes` contract-suite row
|
||||
> (`alkstore-contract-suite/src/properties.rs`, version-stamped
|
||||
> ADR-006 + ADR-008 §3, doc comment cross-references the close arms it
|
||||
> does not re-pin) and wired it into both engines' suite targets
|
||||
> (SQLite tokio test, pg `harness_row!`) — 23 → 24 rows per column.
|
||||
> Legs: pre-attached listener + committed notify through all three
|
||||
> recv forms with channel-field match; three-notify burst flooring at
|
||||
> one wake (never an exact count); attach-after-commit never replays
|
||||
> (`recv_timeout` idles, settled); foreign-channel notify never
|
||||
> surfaces a foreign wake + same-channel positive control. Verified:
|
||||
> SQLite column green server-less; pg column green against the harness
|
||||
> server (postgres/poc@:15432); 3 solo re-runs of the row per engine
|
||||
> (determinism); `cargo test -p alkstore-sqlite -p alkstore-postgres`
|
||||
> green (SQLite 189+24, pg 121+24+9); workspace `cargo test` green;
|
||||
> clippy `-D warnings` clean; fmt clean (fmt reflowed the pg
|
||||
> `harness_row!` after the first pass).
|
||||
Reference in new issue
Block a user