Contract-suite lock rows (task suite-lock-rows): two version-stamped rows discharging the lock backlog rows — lock_ttl_expiry_and_reacquisition (the ADR-008 §7 guarantee row: a held lock excludes a second acquirer (contender None); after a 1 s TTL the exclusion lapses silently — no revocation event, no error — and a second owner acquires; the original holder's post-expiry renew is refused (false, the lost-it arm); the second owner's release frees the name for a third acquirer, which consumes cleanly; tolerance-sleep posture, state outcomes only; ADR-008 §7 + ADR-019 §1, duration-guard legs cross-referenced to duration_refusal_on_non_positive_ttl) and concurrent_try_lock_loser_is_a_value (the contention posture: four sequential contenders — two owners, repeated — against a held lock all land the clean None value, never Database, never a busy-throw; the backlog row's SQLite busy-path open question answered: no divergence from the pg reference; release-then-contend cycle proves the loser path leaves no state blocking a later acquire, granted to a former loser and consumed cleanly; ADR-008 §5 + §7 + ADR-019 §1) — wired into both engines' suite targets (SQLite tokio tests, pg harness_row!s), 23 rows per column up from 21. Dispositions in Notes: no divergence found (no fix/ADR call needed), ADR-023 §2 excluded from stamps (its guard property is the duration-refusal row's, cross-referenced), the backlog parenthetical re-acquire-does-not-refresh-TTL stays engine-pinned, renew-refusal asserted after the second owner's re-acquisition (strongest form), contenders distinct-owner only (same-owner re-acquire grants per the inherited substrate shape), and one unreproducible first-cold-run pg failure recorded (message lost to truncation; 13 subsequent clean runs incl. concurrent SQLite+pg — no timing hazard identified, the lapse assertions are post-sleep state outcomes). Drive-by: alkstore-contract-suite's tokio dep gained the macros feature — a pre-existing compile break in the crate's own tests/suite_harness.rs (since 7f749ac) failed the harness target and the workspace test gate on HEAD; test-side non-event (ADR-017 §2 class 4). Verified: cargo test -p alkstore-sqlite -p alkstore-postgres green (SQLite 121+23+9, pg 189+23 vs harness server on :15432, server-less pg skips clean), workspace cargo test green (12 binaries), clippy -D warnings, fmt clean
This commit is contained in:
1 parent
1d05df200e
commit
98de4a49cd
6 files changed
+285
-17
No files matched your search
@@ -1,7 +1,7 @@
|
||||
---
|
||||
id: suite-lock-rows
|
||||
name: Contract-suite rows — lock TTL/expiry re-acquisition + concurrent try_lock loser
|
||||
status: pending
|
||||
status: completed
|
||||
depends_on: []
|
||||
scope: narrow
|
||||
risk: medium
|
||||
@@ -51,14 +51,14 @@ divergence silently.
|
||||
|
||||
## Acceptance Criteria
|
||||
|
||||
- [ ] Two rows exist, version-stamped (ADR-008 §7, ADR-019 §1,
|
||||
- [x] Two rows exist, version-stamped (ADR-008 §7, ADR-019 §1,
|
||||
ADR-023 §2 as applicable)
|
||||
- [ ] Rows wired into both engines' `contract_suite.rs` targets
|
||||
- [ ] SQLite column green server-less; pg column green against the
|
||||
- [x] Rows wired into both engines' `contract_suite.rs` targets
|
||||
- [x] SQLite column green server-less; pg column green against the
|
||||
harness server
|
||||
- [ ] Any engine divergence found is recorded in Notes with its
|
||||
- [x] Any engine divergence found is recorded in Notes with its
|
||||
disposition (fix or documented asymmetry) — not pinned silently
|
||||
- [ ] `cargo test -p alkstore-sqlite -p alkstore-postgres` green
|
||||
- [x] `cargo test -p alkstore-sqlite -p alkstore-postgres` green
|
||||
(pg rows skip cleanly server-less); clippy `-D warnings`; fmt clean
|
||||
|
||||
## References
|
||||
@@ -71,8 +71,96 @@ divergence silently.
|
||||
|
||||
## Notes
|
||||
|
||||
> To be filled by implementation agent
|
||||
> Decisions of record the description didn't pin:
|
||||
|
||||
- **The open question is answered: no divergence** — the SQLite
|
||||
substrate's busy-path under lock contention never surfaces
|
||||
`Database`: contended `try_lock` returns the same clean
|
||||
`Ok(None)` value as pg (the engines route lock ops through the
|
||||
writer-slot-serialized surface / pool acquire respectively, and
|
||||
both acquire ops are opportunistic-expiry-delete +
|
||||
insert-or-ignore + read-back, so a held row reads as foreign —
|
||||
the loser value — on both). No engine fix and no ADR-level
|
||||
asymmetry call was needed; the row pins the convergence rather
|
||||
than recording one.
|
||||
- **Stamp scope** — ADR-023 §2 is *not* on either row's stamp list:
|
||||
the duration-guard behavior it pins (`ttl <= 0` rejecting on
|
||||
`try_lock`/`renew`) is `duration_refusal_on_non_positive_ttl`'s
|
||||
property (cross-referenced in the TTL row's doc text, as are
|
||||
that row's legs from this one). The rows carry stamps for the
|
||||
behavior they test: ADR-008 §7 (the guarantee row / contention
|
||||
composition), ADR-008 §5 (the loser-value-not-error rule the
|
||||
contention row pins), ADR-019 §1 (the `Lock` handle surface).
|
||||
- **Backlog-row parenthetical stays engine-side** — the backlog
|
||||
row's "re-acquire-does-not-refresh-TTL behavior is upstream's,
|
||||
inherited deliberately" note remains pinned by the SQLite
|
||||
engine tests (`store/lock_tests.rs`'s mapping-row pin); the
|
||||
suite row pins the task description's five lifecycle legs only
|
||||
and does not re-pin the same-owner-re-acquire-returns-Some /
|
||||
TTL-not-refreshed shape (deliberate scope: that shape is the
|
||||
acquisition semantics' *non-lapse* twin, both engine tests pin
|
||||
it, and neither task text asked the suite to own it).
|
||||
- **renew-refusal ordering** — the original holder's `renew` is
|
||||
asserted *after* the second owner's re-acquisition (the
|
||||
strongest form: the row the refuser targets belongs to another
|
||||
owner), rather than immediately post-lapse while the stale row
|
||||
survives; both forms land `false` on both engines, so only the
|
||||
strongest is pinned.
|
||||
- **Contenders are distinct-owner only** — the contention row
|
||||
never drives a same-owner `try_lock` against a held lock: the
|
||||
inherited substrate shape means a same-owner re-acquire grants
|
||||
(`Some`, original row kept) rather than losing, so including it
|
||||
in a "loser is a value" row would misdescribe the property.
|
||||
- **One unreproducible pg failure, first cold run** — the very
|
||||
first pg full-suite run failed `row_lock_ttl_expiry_and_
|
||||
reacquisition`; the failure message was lost to output
|
||||
truncation and the row passed on every subsequent run (5
|
||||
isolated full-suite runs, 3 concurrent SQLite+pg full-suite
|
||||
runs, 5 focused `--test-threads=16` runs — 13 clean total). No
|
||||
divergence observed, no repro found; recorded per the stream-
|
||||
rows task's precedent. The TTL legs' assertions are
|
||||
post-sleep state outcomes (a slower clock can only *delay* the
|
||||
lapse, never un-lapse it), so no timing hazard is identified.
|
||||
|
||||
## Summary
|
||||
|
||||
> To be filled on completion
|
||||
> What landed, verified how:
|
||||
|
||||
Two rows added to `alkstore-contract-suite/src/properties.rs`,
|
||||
re-exported from the crate's lib, wired into both engines'
|
||||
`contract_suite.rs` targets (SQLite: direct test fns; pg: the
|
||||
`harness_row!` macro with unique factory tags) — 23 rows in each
|
||||
engine's column, up from 21:
|
||||
|
||||
- `lock_ttl_expiry_and_reacquisition` — the ADR-008 §7 guarantee
|
||||
row: held → contender `None`; post-1 s-TTL silent lapse (second
|
||||
owner acquires, no error, no revocation event); original
|
||||
holder's post-expiry `renew` refused (`false`); second owner's
|
||||
`release` frees the name for a third acquirer. Stamped ADR-008
|
||||
§7 + ADR-019 §1; duration-guard legs cross-referenced to
|
||||
`duration_refusal_on_non_positive_ttl` (ADR-023 §2).
|
||||
- `concurrent_try_lock_loser_is_a_value` — the contention
|
||||
posture: four sequential contenders (two distinct owners,
|
||||
repeated) against a held lock all get the clean `None` value —
|
||||
never `Database`, never a busy-throw (the backlog row's SQLite
|
||||
busy-path open question, answered: no divergence from the pg
|
||||
reference) — plus a release-then-contend cycle granting a
|
||||
former loser (no blocking state left) and consuming cleanly.
|
||||
Stamped ADR-008 §5 + §7 + ADR-019 §1.
|
||||
|
||||
Drive-by fix: `alkstore-contract-suite/Cargo.toml`'s tokio dep
|
||||
gained the `macros` feature — a pre-existing break (since 7f749ac
|
||||
added the dep without it) left the crate's own
|
||||
`tests/suite_harness.rs` target failing to compile, which failed
|
||||
`cargo test -p alkstore-contract-suite` and the workspace gate on
|
||||
HEAD before this task. Test-side non-event (ADR-017 §2 class 4);
|
||||
harness target green (3 tests).
|
||||
|
||||
Verification: `cargo test -p alkstore-sqlite -p
|
||||
alkstore-postgres` green (SQLite lib 121 + suite 23/23 +
|
||||
harness-shape; pg lib 189 + suite 23/23 against the harness
|
||||
server on :15432), server-less pg rows skip cleanly, full
|
||||
workspace `cargo test` green (12 binaries), `cargo clippy
|
||||
--workspace --all-targets -- -D warnings` clean, `cargo fmt
|
||||
--check` clean. Stability: 13 clean runs of the pg suite's lock
|
||||
rows/full suite as recorded in Notes.
|
||||
Reference in new issue
Block a user