decompose wave 5 — contract suite: audit-first split of the verification backlog (engines' columns already discharge most rows; map in review-wave-5's appendix), seven mechanism-grouped suite-row tasks (queue depth, scheduler, tx commit-atomicity, streams, locks, wakes, opts/backoff equivalence), two engine-side hardening tasks (sqlite commit-error arm, pg F-1 defense-in-depth), and the review-wave-5 gate that flips the engine specs to stable
This commit is contained in:
1 parent
9a00fb8a7e
commit
250511d480
11 files changed
+911
-2
No files matched your search
@@ -0,0 +1,93 @@
|
||||
---
|
||||
id: suite-scheduler-rows
|
||||
name: Contract-suite rows — scheduler boundary/catch-up/leadership (+ determinism-posture extension)
|
||||
status: pending
|
||||
depends_on: []
|
||||
scope: moderate
|
||||
risk: medium
|
||||
impact: phase
|
||||
level: implementation
|
||||
tags: [wave-5, contract-suite, scheduler]
|
||||
---
|
||||
|
||||
## Description
|
||||
|
||||
Add the scheduler contract rows to
|
||||
`alkstore-contract-suite/src/properties.rs` and wire them into both
|
||||
engines' suite targets, discharging the backlog row "Scheduler + depth
|
||||
properties on Postgres" (core-contract.md §Verification backlog): the
|
||||
tick machinery — boundary advance, bounded catch-up, leadership-loss
|
||||
discipline — pinned engine-uniform (SQLite inherits the substrate's
|
||||
test-pinned implementation; pg re-derived; the suite pins identical
|
||||
*behavior*).
|
||||
|
||||
**Posture extension first** (test-side, ADR-017 §2 class 4): the
|
||||
suite's determinism statement (`properties.rs` module doc) currently
|
||||
says runner spawning stays engine-test-side. The backlog explicitly
|
||||
demands these rows in the suite, so amend the module doc to admit
|
||||
**runner-driving rows**: a spawned `run_schedules(stop)` task with a
|
||||
`StopToken`, assertions on state outcomes (jobs fired, leadership
|
||||
returned) with tolerances bounded well above the boundary resolution —
|
||||
never timing-value assertions, never two-task race windows. Document
|
||||
the extension where the posture is stated.
|
||||
|
||||
Rows to add:
|
||||
|
||||
- **`scheduler_boundary_fires`** — register `@every 1s`, run the
|
||||
runner briefly, stop: boundary fires land as ordinary claimable jobs
|
||||
stamped with the `ScheduleOpts`/derived-default resolution
|
||||
(ADR-009 §3, ADR-020 §3); no double-fire per boundary while one
|
||||
leader runs (fire + boundary-advance commit atomically).
|
||||
- **`scheduler_bounded_catchup`** — register, delay before starting
|
||||
the runner (several elapsed boundaries), then run: missed boundaries
|
||||
replay boundary-by-boundary (at-least-once per elapsed boundary),
|
||||
the fired count bounded by the 64-cap (a multi-second downtime stays
|
||||
far below it — the ≤64 catch-up leg is the suite-pinnable one).
|
||||
**The beyond-cap skip-forward leg needs >64 elapsed boundaries
|
||||
(~65+ s) and row-backdating the public surface does not express —
|
||||
pin it engine-side where the schedule row's `next_fire_at` is
|
||||
directly manipulable (both engines' scheduler tests), and record
|
||||
that disposition in Notes for the review gate.**
|
||||
- **`scheduler_leadership_discipline`** — two concurrent runners:
|
||||
exactly one leader (fires not duplicated), the loser surfaces
|
||||
`LeadershipLost` (ADR-009 §6) rather than silently co-ticking;
|
||||
a stopped runner's clean-stop return shape per ADR-019 §4.
|
||||
|
||||
**Disposition note from the wave-4 fix-batch gate** (recorded, not a
|
||||
defect): the pg tick's in-tx enqueue fires issue no `pg_notify` wake
|
||||
(SQLite's watcher wakes on those commits) — a cross-engine
|
||||
wake-latency-parity gap the re-poll safety net covers for correctness.
|
||||
If this row's shape demands the parity, the one-call `wake_tx` inside
|
||||
the tick's tx rides **this** task; otherwise record the row's
|
||||
latency-posture in Notes and leave the engines as they are.
|
||||
|
||||
## Acceptance Criteria
|
||||
|
||||
- [ ] The determinism-posture extension documented in
|
||||
`properties.rs`'s module doc (runner-driving rows admitted,
|
||||
tolerance-bounded state assertions only)
|
||||
- [ ] Three rows exist, version-stamped (ADR-009 §3/§4/§6, ADR-019 §4,
|
||||
ADR-020 §3 as applicable)
|
||||
- [ ] Rows wired into both engines' `contract_suite.rs` targets
|
||||
- [ ] SQLite column green server-less; pg column green against the
|
||||
harness server
|
||||
- [ ] The skip-forward-leg disposition and the fire-wake-parity
|
||||
disposition recorded in Notes
|
||||
- [ ] `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 (scheduler
|
||||
+ depth properties on Postgres)
|
||||
- docs/architecture/decisions/009-scheduler-collapse.md §3/§4/§6
|
||||
- docs/architecture/decisions/019-mechanism-handle-surfaces.md §4
|
||||
- tasks/review-wave-4-fixes.md (the fire-wake-parity recorded-for-later note)
|
||||
|
||||
## Notes
|
||||
|
||||
> To be filled by implementation agent
|
||||
|
||||
## Summary
|
||||
|
||||
> To be filled on completion
|
||||
Reference in new issue
Block a user