pg_lease — Failure Model

Implementation-independent statements of durability, failure behavior, and recovery. Tests must map to each item marked TESTABLE.

1. Durability requirements

  • D1 (TESTABLE). Lease state (holder, epoch, expiry) is transactionally durable: after a clean server restart, every key’s state is exactly what it was at the last committed operation before shutdown.
  • D2 (TESTABLE). Epochs are durable and never regress across restart: the epoch observed after restart is greater than or equal to the last pre-restart epoch.
  • D3. Expiry survives restarts in effect: a lease that would have lapsed during downtime is lapsable immediately after recovery — downtime does not extend ownership.
  • D4. If the implementation includes any non-durable acceleration (in-memory wait queues, caches), losing it may degrade performance but MUST NOT violate any invariant in INVARIANTS.md.

2. Failure behavior (per failure mode)

Failure mode Required behavior
Holder session terminates (clean disconnect) (TESTABLE) The lease does not vanish and is not instantly freed; it lapses at expiry per the normal model. If the implementation can also offer immediate release on session death, that is an optional documented behavior — but TTL lapse must work with the session merely hung, where no death signal exists.
Holder hangs / network partitions (session alive) (TESTABLE) Renewals stop; the lease lapses at expiry; takeover succeeds per I5. This is the core scenario advisory locks cannot handle.
Operation transaction aborts (TESTABLE) The operation’s state change is rolled back with the transaction; the pre-operation state stands; no invariant is violated. Documented non-transactional mechanisms (if any) must still satisfy I1–I11.
Client crashes mid-operation Same as abort: either the operation applied or it did not; no partial state (I6).
Server crash (unclean) (TESTABLE) After crash recovery, state is the last durably committed state (D1–D2). Leases that lapsed during downtime lapse immediately (D3).
Server restart (clean) Same as unclean crash from the spec’s perspective: durable state, epochs never regress.
TTL shorter than operation latency (TESTABLE) The holder experiences lapse mid-work; its renewals/operations fail with lapsed; correctness is preserved — a too-short TTL is a liveness mistake by the caller, never a safety violation.
Clock discontinuity on the server (TESTABLE) The primitive’s safety must not depend on wall-clock monotonicity assumptions beyond what PostgreSQL itself guarantees. The implementation must document which clock function it uses and how it bounds (or fails to bound) discontinuity effects; if discontinuity can break safety, that must be stated here, not hidden.
Resource exhaustion (locks, connections, disk) Standard PostgreSQL failure semantics apply; the primitive fails closed (I10).
Primary/replica failover OUT OF SCOPE for safety claims: leases on a failed primary may be observed stale on a replica and epochs/state after failover depend on replication semantics. The primitive documents this boundary explicitly and makes no cross-failover safety guarantee in its first specification.

3. Recovery behavior

  • R1 (TESTABLE). After any restart, keys in HELD state at the durable point resume their TTL countdown against server time; if expiry already passed, they are lapsable immediately upon first access (or eagerly, per the expiry-evaluation model).
  • R2. After restart, former holders re-establish by renewing or re-acquiring; a holder whose durable state shows it lapsed during downtime receives lapsed on renewal.
  • R3. Recovery requires no user-driven repair step: no manual cleanup, no re-initialization. The primitive is self-recovering for all failure modes in §2.

4. Ambiguity accounting (ties to INVARIANTS I4)

The implementation must state, as a specification-level constant or documented bound:

  • A1 — the maximum interval during which a lapsed holder’s belief and a successor’s ownership coexist (expiry-evaluation latency).
  • A2 — the maximum interval a key can remain unowned-but-not-yet-lapsable after expiry (detection latency), which bounds takeover liveness (I5).

Both bounds must be finite, stated in the extension’s docs, and reflected in the concurrency test plan.

5. Explicitly unhandled (documented, not fixed)

  • A hostile owner that ignores fencing rejection: fencing enables rejection by guardians of guarded resources; it cannot stop the owner from writing somewhere that never checks the epoch. Documented as out of scope.
  • Safety across independent databases or across primary→replica promotion: out of scope (§2 failover row).