120 lines
5.7 KiB
Markdown
120 lines
5.7 KiB
Markdown
---
|
|
id: suite-wake-rows
|
|
name: Contract-suite row — wake semantics under the pinned WakeReceiver shapes
|
|
status: completed
|
|
depends_on: []
|
|
scope: narrow
|
|
risk: low
|
|
impact: phase
|
|
level: implementation
|
|
tags: [wave-5, contract-suite, notify]
|
|
---
|
|
|
|
## Description
|
|
|
|
Add the wake-semantics contract row to
|
|
`alkstore-contract-suite/src/properties.rs` and wire it into both
|
|
engines' suite targets, discharging the backlog row "Wake semantics
|
|
under `WakeReceiver` shapes" (core-contract.md §Verification
|
|
backlog): the POCs verified wake delivery/coalescing through their own
|
|
probe types; the pinned `Wake { channel }` / recv forms (ADR-008 §3)
|
|
need the suite's own property on both engines.
|
|
|
|
Row to add:
|
|
|
|
- **`wake_receiver_shapes`** — the wake contract's pinnable core,
|
|
tolerance-bounded (wakes are best-effort hints — the row asserts
|
|
state outcomes, never delivery counts or latencies):
|
|
- a pre-attached listener receives a wake after a committed
|
|
`notify` on its channel (`recv`/`try_recv`/`recv_timeout` forms
|
|
all exercised; the wake's `channel` field matches the listened
|
|
channel — the one piece of semantic content a wake carries);
|
|
- a burst of notifies yields *at least one* wake — never an exact
|
|
per-notify count (coalescing is the documented engine asymmetry:
|
|
possibly coalesced on SQLite, per-notify on pg; the row pins the
|
|
floor, not the shape);
|
|
- a listener attached *after* a commit never sees that commit's
|
|
notify (no-replay — `recv_timeout` idles; the pg no-replay hole
|
|
and SQLite's burst coalescing are both legal under this pin);
|
|
- wakes from a *different* channel do not arrive on this listener
|
|
(channel-scoped delivery — the invalidation-key property caching
|
|
subscribers rely on).
|
|
|
|
The failure-surface arms (watcher death → `recv() -> None` on SQLite;
|
|
the synthetic reconnect-wake on pg) are the engine-differing close
|
|
arms — already pinned engine-side and in the receiver-arms row's
|
|
disposal leg; this row does not re-pin them (cross-reference in the
|
|
doc comment).
|
|
|
|
## Acceptance Criteria
|
|
|
|
- [ ] The row exists, version-stamped (ADR-006, ADR-008 §3)
|
|
- [ ] Wired into both engines' `contract_suite.rs` targets
|
|
- [ ] SQLite column green server-less; pg column green against the
|
|
harness server
|
|
- [ ] The row's doc comment cross-references the close-arm pins it
|
|
deliberately does not duplicate
|
|
- [ ] `cargo test -p alkstore-sqlite -p alkstore-postgres` green
|
|
(pg rows skip cleanly server-less); clippy `-D warnings`; fmt clean
|
|
|
|
## References
|
|
|
|
- docs/architecture/core-contract.md §Verification backlog (wake
|
|
semantics under WakeReceiver shapes); §notify/listen
|
|
- docs/architecture/decisions/006-wake-and-delivery-contract.md
|
|
- docs/architecture/decisions/008-contract-v1-pinning.md §3
|
|
|
|
## Notes
|
|
|
|
> 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
|
|
|
|
> 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). |