Contents

• pg_lease
  • Status
  • Installation
  • Quick start
  • Public API
    • lease.acquire(key text, owner text, ttl interval, wait interval DEFAULT 0)
    • lease.renew(key text, owner text, epoch bigint, ttl interval)
    • lease.release(key text, owner text, epoch bigint)
    • lease.inspect(key text)
    • Errors
  • Semantic model
  • Concurrency behavior
  • Failure model
  • Examples
  • Limitations
  • Supported PostgreSQL versions
  • Testing
  • Benchmark methodology

pg_lease

PostgreSQL-native lease/ownership primitive: time-bounded ownership of a named resource that lapses unless renewed, with monotonic fencing epochs.

Status

Implements the specified semantics per ADR 0006. Passed workflow stages 09–15: regression suite, isolation suite, failure suite, wait-wake test, formal correctness audit (all 11 invariants PROVEN), benchmark baseline, and the Docker compatibility matrix (PG 14/15).

• Specification: specs/ (authoritative for behavior)
• Architecture: docs/adr/0006-pg-lease-architecture.md — pure SQL, lazy expiry, no C, no background workers, no advisory locks
• Benchmark analysis: benchmarks/pg_lease/ANALYSIS.md

Installation

Requirements: PostgreSQL 14 or later (see Supported PostgreSQL versions below). No compiler is needed; the extension is pure SQL.

cd extensions/pg_lease
make install          # copies control + SQL into the pgxs extension dirs

Then, in the target database:

CREATE EXTENSION pg_lease;

The extension is trusted: a non-superuser with CREATE privilege on the database can install and use it. Uninstall with DROP EXTENSION pg_lease — this destroys schema lease and all lease state, including fencing epochs; a re-install starts every key fresh at epoch 1.

Quick start

CREATE EXTENSION pg_lease;

-- Acquire (non-blocking by default)
SELECT acquired, epoch, expires_at
  FROM lease.acquire('job-42', 'worker-a1', interval '30s');
--  acquired | epoch |         expires_at
--  ---------+-------+------------------------------
--  t        |     1 | 2026-09-22 12:00:00.1+05     (server time + 30s)

-- Heartbeat: extend expiry, epoch unchanged
SELECT status, expires_at
  FROM lease.renew('job-42', 'worker-a1', 1, interval '30s');

-- Voluntary release (increments the epoch)
SELECT status FROM lease.release('job-42', 'worker-a1', 1);

-- Observe state
SELECT held, owner, epoch, expires_at FROM lease.inspect('job-42');

Worked pattern for a worker loop: acquire with a TTL well above the renewal interval, renew periodically, and treat any lapsed or epoch_mismatch result as “stop acting immediately; re-acquire if needed.” Fenced side effects should check the epoch the resource guard records against the epoch the holder presents.

Public API

All functions live in schema lease and are SECURITY DEFINER with a pinned search_path; the lease.leases table is extension-internal (REVOKE ALL ... FROM PUBLIC) — the functions are the only supported API.

lease.acquire(key text, owner text, ttl interval, wait interval DEFAULT 0)

→ (acquired boolean, epoch bigint, expires_at timestamptz)

• Takes exclusive ownership of a key whose state is FREE or LAPSED. Sets expiry = server time + ttl and a new epoch.
• Non-blocking (wait = 0): returns immediately. Held key → acquired = false, epoch/expires_at NULL.
• Blocking (wait > 0): polls (50 ms interval) until acquirable or the wait bound passes; on bound exhaustion raises timeout, SQLSTATE 57014. The two denial causes are distinguishable.
• Same-owner acquire of a lease it currently holds (unexpired): idempotent success, same epoch, expiry unchanged.

lease.renew(key text, owner text, epoch bigint, ttl interval)

→ (status text, expires_at timestamptz)

• Heartbeat. Extends expiry to server time + ttl; never changes the epoch.
• Statuses: ok; not_owner (unknown key, free key, or different owner); lapsed (the caller was the holder but the lease expired); epoch_mismatch (stale epoch).

lease.release(key text, owner text, epoch bigint)

→ (status text)

• Transitions a held lease to FREE and increments the epoch. Same statuses and meanings as renew (minus the expiry output).
• Check precedence for renew/release: holder check (not_owner), then lapse (lapsed), then epoch (epoch_mismatch).

lease.inspect(key text)

→ (held boolean, owner text, epoch bigint, expires_at timestamptz)

• Reports current observable state under lazy expiry: a HELD row past expiry reports as unowned.
• For held = false, epoch is the key’s current fencing counter: any action guarded by an epoch ≤ this value is stale, and the next grant carries a strictly greater epoch.
• A never-leased key returns zero rows (distinct from a released key’s one row with held = false).

Errors

Invalid input (NULL/empty key or owner, non-positive ttl, negative wait) raises invalid_input, SQLSTATE 22023, with DETAIL naming the violated constraints. All errors fail closed: no state change.

Semantic model

Authoritative: specs/SEMANTICS.md. Summary:

• States per key: FREE (unowned), HELD(owner, epoch, expires_at), LAPSED (previous grant expired; epoch counter retained). Epochs never reset or decrease, including across lapses, releases, and restarts.
• Time authority: the database server’s clock exclusively (clock_timestamp()). No operation accepts a client timestamp.
• Expiry model: lazy — state is a function of (stored row, server clock); every operation evaluates expiry before acting. There is no reaper; a lapsed lease is immediately acquirable by anyone.
• Every operation is one atomic statement: fully applied or not at all; effects commit or roll back with the caller’s transaction.

Concurrency behavior

Authoritative: SEMANTICS §8–§10; evidence: isolation suite (test/specs/*.spec) and the correctness audit.

• Single-winner: at most one holder per key at any server-time instant; concurrent acquires are serialized by row-level locking, and exactly one wins.
• Takeover: acquire of a LAPSED lease succeeds with an epoch strictly greater than all previous epochs for the key.
• Renew-vs-takeover and release-vs-acquire races resolve through the same atomic transitions; the loser always observes its documented error.
• Waiters: blocking acquires have no starvation or ordering guarantee.
• Transaction isolation: the defined guarantees assume READ COMMITTED (the default). Under REPEATABLE READ / SERIALIZABLE a caller reads its transaction snapshot, so a blocking acquirer may miss a lease freed after its snapshot began (reporting denial or aborting with a serialization error). Run blocking acquires in READ COMMITTED.
• Transaction discipline: an acquire/renew/release inside a transaction that aborts is undone; a blocking acquire holds a transaction open for its full wait.

Failure model

Authoritative: specs/FAILURE-MODEL.md; evidence: failure suite (test/failure-model.sh, 15 checks) and wait-wake (test/wait-wake.sh).

• Durable state: holder, epoch, and expiry are ordinary WAL-logged table data. After clean restart or unclean crash, the last committed state stands; epochs never regress.
• Downtime never extends ownership: a lease that would have lapsed during downtime is lapsable immediately on first access after recovery.
• Holder death/hang: the lease is not freed by session death; it lapses at expiry and is then takeover-able — including when the holder merely hangs (no death signal required).
• Lapsed holder: renew/release fail with lapsed; the former holder must re-acquire (new epoch) and any guarded action with the old epoch must be rejected by the resource’s guard.
• Too-short TTL: the holder experiences lapse mid-work (lapsed on renewal) — a liveness mistake by the caller, never a safety violation.
• Failover boundary: no safety guarantee across primary→replica promotion or across independent databases (documented non-goal).
• A hostile owner that ignores epoch checks is outside the primitive’s power: fencing enables rejection by guards of guarded resources.

Examples

-- 1. Safe retry loop: duplicate acquire returns the same epoch, so a
--    client that loses its result can re-ask without side effects.
SELECT acquired, epoch FROM lease.acquire('job-42', 'worker-a1', interval '30s');
SELECT acquired, epoch FROM lease.acquire('job-42', 'worker-a1', interval '30s');  -- same epoch

-- 2. Takeover of a dead holder's lease by a new owner (a1 stopped
--    renewing; its 10s TTL lapses; b2 blocks until it can take over).
SELECT acquired, epoch FROM lease.acquire('job-42', 'worker-a1', interval '10s');
SELECT acquired, epoch FROM lease.acquire('job-42', 'worker-b2', interval '30s', interval '15s');
-- returns acquired=t with a NEW epoch (2) once the old lease lapses

-- 3. The old owner is now fenced: its renew fails...
SELECT status FROM lease.renew('job-42', 'worker-a1', 1, interval '30s');   -- lapsed
-- ...and any guard that recorded epoch 1 rejects epoch-1 actions.

-- 4. Inspect as a fencing watermark.
SELECT held, owner, epoch FROM lease.inspect('job-42');
-- held=f rows expose the counter: epochs <= it are stale.

-- 5. Distinct keys never interact.
SELECT acquired FROM lease.acquire('job-43', 'worker-a1', interval '30s');  -- independent

A runnable concurrency demonstration (two sessions, wake-on-release) is in test/wait-wake.sh; multi-session races are proven in test/specs/.

Limitations

• One namespace per database; keys are plain text (non-empty).
• Lease rows persist forever (lapse is logical, not deletion); unbounded distinct-key growth is a caller data-management concern.
• No notification/callback on lapse or takeover; holders learn of loss only from lapsed/epoch_mismatch on their own operations or by polling inspect.
• Blocking acquire is a poll loop: wake latency is bounded by the 50 ms poll interval, and it holds a database connection and open transaction for the whole wait.
• No safety across primary→replica failover or across databases.
• Owner identity is a caller convention, not authentication: two clients sharing an identity void the guarantees.
• Server-clock discontinuities (time jumped backward/forward) affect expiry to the same extent they affect any clock_timestamp()-based logic; correctness relies only on single-server clock consistency.
• inspect is advisory-only and statement-snapshot consistent (STABLE).

Supported PostgreSQL versions

Extension	Min version	Tested versions	Evidence
pg_lease	14	14.24, 15.17 (Docker); 14.20, 15.15 (host, supplementary)	full test matrix per version

Per docs/COMPATIBILITY.md’s claim rule, only Docker-matrix-passed versions are claimed as supported. The implementation uses only mechanisms present and behaviorally identical across 14 and 15; no per-version code paths exist. Version 0.1.0 has no update path from earlier versions (none were released).

Testing

Authoritative (Docker, per ADR 0007):

sh docker/pg_lease/run.sh               # full matrix on PG 14 and 15
# single version:
PG_VERSION=15 docker compose -f docker/pg_lease/compose.yaml run --rm test

The matrix runs: build + install, regression suite, isolation suite (5 specs), failure suite (15 checks), and the blocking-acquire wait-wake test, each against a throwaway instance of the image’s own server binary.

Direct local runs (supplementary only; the failure suite requires the server version’s bin dir first in PATH):

make installcheck     # regression + isolation suites
make check-wait       # blocking-acquire wake test
make check-failure    # failure-model suite

Invariant→test mapping: test/INVARIANT-MAP.md; formal audit: test/CORRECTNESS-AUDIT.md.

Benchmark methodology

Authoritative: benchmarks/pg_lease/run-baseline.sh and benchmarks/pg_lease/ANALYSIS.md (results recorded per run in benchmarks/pg_lease/results/<timestamp>/ including a full environment record: PostgreSQL/pgbench versions, OS, CPU, storage, and relevant GUCs — fsync=on, synchronous_commit=on).

• W1-cycle: pgbench transactions of acquire+renew+release on private keys (end-to-end primitive cycle incl. commit), 3 ops/tx.
• W2-contend: single acquire attempts on 4 shared keys (pure primitive-statement cost and contention), 1 op/tx.
• Clients ¼/16; per-transaction latency logs; p50/p95/p99 computed from the pgbench log. Baseline (PG 15.15, Apple M1 Max, local socket): single uncontended operation ~39 µs p50; W1 cycle 368 µs p50 at 1 client; measured commit overhead dominates the cycle (~250 µs).
• The stage-14 optimization review (ANALYSIS.md) rejected all four proposals — each either targeted commit/fsync cost outside the extension, weakened specified durability/mutual-exclusion semantics, or lacked measurable support. No optimization was implemented; no performance claims are made beyond the recorded environment.