5.7 KiB
id, name, status, depends_on, scope, risk, impact, level, tags
| id | name | status | depends_on | scope | risk | impact | level | tags | |||
|---|---|---|---|---|---|---|---|---|---|---|---|
| suite-wake-rows | Contract-suite row — wake semantics under the pinned WakeReceiver shapes | completed | narrow | low | phase | implementation |
|
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
notifyon its channel (recv/try_recv/recv_timeoutforms all exercised; the wake'schannelfield 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_timeoutidles; 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).
- a pre-attached listener receives a wake after a committed
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.rstargets - 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-postgresgreen (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_versionbaseline is captured at store open, so a commit landing between the watcher's last poll and the latelisten()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
channelfield, 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-aand 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_timeoutcalls (400 ms / 400 ms) — the documentedOk(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_shapescontract-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, pgharness_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_timeoutidles, 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-postgresgreen (SQLite 189+24, pg 121+24+9); workspacecargo testgreen; clippy-D warningsclean; fmt clean (fmt reflowed the pgharness_row!after the first pass).