ADR-013: Durable Run Leases and Guarded Finalization¶
Status¶
Accepted. Queue storage keeps the same run_lease invariant, but the physical attempt identity is carried by queue-storage claim / lease state rather than by mutating a single canonical jobs heap row.
Context¶
The earlier completion contract allowed a stale worker to finalize the wrong running attempt if a job had been rescued, reclaimed, and started again before the old completion reached Postgres.
That made completion correctness too weak for further optimization work, especially batching. A batched finalizer is only safe if the database can distinguish "the current running attempt" from "an old completion arriving late".
The TLA+ models already treated running attempts as lease-bearing identities, but the Rust runtime still needed a durable database-level token to match that model.
Decision¶
Add a monotonic run_lease to the running attempt identity and require all heartbeat/finalization/callback state transitions to match on:
idstate = 'running'run_lease
The runtime increments run_lease on every claim to running. Local in-flight state is keyed by (job_id, run_lease).
Finalization Rule¶
Finalization succeeds only if the current storage state still matches the claiming attempt's lease. If the guarded transition affects zero rows, the result is stale and must be discarded.
Batched Completion¶
Completed outcomes may be flushed in batches, but local in-flight tracking and capacity are not released until the batch flush acknowledges either:
- successful guarded transition, or
- stale rejection (
rows_affected = 0)
This keeps shutdown drain, heartbeat, and stale-completion safety aligned.
Consequences¶
Positive¶
- Prevents stale completions from mutating a newer running attempt
- Aligns the Rust runtime with the existing correctness model
- Makes lease-safe batched completion possible
- Allows heartbeat and cancellation to address exact running attempts
Negative¶
- Every claim now mutates an additional column
- Runtime state is slightly more complex because local tracking is per-attempt rather than per-job
- Any code path that touches running jobs must propagate the lease token
Notes¶
attempt is not used as the safety guard because it has ABA holes: snooze and admin retry can reset or decrement it. run_lease is monotonic and only advances on a new running claim, which makes it suitable as the durable attempt identity.
Relationship to ADR-019¶
The run_lease guard decision carries into queue storage unchanged. Under ADR-019, run_lease becomes the second component of the composite key (job_id, run_lease) identifying {schema}.active_leases and {schema}.attempt_state rows. Every heartbeat, flush-progress, register-callback, complete, and rescue path still matches on both columns; stale completions are rejected because the UPDATE matches zero rows when the lease row has been deleted or replaced. The AwaSegmentedStorageRaces TLA+ model checks that stale run_lease commits cannot land a lease in a retired segment, and AwaSegmentedStorageTrace replays concrete test sequences to validate the guard end-to-end. See ADR-019.
Relationship to ADR-042¶
ADR-042 exposes guarded completion inside a caller's PostgreSQL transaction. The runtime reconciles the attempt token against receipt or materialized-lease authority before interpreting the handler result. After a bounded database outage it may release heavyweight local capacity, but the durable attempt remains open for rescue and is never converted to a retry or completion without evidence. If rescue has already replaced the run lease, finalization raises a stale-attempt error so the application writes and the rejected completion cannot commit independently.