pg_lease — Invariant → Test Mapping

Stage-09 regression suite (test/sql/pg_lease.sql). Test IDs are the comment banners in the test file. Regression tests are single-session; multi-session races belong to the stage-10 isolation suite, restart/crash to the stage-11 failure suite — noted below where that is the authoritative test.

SEMANTICS.md operations

Spec item Test
§4.1 Acquire fresh key (epoch 1, expiry) OPS-02
§4.1 Acquire denied while HELD (not_acquirable) OPS-04
§4.1 Blocking mode wait bound exhausted = timeout (57014) OPS-11
§4.1 Same-owner idempotent re-acquire (Issue 3) OPS-03
§4.2 Renew ok / non-holder / wrong epoch / unknown key OPS-06
§4.3 Release wrong owner / wrong epoch / ok / duplicate OPS-07, OPS-08
§4.3 Release after lapse = lapsed (review finding 2) OPS-10
§4.4 Inspect held / unleased / lapsed (lazy model, Issue 1) OPS-02, OPS-05, OPS-09
§5 Input constraints, §7 invalid_input OPS-01
§7 lapsed vs not_owner distinguishability OPS-06, OPS-09, OPS-10
§7 timeout vs non-blocking denial distinguishability OPS-04, OPS-11
§8 Transaction semantics: commit persists TXN-01
§8 Rollback undoes acquire / renew / release TXN-02, TXN-03, TXN-04
§9 Takeover of lapsed lease OPS-09
§10 Lapsed holder: renew and release fail; must re-acquire OPS-09, OPS-10

INVARIANTS.md

Invariant Regression test Authoritative stage
I1 Mutual exclusion OPS-04 (denied acquire while held); OPS-09 (post-lapse only) Stage 10 (simultaneous-acquire races)
I2 Epoch monotonicity INV-I2 chain 3→4→5; OPS-08 duplicate release leaves epoch; INV-I2/I9 7→8→9; OPS-09 takeover epoch 2 regression
I3 Fencing effectiveness epoch_mismatch on renew/release with stale epoch (OPS-06, OPS-07); consumer-side rejection is a caller convention, specified S4/S10 regression (spec-level)
I4 Ambiguity window bounded OPS-09 (lapse observable immediately after expiry; inspect reports unowned) regression; window bound A1/A2 stated at stage 16
I5 Takeover liveness OPS-09 (takeover succeeds after TTL without holder action) regression
I6 Atomicity of transitions TXN-02/03/04 (all-or-nothing under rollback) regression; race-level in stage 10
I7 No client clock trust INV-I7 (no operation accepts a timestamp; lapse governed by server clock) regression (structural)
I8 Renewal preserves identity and epoch OPS-03 (idempotent re-acquire), OPS-06 (renew ok keeps epoch 1) regression
I9 Restart survival — Stage 11 (crash/restart suite); epoch durability structurally via WAL-backed table
I10 Fail-closed OPS-01 (no rows after invalid ops); denied ops leave state unchanged (OPS-04, OPS-06, OPS-07) regression
I11 Key independence INV-I11 regression; cross-key races in stage 10

Notes

  • OPS-01 also asserts the invalid-input block leaves zero rows (I10).
  • Timestamp masking (in_future flags) keeps expected output deterministic; exact expiry values are never asserted, only ordering vs server time.
  • Stage 10 (isolation): simultaneous acquire, renew-vs-takeover, release-vs-acquire, blocked-acquire wake behavior — I1, I4, I6, I11 races.
  • Stage 10 suite: test/specs/*.spec via make installcheck — compete (I1 single-winner, all start orders), races (renew/release vs acquire/takeover: I1, I3), stale-client (I2, I3 post-takeover rejection), rollback-race (S8, I6: blocked acquirer resolved by COMMIT/ROLLBACK of the competing transaction — ordering proven by <waiting ...> serialization, not sleeps), independent-keys (I11).
  • Waiter wake (test/wait-wake.sh, make check-wait): a blocking acquirer must observe a release by another session within its wait bound — S4.1 blocking mode. Not expressible in isolationtester (the waiter sleeps on a timer, not a lock); asserted via two concurrent sessions with a generous bound, so it tests ordering, not timing.
  • Stage 11 (failure): crash/restart (I9, D1–D3), session termination, resource-exhaustion fail-closed behavior.