# pg_lease — Semantics Implementation-independent specification. It defines externally observable behavior only; data representation, function signatures, and internal mechanisms are chosen later and must not alter this contract. ## 1. Problem Multiple clients (sessions, workers, nodes) need temporary, exclusive ownership of a named resource, such that: - Ownership survives as long as — and only as long as — the owner keeps it alive. - A holder that stops participating (crash, hang, network loss) does not block the resource forever: ownership eventually becomes acquirable by others. - A former owner that continues acting after losing ownership can be detected, so its actions can be rejected (fencing). - All state lives in PostgreSQL and inherits its transactional guarantees. Advisory locks provide the lifetime-scoped version of this (ownership = session lifetime) but no time bound, no fencing, and poor pool behavior. pg_lease provides the time-scoped primitive. ## 2. Terminology - **Lease key** — a caller-chosen name identifying the resource being owned. Keys live in one namespace per database. - **Holder** — the client that currently owns a lease; identified by a caller-supplied **owner identity**. - **TTL** — the maximum age of a lease grant or renewal. Ownership lapses when not renewed within TTL. - **Epoch (fencing token)** — a monotonically increasing counter per lease key, incremented on every ownership transition. Revealed to owners so third parties can reject actions from stale owners. - **Expiry** — the point in time, computed from the database server's clock, at which an unrenewed lease lapses. - **Lapsed lease** — a lease whose expiry has passed and which has not yet been acquired by a new holder. ## 3. State model For each lease key, the primitive exposes a state in: - **FREE** — no holder; anyone may acquire. - **HELD(owner, epoch, expires_at)** — owned by `owner` until `expires_at`. - **LAPSED(former epoch)** — the previous grant's expiry has passed; the key is not owned but retains its epoch counter. Time authority: **the database server's clock exclusively**. The primitive never accepts a client-supplied timestamp as a statement about the current time. All expiry comparisons use server time. The epoch counter for a key never resets and never decreases, including across lapses and manual releases. ## 4. Operations Four operations. Signatures and SQL types are implementation choices. ### 4.1 Acquire - **Inputs:** lease key; owner identity; TTL. - **Behavior:** atomically transitions the key to HELD for this owner if and only if its current state is FREE or LAPSED. On success, sets expiry = server_now + TTL and increments the epoch. - **Outputs:** success/failure; on success, the granted epoch and the expiry time. - **Modes:** blocking (wait until acquirable) and non-blocking (return immediately). A wait-timeout bound is permitted in the blocking mode. - **Idempotent re-acquire:** an acquire by the _same_ owner identity while already HELD by that owner MAY either fail or extend-with-new-epoch; which one is a specification decision that must be fixed before PROTOTYPE exits. It MUST NOT return a stale epoch or extend without changing the epoch. ### 4.2 Renew (heartbeat) - **Inputs:** lease key; owner identity; epoch; TTL. - **Behavior:** if the key is HELD by this owner with this epoch and has not lapsed, sets expiry = server_now + TTL. Otherwise fails. - **Outputs:** success (with new expiry) or failure (`not_owner`, `lapsed`, or `epoch_mismatch` per 7). - A renewal never changes the epoch. - A renewal submitted after lapse fails; the owner must re-acquire (getting a new epoch) to continue. ### 4.3 Release - **Inputs:** lease key; owner identity; epoch. - **Behavior:** if the key is HELD by this owner with this epoch, transitions to FREE (or LAPSED; equivalent observably — unowned) and increments the epoch. Otherwise fails. - **Outputs:** success or failure (`not_owner`, `lapsed`, or `epoch_mismatch` per 7). ### 4.4 Inspect - **Inputs:** lease key. - **Behavior:** reports current observable state: unowned or held(owner, epoch, expiry). - **Outputs:** the state. - Inspect is advisory-only: a HELD report past expiry without a lapse event is not a violation if the primitive defines lapse as evaluated-on-access (lazy expiry). The implementation must document which expiry evaluation model it uses (lazy, eager, or hybrid) and all operations must be consistent with that model. ## 5. Inputs (constraints on callers) - Lease key: non-empty, caller-chosen, unique per database. - Owner identity: non-empty, stable within one holder's lifetime. Two concurrent clients MUST NOT share an identity; doing so voids guarantees (see 10). - TTL: positive. Minimal useful TTL is bounded below by operation latency; the implementation documents a recommended minimum, but correctness never depends on a particular TTL. ## 6. Outputs - Acquire: granted/denied; epoch; expiry. - Renew: renewed/denied; expiry. - Release: released/denied. - Inspect: state. - Errors are distinguishable by cause (see 7). ## 7. Errors Every failure is one of: - `not_acquirable` — key HELD by another owner (non-blocking acquire). - `timeout` — blocking acquire exceeded its wait bound. Raised as an error (SQLSTATE 57014), so it is distinguishable from the non-blocking denial, which returns not-acquired. - `not_owner` — renew/release caller holds no live lease: unknown key, free key, or a key held by a different owner. - `lapsed` — renew/release caller matches the most recent holder identity but the lease has expired; the caller must re-acquire (getting a new epoch) to continue. - `epoch_mismatch` — renew/release presented a stale epoch. - `invalid_input` — empty key/identity, non-positive TTL. Error causes must be distinguishable from one another: a lapsed holder MUST be able to tell that its lease lapsed (vs. never held) so it can stop acting — hence `lapsed` vs `not_owner`. Check precedence for renew/release (documented): holder check first (`not_owner`), then lapse (`lapsed`), then epoch (`epoch_mismatch`). ## 8. Transaction semantics - Each operation is atomic: it either fully applies or has no effect. - An operation's effects are immediately visible to subsequently started transactions in every session (read-committed or stronger). - If an operation runs inside a caller transaction that later aborts, the lease state change is undone together with the transaction, **except** where the implementation deliberately uses non-transactional mechanisms (e.g., session-scoped locks); any such divergence MUST be documented and MUST NOT create a state where two owners believe they hold the same lease. - Acquire must be linearizable: of concurrent acquirers, exactly one wins; all others observe not_acquirable or wait. - Snapshot visibility (clarification, extension review 2026-09-22): the defined single-winner and liveness guarantees assume READ COMMITTED. Under REPEATABLE READ / SERIALIZABLE, a caller reads its transaction snapshot: state committed after the snapshot (e.g., a lease freed while a blocking acquire polls) is not observed, so a waiter may report not_acquirable for a free key, or the transaction may abort with a serialization error. This is ordinary PostgreSQL snapshot semantics, not a primitive defect; blocking acquire should run in READ COMMITTED transactions. ## 9. Concurrency semantics - **Single-winner:** at most one holder holds a key at any server-time instant within the skew bounds of 10. - **Takeover:** acquire during LAPSED succeeds; the new epoch is strictly greater than all previous epochs for the key. - **Renew-vs-takeover race:** a renewal and an acquire by different clients race only through atomic transitions; the primitive guarantees that no interleaving produces two holders. The loser observes its documented error. - **Writers of side effects** (the point of fencing): any party performing guarded actions must require the caller to present the current epoch; after any ownership transition, the previous epoch is rejected. - Waiters: blocking acquires are served without starvation guarantees; ordering among waiters is unspecified unless the implementation documents one. ## 10. Ownership semantics - Ownership is defined by server time: a holder owns a lease from its acquire (or last successful renewal) until expiry. - **Skew bound:** because the database server's clock is the sole authority and every decision happens in the database, client clock skew is irrelevant to correctness. What remains is server-internal time consistency; the primitive assumes a single PostgreSQL instance's clock for the primary. The primitive does NOT provide safety across multiple databases or a primary/replica failover boundary — see FAILURE-MODEL.md. - **Lapsed holder:** after expiry, the former owner's renewals fail and any guarded action with the old epoch must be rejected. The former owner gets `lapsed` (or `not_owner`/`epoch_mismatch`) and must stop. - **Shared-identity misuse:** if two clients use one identity, the primitive treats them as one holder; no guarantee is made about which acts. ## 11. Durability requirements See FAILURE-MODEL.md. Summary: lease state must survive server restart; the primitive must specify, per state element, whether it is transactionally durable. ## 12. Non-goals Exactly the research non-goals (see `candidates/pg-lease.md`): no distributed consensus; no exactly-once execution; no scheduler/worker; no multi-database or cluster-wide leases; no guarantee against a hostile owner that ignores fencing rejection; no API shape fixed by this document beyond the four operations' observable contracts. ## 13. PostgreSQL version assumptions - The minimum supported version is not yet fixed; it must be set at the Architecture stage based on mechanisms chosen, recorded in `docs/COMPATIBILITY.md`, and justified. - The specification assumes only: transactional DML, unique constraints, row locking, server-side clock access, and advisory locks — all present in every currently supported PostgreSQL major version. No reliance on undocumented behavior is permitted (root AGENTS.md section 15).