From 98de4a49cd02c656cd7657d553c27e41a7d4da16 Mon Sep 17 00:00:00 2001 From: "glm-5.3-flash" Date: Sat, 10 Oct 2026 06:58:54 +0000 Subject: [PATCH] =?UTF-8?q?Contract-suite=20lock=20rows=20(task=20suite-lo?= =?UTF-8?q?ck-rows):=20two=20version-stamped=20rows=20discharging=20the=20?= =?UTF-8?q?lock=20backlog=20rows=20=E2=80=94=20lock=5Fttl=5Fexpiry=5Fand?= =?UTF-8?q?=5Freacquisition=20(the=20ADR-008=20=C2=A77=20guarantee=20row:?= =?UTF-8?q?=20a=20held=20lock=20excludes=20a=20second=20acquirer=20(conten?= =?UTF-8?q?der=20None);=20after=20a=201=20s=20TTL=20the=20exclusion=20laps?= =?UTF-8?q?es=20silently=20=E2=80=94=20no=20revocation=20event,=20no=20err?= =?UTF-8?q?or=20=E2=80=94=20and=20a=20second=20owner=20acquires;=20the=20o?= =?UTF-8?q?riginal=20holder's=20post-expiry=20renew=20is=20refused=20(fals?= =?UTF-8?q?e,=20the=20lost-it=20arm);=20the=20second=20owner's=20release?= =?UTF-8?q?=20frees=20the=20name=20for=20a=20third=20acquirer,=20which=20c?= =?UTF-8?q?onsumes=20cleanly;=20tolerance-sleep=20posture,=20state=20outco?= =?UTF-8?q?mes=20only;=20ADR-008=20=C2=A77=20+=20ADR-019=20=C2=A71,=20dura?= =?UTF-8?q?tion-guard=20legs=20cross-referenced=20to=20duration=5Frefusal?= =?UTF-8?q?=5Fon=5Fnon=5Fpositive=5Fttl)=20and=20concurrent=5Ftry=5Flock?= =?UTF-8?q?=5Floser=5Fis=5Fa=5Fvalue=20(the=20contention=20posture:=20four?= =?UTF-8?q?=20sequential=20contenders=20=E2=80=94=20two=20owners,=20repeat?= =?UTF-8?q?ed=20=E2=80=94=20against=20a=20held=20lock=20all=20land=20the?= =?UTF-8?q?=20clean=20None=20value,=20never=20Database,=20never=20a=20busy?= =?UTF-8?q?-throw;=20the=20backlog=20row's=20SQLite=20busy-path=20open=20q?= =?UTF-8?q?uestion=20answered:=20no=20divergence=20from=20the=20pg=20refer?= =?UTF-8?q?ence;=20release-then-contend=20cycle=20proves=20the=20loser=20p?= =?UTF-8?q?ath=20leaves=20no=20state=20blocking=20a=20later=20acquire,=20g?= =?UTF-8?q?ranted=20to=20a=20former=20loser=20and=20consumed=20cleanly;=20?= =?UTF-8?q?ADR-008=20=C2=A75=20+=20=C2=A77=20+=20ADR-019=20=C2=A71)=20?= =?UTF-8?q?=E2=80=94=20wired=20into=20both=20engines'=20suite=20targets=20?= =?UTF-8?q?(SQLite=20tokio=20tests,=20pg=20harness=5Frow!s),=2023=20rows?= =?UTF-8?q?=20per=20column=20up=20from=2021.=20Dispositions=20in=20Notes:?= =?UTF-8?q?=20no=20divergence=20found=20(no=20fix/ADR=20call=20needed),=20?= =?UTF-8?q?ADR-023=20=C2=A72=20excluded=20from=20stamps=20(its=20guard=20p?= =?UTF-8?q?roperty=20is=20the=20duration-refusal=20row's,=20cross-referenc?= =?UTF-8?q?ed),=20the=20backlog=20parenthetical=20re-acquire-does-not-refr?= =?UTF-8?q?esh-TTL=20stays=20engine-pinned,=20renew-refusal=20asserted=20a?= =?UTF-8?q?fter=20the=20second=20owner's=20re-acquisition=20(strongest=20f?= =?UTF-8?q?orm),=20contenders=20distinct-owner=20only=20(same-owner=20re-a?= =?UTF-8?q?cquire=20grants=20per=20the=20inherited=20substrate=20shape),?= =?UTF-8?q?=20and=20one=20unreproducible=20first-cold-run=20pg=20failure?= =?UTF-8?q?=20recorded=20(message=20lost=20to=20truncation;=2013=20subsequ?= =?UTF-8?q?ent=20clean=20runs=20incl.=20concurrent=20SQLite+pg=20=E2=80=94?= =?UTF-8?q?=20no=20timing=20hazard=20identified,=20the=20lapse=20assertion?= =?UTF-8?q?s=20are=20post-sleep=20state=20outcomes).=20Drive-by:=20alkstor?= =?UTF-8?q?e-contract-suite's=20tokio=20dep=20gained=20the=20macros=20feat?= =?UTF-8?q?ure=20=E2=80=94=20a=20pre-existing=20compile=20break=20in=20the?= =?UTF-8?q?=20crate's=20own=20tests/suite=5Fharness.rs=20(since=207f749ac)?= =?UTF-8?q?=20failed=20the=20harness=20target=20and=20the=20workspace=20te?= =?UTF-8?q?st=20gate=20on=20HEAD;=20test-side=20non-event=20(ADR-017=20?= =?UTF-8?q?=C2=A72=20class=204).=20Verified:=20cargo=20test=20-p=20alkstor?= =?UTF-8?q?e-sqlite=20-p=20alkstore-postgres=20green=20(SQLite=20121+23+9,?= =?UTF-8?q?=20pg=20189+23=20vs=20harness=20server=20on=20:15432,=20server-?= =?UTF-8?q?less=20pg=20skips=20clean),=20workspace=20cargo=20test=20green?= =?UTF-8?q?=20(12=20binaries),=20clippy=20-D=20warnings,=20fmt=20clean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- alkstore-contract-suite/Cargo.toml | 2 +- alkstore-contract-suite/src/lib.rs | 5 +- alkstore-contract-suite/src/properties.rs | 157 ++++++++++++++++++++++ alkstore-postgres/tests/contract_suite.rs | 17 ++- alkstore-sqlite/tests/contract_suite.rs | 17 ++- tasks/suite-lock-rows.md | 104 ++++++++++++-- 6 files changed, 285 insertions(+), 17 deletions(-) diff --git a/alkstore-contract-suite/Cargo.toml b/alkstore-contract-suite/Cargo.toml index 6c56487..17e45bb 100644 --- a/alkstore-contract-suite/Cargo.toml +++ b/alkstore-contract-suite/Cargo.toml @@ -9,4 +9,4 @@ publish = false [dependencies] alkstore = { version = "0.1", path = "../alkstore" } serde_json = "1" -tokio = { version = "1", features = ["rt", "time"] } \ No newline at end of file +tokio = { version = "1", features = ["rt", "time", "macros"] } \ No newline at end of file diff --git a/alkstore-contract-suite/src/lib.rs b/alkstore-contract-suite/src/lib.rs index 2513c4a..4029558 100644 --- a/alkstore-contract-suite/src/lib.rs +++ b/alkstore-contract-suite/src/lib.rs @@ -38,8 +38,9 @@ pub mod version_stamp; pub use factory::StoreFactory; pub use properties::{ - duration_refusal_on_non_positive_ttl, enqueue_opts_resolution, extent_clamp_semantics, - in_tx_reads_see_own_writes, job_handle_validity_predicate, + concurrent_try_lock_loser_is_a_value, duration_refusal_on_non_positive_ttl, + enqueue_opts_resolution, extent_clamp_semantics, in_tx_reads_see_own_writes, + job_handle_validity_predicate, lock_ttl_expiry_and_reacquisition, name_validation_rejects_empty_and_reserved, outbox_enqueue_tx_commit_atomicity, payload_round_trip_stores_exact_encoding, payload_too_large_never_produced_on_sqlite, payload_too_large_produced_on_pg, publish_with_key_tx_commit_atomicity, diff --git a/alkstore-contract-suite/src/properties.rs b/alkstore-contract-suite/src/properties.rs index 1679124..2a651b6 100644 --- a/alkstore-contract-suite/src/properties.rs +++ b/alkstore-contract-suite/src/properties.rs @@ -525,6 +525,163 @@ pub async fn duration_refusal_on_non_positive_ttl(factory: &dyn StoreFactory) { factory.teardown().await.expect("factory teardown"); } +/// **Lock TTL/expiry re-acquisition** — the ADR-008 §7 guarantee row: +/// a held lock excludes a second acquirer (`None` — the loser value, +/// never an error); after the TTL elapses exclusion lapses *silently* +/// — no revocation event, no error anywhere — and a second owner's +/// acquire succeeds; the original holder's post-expiry `renew` is +/// refused (`false` — the deadline-lapse refusal of the handle's +/// uniform predicate shape); and the second owner's `release` frees +/// the name for a third acquirer. Short-TTL (1 s) stamps with the +/// tolerance-sleep posture (state outcomes asserted, never durations; +/// sequential single-store drive). +/// +/// Cross-reference: the duration-guard legs (`ttl <= 0` rejecting on +/// `try_lock`/`renew`) pin in `duration_refusal_on_non_positive_ttl` +/// (ADR-023 §2) — this row owns the TTL *lifecycle* (lapse, +/// silent-exclusion loss, re-acquisition, post-expiry refusal, and +/// name-freedom after release). +/// +/// Contract stamp: ADR-008 §7 (the locks guarantee row — mutual +/// exclusion bounded by TTL + renewal; expiry is a silent loss of +/// exclusivity, not an error; exclusivity resumes with +/// re-acquisition); ADR-019 §1 (the `Lock` handle surface the +/// refusals ride — repeatable `renew` with the lost-it `false`, the +/// consuming `release`). +pub async fn lock_ttl_expiry_and_reacquisition(factory: &dyn StoreFactory) { + let store = factory.open().await.expect("factory opens a store"); + + let holder = store + .try_lock("lapse", "a", 1) + .await + .expect("try_lock on a free name must not error") + .expect("the first acquire holds the free name"); + let contender = store + .try_lock("lapse", "b", 300) + .await + .expect("a contender's try_lock must not error"); + assert!( + contender.is_none(), + "a held lock excludes a second acquirer" + ); + + // TTL expiry (a 1 s stamp; the sleep is bounded well past the + // second-precision stamp's resolution): exclusion lapses silently + // — the second owner's acquire is a clean Ok(Some) with no error + // preceding it and no revocation event to observe. + past_stamp_sleep(2_500); + let second = store + .try_lock("lapse", "b", 300) + .await + .expect("the post-expiry acquire must not error (silent lapse, no revocation event)") + .expect("after TTL expiry exclusion has silently lapsed: a second owner acquires"); + + assert!( + !holder + .renew(300) + .await + .expect("renew errs only on storage failure, never on lapse"), + "the original holder's post-expiry renew is refused: the lost-it arm" + ); + + assert!( + second + .release() + .await + .expect("the second owner's release errs only on storage failure"), + "the second owner's release deletes its own row" + ); + let third = store + .try_lock("lapse", "c", 300) + .await + .expect("try_lock on the freed name must not error") + .expect("the released name is acquirable by a third owner"); + assert!( + third + .release() + .await + .expect("the third release errs only on storage failure"), + "the third owner releases its own row (no residue for teardown)" + ); + + factory.teardown().await.expect("factory teardown"); +} + +/// **Concurrent `try_lock` loser is a value** — the contention +/// posture: with a lock held, contenders' `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 this row pins; the pg side is the +/// reference behavior the suite drives first). Contenders are driven +/// sequentially against one held lock (several distinct owners, +/// including a repeat contender), and a release-then-contend cycle +/// proves the loser path leaves no state behind that blocks a later +/// acquire — the former loser acquires cleanly on an empty field. +/// +/// Cross-reference: the TTL-lapse arms of the loser value pin in +/// `lock_ttl_expiry_and_reacquisition` — this row owns the +/// *held-lock* loser path (the substrate's busy-path behavior is the +/// thing under test, the backlog row's open question). +/// +/// Contract stamp: ADR-008 §5 (the value-not-error rule — `try_lock` +/// returning `Option` is explicitly not a taxonomy item; a +/// loser `Database` error would be a contract violation); ADR-008 §7 +/// (the exclusion row the contention composes with); ADR-019 §1 (the +/// handle surface the winner's consuming `release` rides). +pub async fn concurrent_try_lock_loser_is_a_value(factory: &dyn StoreFactory) { + let store = factory.open().await.expect("factory opens a store"); + + let holder = store + .try_lock("contended", "holder", 300) + .await + .expect("try_lock on a free name must not error") + .expect("the first acquire holds the free name"); + + // Sequential contenders against the held lock: every loser sees + // the clean `None` value — a `Database` error on any of them is + // the busy-path finding this row exists to catch. + for attempt in 0..4u32 { + let owner = if attempt.is_multiple_of(2) { + "contender-1" + } else { + "contender-2" + }; + let out = store + .try_lock("contended", owner, 300) + .await + .expect("a contended try_lock must not error (no busy-throw surfacing)"); + assert!( + out.is_none(), + "a held lock must lose contenders the None value, not a granted lock" + ); + } + + // Release-then-contend: the loser path left no state — an + // immediate re-contend after release grants, to a former loser's + // owner, and consumes cleanly. + assert!( + holder + .release() + .await + .expect("the winner's release errs only on storage failure"), + "the winner's release deletes its own row" + ); + let winner = store + .try_lock("contended", "contender-1", 300) + .await + .expect("the post-release contend must not error") + .expect("the loser path left no state blocking a later acquire"); + assert!( + winner + .release() + .await + .expect("release errs only on storage failure"), + "the new winner releases cleanly (no residue for teardown)" + ); + + factory.teardown().await.expect("factory teardown"); +} + /// **`encode_payload` typed-failure round-trip** — enqueue and publish /// store the exact serde_json serialization of the input `Value` and /// decode back to `Value` equality; the helper's failure arm is typed diff --git a/alkstore-postgres/tests/contract_suite.rs b/alkstore-postgres/tests/contract_suite.rs index edeee48..90316be 100644 --- a/alkstore-postgres/tests/contract_suite.rs +++ b/alkstore-postgres/tests/contract_suite.rs @@ -163,9 +163,10 @@ async fn harness_ready() -> bool { mod rows { use alkstore_contract_suite::properties::{ - drop_rollback_leaves_no_ghosts, duration_refusal_on_non_positive_ttl, - enqueue_opts_resolution, extent_clamp_semantics, in_tx_reads_see_own_writes, - job_handle_validity_predicate, name_validation_rejects_empty_and_reserved, + concurrent_try_lock_loser_is_a_value, drop_rollback_leaves_no_ghosts, + duration_refusal_on_non_positive_ttl, enqueue_opts_resolution, extent_clamp_semantics, + in_tx_reads_see_own_writes, job_handle_validity_predicate, + lock_ttl_expiry_and_reacquisition, name_validation_rejects_empty_and_reserved, outbox_enqueue_tx_commit_atomicity, payload_round_trip_stores_exact_encoding, payload_too_large_produced_on_pg, publish_with_key_tx_commit_atomicity, queue_depth_reclaim_and_dead_letter, receiver_close_and_save_arms, @@ -207,6 +208,16 @@ mod rows { duration_refusal_on_non_positive_ttl, "row-duration-refusal" ); + harness_row!( + row_lock_ttl_expiry_and_reacquisition, + lock_ttl_expiry_and_reacquisition, + "row-lock-ttl-expiry" + ); + harness_row!( + row_concurrent_try_lock_loser_is_a_value, + concurrent_try_lock_loser_is_a_value, + "row-lock-loser-value" + ); harness_row!( row_payload_round_trip_stores_exact_encoding, payload_round_trip_stores_exact_encoding, diff --git a/alkstore-sqlite/tests/contract_suite.rs b/alkstore-sqlite/tests/contract_suite.rs index 080c056..311d1eb 100644 --- a/alkstore-sqlite/tests/contract_suite.rs +++ b/alkstore-sqlite/tests/contract_suite.rs @@ -67,9 +67,10 @@ impl StoreFactory for SqliteFactory { mod rows { use alkstore_contract_suite::properties::{ - drop_rollback_leaves_no_ghosts, duration_refusal_on_non_positive_ttl, - enqueue_opts_resolution, extent_clamp_semantics, in_tx_reads_see_own_writes, - job_handle_validity_predicate, name_validation_rejects_empty_and_reserved, + concurrent_try_lock_loser_is_a_value, drop_rollback_leaves_no_ghosts, + duration_refusal_on_non_positive_ttl, enqueue_opts_resolution, extent_clamp_semantics, + in_tx_reads_see_own_writes, job_handle_validity_predicate, + lock_ttl_expiry_and_reacquisition, name_validation_rejects_empty_and_reserved, outbox_enqueue_tx_commit_atomicity, payload_round_trip_stores_exact_encoding, payload_too_large_never_produced_on_sqlite, publish_with_key_tx_commit_atomicity, queue_depth_reclaim_and_dead_letter, receiver_close_and_save_arms, @@ -99,6 +100,16 @@ mod rows { duration_refusal_on_non_positive_ttl(&factory("row-duration-refusal")).await; } + #[tokio::test(flavor = "multi_thread")] + async fn row_lock_ttl_expiry_and_reacquisition() { + lock_ttl_expiry_and_reacquisition(&factory("row-lock-ttl-expiry")).await; + } + + #[tokio::test(flavor = "multi_thread")] + async fn row_concurrent_try_lock_loser_is_a_value() { + concurrent_try_lock_loser_is_a_value(&factory("row-lock-loser-value")).await; + } + #[tokio::test(flavor = "multi_thread")] async fn row_payload_round_trip_stores_exact_encoding() { payload_round_trip_stores_exact_encoding(&factory("row-payload-round-trip")).await; diff --git a/tasks/suite-lock-rows.md b/tasks/suite-lock-rows.md index 57350cd..a17f958 100644 --- a/tasks/suite-lock-rows.md +++ b/tasks/suite-lock-rows.md @@ -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 \ No newline at end of file +> 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. \ No newline at end of file