# 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).