pg_lease — Invariants

Properties that must hold for every execution, every schedule, and every failure sequence. Tests (workflow stages 09–11) must map to these.

I1. Mutual exclusion (safety)

At any server-time instant, at most one holder holds a given lease key, except during an ambiguity window bounded by the expiry-evaluation model (see I4 and FAILURE-MODEL.md §A1).

I2. Epoch monotonicity

For each lease key, epochs are strictly increasing across all ownership transitions (acquire, takeover, release). No observation ever returns an epoch smaller than one previously returned for that key.

I3. Fencing effectiveness

Any guarded action checked against the current epoch succeeds only for the current holder’s epoch. After a transition, the prior epoch is always rejected.

I4. Ambiguity window

A lapsed holder and its successor may both believe they hold the lease only within the interval between expiry (server clock) and the successor’s acquire. Outside this window, beliefs converge: the lapsed holder’s operations fail. The implementation must state the maximum window implied by its expiry-evaluation model, and it must be finite and bounded by a documented quantity (e.g., time to next access).

I5. Liveness of takeover

A lease whose holder stops renewing becomes acquirable within TTL plus a documented, finite detection bound (the expiry-evaluation model’s maximum stale-state age). There is no schedule in which a non-renewing holder blocks acquisition indefinitely.

I6. Atomicity of transitions

Acquire, renew, and release are atomic with respect to each other and to inspect. No partial state is observable.

I7. No clock trust in clients

No operation accepts a client timestamp as authority over expiry. All expiry decisions derive from the database server’s clock.

I8. Renewal preserves identity and epoch

A successful renewal extends expiry only for the presented (key, identity, epoch) triple; it never changes the epoch and never transfers ownership.

I9. Restart survival

All observable lease state (holders, epochs, expiries) survives a clean server restart. Epochs never regress across restarts (see FAILURE-MODEL.md).

I10. Fail-closed errors

Every failed operation leaves lease state unchanged. A denied renew/release never mutates state; a denied acquire never mutates state (except, where documented, waiter bookkeeping that is externally invisible).

I11. Key independence

Operations on different lease keys never affect each other’s state, epochs, or outcomes.