166 lines
8.1 KiB
Markdown
166 lines
8.1 KiB
Markdown
---
|
|
id: suite-lock-rows
|
|
name: Contract-suite rows — lock TTL/expiry re-acquisition + concurrent try_lock loser
|
|
status: completed
|
|
depends_on: []
|
|
scope: narrow
|
|
risk: medium
|
|
impact: phase
|
|
level: implementation
|
|
tags: [wave-5, contract-suite, locks]
|
|
---
|
|
|
|
## Description
|
|
|
|
Add the named-locks contract rows to
|
|
`alkstore-contract-suite/src/properties.rs` and wire them into both
|
|
engines' suite targets, discharging two backlog rows
|
|
(core-contract.md §Verification backlog): "Named-lock TTL/expiry
|
|
re-acquisition on SQLite" (pinned on pg by the POC's lock probe; on
|
|
SQLite it rests on the forked substrate's lock machinery — the suite
|
|
pins both engines to identical behavior) and "Concurrent `try_lock`
|
|
loser/error behavior on SQLite" (the substrate's busy-path under lock
|
|
contention is the thing to pin — the pg side returns cleanly).
|
|
|
|
Rows to add:
|
|
|
|
- **`lock_ttl_expiry_and_reacquisition`** — the ADR-008 §7 guarantee
|
|
row: mutual exclusion bounded by TTL + renewal. Pin: a held lock
|
|
excludes a second acquirer (`None`); after TTL expiry exclusion
|
|
lapses *silently* (no revocation event, no error — a second owner
|
|
acquires); the original holder's post-expiry `renew` is refused
|
|
(`false` — the deadline-lapse refusal, ADR-010 §2's uniform
|
|
predicate shape on the lock handle); `release` on the second owner
|
|
frees the name for a third acquirer. Short TTL (1 s) + tolerance
|
|
sleeps — sequential single-store, fits the determinism posture.
|
|
- **`concurrent_try_lock_loser_is_a_value`** — contention posture:
|
|
with a lock held, contender `try_lock` calls return the clean
|
|
no-work value (`None`) on **both** engines — never a `Database`
|
|
error, never a busy-throw surfacing (the SQLite substrate's
|
|
busy-path is the risk site; the pg side is the reference behavior).
|
|
Drive several contenders sequentially against one held lock, and a
|
|
release-then-contend cycle proving the loser path leaves no state
|
|
that blocks a later acquire.
|
|
|
|
Risk note: what the SQLite busy-path *actually* returns under
|
|
contention is the open question this row exists to answer — if it
|
|
surfaces `Database` where pg returns `None`, that is a real
|
|
conformance finding: stop, record it in Notes, and raise it (an
|
|
engine fix or an ADR-level asymmetry call) rather than pinning the
|
|
divergence silently.
|
|
|
|
## Acceptance Criteria
|
|
|
|
- [x] Two rows exist, version-stamped (ADR-008 §7, ADR-019 §1,
|
|
ADR-023 §2 as applicable)
|
|
- [x] Rows wired into both engines' `contract_suite.rs` targets
|
|
- [x] SQLite column green server-less; pg column green against the
|
|
harness server
|
|
- [x] Any engine divergence found is recorded in Notes with its
|
|
disposition (fix or documented asymmetry) — not pinned silently
|
|
- [x] `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 (lock
|
|
TTL/expiry re-acquisition; concurrent try_lock loser)
|
|
- docs/architecture/decisions/008-contract-v1-pinning.md §7
|
|
- docs/architecture/decisions/019-mechanism-handle-surfaces.md §1
|
|
- docs/architecture/engine-sqlite.md (the substrate's lock machinery)
|
|
|
|
## Notes
|
|
|
|
> 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
|
|
|
|
> 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. |