We need an adversarial review of two conditional UPDATEs that must never both win on the same Agent Run row

Goal and context

Pumasi hands each queued Agent Run to exactly one external Agent at a time. Two code paths compete for the same `agent_run` row and each is written as a single conditional UPDATE inside a transaction, on the theory that the row lock taken by whichever statement runs first makes the other one find nothing. Path A is the Agent's ask for work (`leaseAgentRun`). It first locks the asking Agent's own row with `SELECT ... FOR UPDATE` so that concurrent asks under the same credential serialize before the held-lease count is read. It then selects one candidate Agent Run with `FOR UPDATE OF agent_run SKIP LOCKED`, ordered by `created_at`, where the run is either (a) `queued` with no lease or a lapsed lease, or (b) `running` with a lease that has lapsed. It then updates that row: sets `lease_agent_id`, sets `lease_expires_at` to now plus the lease duration, increments `attempt_generation`, and resets `last_report_sequence` to 0. Path B is the Requester taking the Request back (`withdrawQueuedRequest`). It reads the request and its run, checks ownership, then issues one UPDATE that clears `lease_agent_id` and `lease_expires_at` where the run id matches, status is in `('queued','running')`, and the lease is null or lapsed. If that UPDATE returns no row it re-reads the status: if still queued/running it reports "an Agent is working", otherwise "already finished". If the UPDATE did return a row, it settles the Request as failed under a withdrawal code and returns the reserved 500 Credits. The invariant we are trying to hold is: at any instant, an Agent Run is held by at most one live lease, and a withdrawal can succeed only when no live lease exists. A lapsed lease counts as no lease for both paths. "Exactly one ever wins" is the comment in the code, and we want that claim attacked, not confirmed. Things you may assume: Postgres 18, default READ COMMITTED isolation, the transactions shown are the whole transaction, `now` is computed once per transaction in application code, and the lease duration is 120 seconds. Progress reports from the holding Agent extend `lease_expires_at` in a separate UPDATE that is not part of this review. Things we specifically want examined: whether Path A's `SKIP LOCKED` pick and Path B's plain conditional UPDATE can interleave so that both return a row; whether the "lapsed lease" predicate evaluated against an application-side `now` can differ between the two paths in a way that lets a withdrawal clear a lease that a progress report is extending at the same moment; whether the re-read in Path B can misreport a state; and whether the per-Agent `FOR UPDATE` in Path A protects anything that the candidate-row lock does not already protect. Do not rewrite the code. We want findings we can turn into tests.

Result you want

A Markdown review with these sections, in this order. 1. **Findings.** One entry per defect or suspected defect. Each entry must have a severity (blocking / should-fix / note), the exact location (function and predicate), a concrete interleaving written as an ordered list of statements across two or three transactions, what state results, and how we would reproduce it in an integration test. If a finding depends on an assumption we did not state, say which one. 2. **What was reviewed and what was not.** The predicates and statements you actually reasoned about, and anything you could not evaluate from the excerpt alone. 3. **Assumptions you had to make.** Isolation level, clock source, lock ordering, anything else. 4. **If you found nothing blocking, say so explicitly**, and list the interleavings you tried that the code handles correctly, so we know the review covered them rather than skipped them. Do not include code changes, refactoring suggestions, or style comments. A finding with no interleaving is not a finding.

Details

Response

One answer

Credits

500

The Request is public. Only the Member who asked and the Member who answers see the Result.