Repository navigation
Land and landsignal DLQs fail a landing batch that Runway goes on to merge #819
Copy link
Copy link
Open
Labels
bugSomething isn't workingSomething isn't working
Description
Problem
A batch is reported failed, and its requests error, even though Runway merged the change onto the target branch.
Cause
failBatch (submitqueue/orchestrator/controller/dlq/dlq.go) moves any non-terminal batch to failed, landing included. A landing batch has already handed its outcome to Runway, so the reconciler cannot know whether the merge happened. Two DLQs reach failBatch while the batch is landing:
submitqueue-landDLQ. The Runway publish island's last step, so a lost ack, or an ambiguous publish error after the row was written, leaves Runway holding the MergeRequest. If later attempts then fail on a storage error, the message dead-letters.landsignalDLQ.landsignalholds Runway'sSUCCEEDED, but the batch compare-and-swap keeps failing on a storage fault. The DLQ payload contains the verdict, and the reconciler discards it.
When Runway's answer arrives later, landsignal sees a terminal batch, re-fans out, and acks. Nothing corrects the outcome.
Interleaving (TLC's shortest counterexample)
speculate: batch speculating → landing, publish to submitqueue-land
land: publish MergeRequest to runway-merge, then the attempt fails; retries exhaust → land DLQ
runway: merges, publishes SUCCEEDED
land DLQ: failBatch: landing → failed, fan out requests → error
landsignal: batch already terminal → ack, outcome unchanged
Why the obvious fixes are not enough
Found by model checking spec/submitqueue/landoutcome/LandOutcome.tla, which checks 24 design combinations:
- Skip
landingin the DLQ and wait for Runway. This trades the wrong answer for a batch that never finishes, when Runway's answer is itself the message that dead-lettered. - Re-send the MergeRequest from the DLQ. This is unsound against today's Runway, for two reasons:
- A stale
FAILEDcan win. Runway's first attempt dead-letters without pushing, so its DLQ honestly answersFAILED. The re-send then merges on a second attempt, and the earlierFAILEDis applied. - The replay is swallowed. A replayed answer reuses the request ID as its message ID and is deduped by the queue (the messagequeue: entity-ID message IDs + publish dedup silently drop wake-up events; use intent-scoped message IDs #352 class).
- A stale
- The only design that passes every property has four parts: the DLQ re-sends; Runway's DLQ checks the branch; Runway records its verdict per request ID; and answers do not dedup on the request ID alone. That gives Runway state, so cheaper designs are worth modelling first. Two candidates: the
landsignalDLQ applies the verdict it holds, andlandrecords "dispatched" before it publishes.
Acceptance criteria
- A dead letter on
submitqueue-landorlandsignalnever moves alandingbatch tofailedwhile the change can still land or has landed. - Every
landingbatch still reaches a terminal state. - Unit tests that interleave the DLQ with a late
SUCCEEDED, confirmed to fail before the fix. -
LandOutcome.tlaupdated to the chosen design.
Related: #818 (the same symptom through the speculate path).
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working
Activity
behinddwalls commentedon Oct 8, 2026
Runway-side companion: #820. No orchestrator-side fix can repair that one.
docs(rfc): propose model checking protocols with TLA+