Prove serialization by message, not by execution - #12
Conversation
The failure-recovery demo asserted the serialization control file held exactly four events. A worker that loses its lease mid-operation leaves the replacement to execute the same message again, so a slower machine produces six, and the demo failed for the at-least-once behaviour the library documents and the crash and fencing proofs rely on. It failed five times on GitHub runners, on Node 24.15.0 as well as the lower floor, and passed on rerun, so the assertion was reporting the runner's speed rather than a durability property. The proof now asserts what the runtime guarantees: executions never overlap, every start has a matching finish, and exactly the two sent messages ran. The committed state check is unchanged, and it is the one that would catch a lost or doubled write. assertSerializedExecution moves into its own module so it can be tested at the lowest layer. The unit tests cover the retry, overlap, unfinished, and lost-message cases, and each rejection case fails when the rule is removed. The lease timing stays as it was. proveCrashRecovery and proveFencing depend on a short lease, so raising it to hide the retry would weaken them.
Greptile SummaryThe PR revises the failure-recovery serialization proof to distinguish execution attempts and tolerate documented at-least-once retries while continuing to reject overlap between surviving executions.
Confidence Score: 5/5The PR appears safe to merge. No blocking failure remains. Important Files Changed
Flowchart%%{init: {'theme': 'neutral'}}%%
flowchart TD
S[Read serialization events] --> P[Pair start and finish by message, attempt, and process]
P --> C{Every execution complete?}
C -- No --> F[Fail proof]
C -- Yes --> M{Expected messages observed?}
M -- No --> F
M -- Yes --> H[Select highest attempt per message]
H --> O{Surviving executions overlap?}
O -- Yes --> F
O -- No --> R[Return execution and retry details]
Reviews (4): Last reviewed commit: "fix: pair each start with its own finish" | Re-trigger Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| assert.equal( | ||
| open, | ||
| undefined, | ||
| `execution of ${event.messageId} overlaps the open execution of ${open}`, | ||
| ) | ||
| open = event.messageId |
There was a problem hiding this comment.
When a worker loses its lease while serialize is still running, a replacement starts the same message before the stale attempt writes its finish. The single open slot rejects that documented at-least-once interleaving as overlapping execution, causing the recovery demo to fail for the behavior this change is intended to accept.
Prompt To Fix With AI
This is a comment left during a code review.
Path: examples/failure-recovery/serialization.ts
Line: 34-39
Comment:
**Lease-loss retry triggers overlap assertion**
When a worker loses its lease while `serialize` is still running, a replacement starts the same message before the stale attempt writes its finish. The single `open` slot rejects that documented at-least-once interleaving as overlapping execution, causing the recovery demo to fail for the behavior this change is intended to accept.
---
For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.The first rule demanded strict alternation across the whole log, which rejects the case it was written to accept. The attempt that loses its lease is the one that was slow, so it is still running when the replacement starts, and both write to the control file. Overlap is now allowed only when a message ran more than once, which is the only thing that produces a stale owner. Without a retry the proof still demands strict serialization. The rule tracks open attempts per message, so a message may be open twice. The demo reports executions, retried, and overlapped instead of a hardcoded overlap: false, so a run says what it actually saw. Found by Greptile on the first commit. The stale-overlap case is now a test, and it fails against the alternation rule.
|
@greptileai review Valid finding, and it reproduces as a test. The attempt that loses its lease is the one that was slow, so it is still running when the replacement starts, and both write to the control file. The alternation rule rejected exactly the case this PR exists to accept. Fixed in fd29399: overlap is allowed only when a message ran more than once, since that is the only thing that produces a stale owner. Without a retry the proof still demands strict serialization. The rule now tracks open attempts per message, so one message may be open twice.
|
| if (!retried) { | ||
| assert.equal(concurrent, 1, "executions overlapped without a lost lease to explain it") | ||
| } |
There was a problem hiding this comment.
When one message retries while two different message IDs overlap, retried becomes true and skips the only concurrency assertion, causing the helper to report a successful serialization proof even though distinct messages for the same identity executed concurrently.
Prompt To Fix With AI
This is a comment left during a code review.
Path: examples/failure-recovery/serialization.ts
Line: 71-73
Comment:
**Retry masks cross-message overlap**
When one message retries while two different message IDs overlap, `retried` becomes true and skips the only concurrency assertion, causing the helper to report a successful serialization proof even though distinct messages for the same identity executed concurrently.
---
For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.Treating any retry as a licence to overlap let a real violation through: once one message retried, two different messages could run at the same time and the proof still passed. A retry excuses only the attempt it superseded. The rule now tracks which attempt of each message is the last one started, and asserts that at most one message has its surviving attempt open at any moment. Earlier attempts may overlap anything, because their writes are fenced. Found by Greptile on the previous commit. The case is now a test, and removing the assertion fails it along with the no-retry overlap case.
|
@greptileai review Valid again, and it reproduces as a test: with one message retried, the previous rule skipped the concurrency assertion entirely, so two different messages could run at the same time and still pass. Fixed in 59e4a4f. A retry excuses only the attempt it superseded. The rule tracks which attempt of each message started last and asserts that at most one message has its surviving attempt open at any moment. Earlier attempts may overlap anything, because their writes are fenced.
|
| const startedAt = openForMessage.pop() | ||
| open.set(event.messageId, openForMessage) | ||
| running -= 1 | ||
| if (startedAt === lastStartedAt.get(event.messageId)) surviving.delete(event.messageId) |
There was a problem hiding this comment.
When a stale attempt finishes after its replacement starts, openForMessage.pop() attributes that finish to the replacement and removes the replacement from surviving. A second message can then overlap that still-running replacement without triggering the assertion, so the serialization proof accepts concurrent surviving attempts.
Prompt To Fix With AI
This is a comment left during a code review.
Path: examples/failure-recovery/serialization.ts
Line: 71-74
Comment:
**Stale finish clears surviving attempt**
When a stale attempt finishes after its replacement starts, `openForMessage.pop()` attributes that finish to the replacement and removes the replacement from `surviving`. A second message can then overlap that still-running replacement without triggering the assertion, so the serialization proof accepts concurrent surviving attempts.
---
For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.Two attempts of the same message can both be writing to the control file at once: the superseded attempt keeps running until it notices the lost lease, and its finish can land after the replacement's start. The previous rule paired a start with whichever finish came next, so that late finish read as the replacement's, and a second message could then overlap a replacement that was in fact still running. Each event now carries the message's attempt and the writing process, so a start pairs only with the finish of that same execution. The proof still asserts one thing about the surviving attempts, that none of them overlap another message's surviving attempt, and lets a superseded attempt overlap anything, because its write is fenced out and the committed state is the assertion that proves it. Found by Greptile on the previous commit, and reproduced as a test: a superseded attempt that finishes after its replacement starts, followed by a second message that starts while the replacement is still running. Removing the overlap assertion fails that case and the no-retry case.
|
@greptileai review Valid, and it exposes the actual gap: the log recorded only Fixed in b201fe2. Each event now carries the message's attempt and the writing process (the actor already has New tests: a superseded attempt whose finish lands after its replacement starts, and a second message that overlaps that still-running replacement — the second one throws. Removing the overlap assertion fails both, plus the original no-retry case. |
1 participant
The failure-recovery demo's serialization proof asserted that the control file
held exactly four events. That is a claim about the machine's speed, not about
the runtime, and it has been failing on GitHub runners.
What happens
proveSerializationsends two messages to one identity and runs two workers.The runtime is configured with
leaseDurationMilliseconds: 250, becauseproveCrashRecoveryandproveFencingneed a short lease to demonstraterecovery. On a slow runner a worker can lose that lease mid-operation, and the
replacement executes the same message again. The control file is written outside
the transaction, so it records six events instead of four.
That is the at-least-once contract the library documents, and the same behaviour
the crash and fencing proofs assert deliberately (
repeatedEffects: 2). Thecommitted state is still
2, because the stale owner's write is fenced out.Evidence
The assertion failed five times on GitHub runners and passed on rerun each time:
qualityjobIt does not reproduce locally. Six runs of the demo pass on both 24.4.0 and
24.18.0, and forcing the lease down to 40 ms still produced four events every
time, because the operation completes long before the lease expires on fast
hardware.
Change
assertSerializedExecutionnow asserts what the runtime guarantees:rather than only the first pair;
assert.equal(snapshot.count, 2)is unchanged, and it is the assertion thatwould catch a lost or doubled write.
The lease timing is unchanged. Raising it to hide the retry would weaken
proveCrashRecoveryandproveFencing, which depend on it.Tests
assertSerializedExecutionmoved intoexamples/failure-recovery/serialization.tsso it can be tested at the lowest layer, and the demo imports it.
test/failure-recovery-serialization.test.tscovers:today;
The test file was written first and failed with
Cannot find module. Replacingthe rule body with
returnmakes the three rejection cases fail, so they testsomething rather than passing by construction.
Validation
pnpm run format:check,pnpm run check,pnpm run test(33 files, 249 passed,11 skipped),
pnpm run build, andpnpm run test:recoveryall pass locally.