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

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

Then, in the target database:

```sql
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

```sql
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

```sql
-- 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
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):

```sh
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 1/4/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.