-
Type:
Task
-
Resolution: Unresolved
-
Priority:
Major - P3
-
None
-
Affects Version/s: None
-
Component/s: None
-
None
-
None
-
None
-
None
-
None
-
None
-
None
Summary
TLA+ model + regression jstest pinning the SERVER-124271 idempotency violation: ContainerBasedSpiller::mergeSpills() drives a MergeIterator from inside a writeConflictRetry lambda, so a WCE-driven rollback_transaction() resets the read cursors backing the merge while the iterator's in-memory heap state is unchanged — yielding silent drops or duplicates on retry.
Files
- src/mongo/tla_plus/Sorter/MergeSpillCursorReset/MergeSpillCursorReset.tla (310 lines)
- src/mongo/tla_plus/Sorter/MergeSpillCursorReset/MCMergeSpillCursorReset.tla (28)
- src/mongo/tla_plus/Sorter/MergeSpillCursorReset/MCMergeSpillCursorReset.cfg (green)
- src/mongo/tla_plus/Sorter/MergeSpillCursorReset/MCMergeSpillCursorResetBug.cfg (bug)
- src/mongo/tla_plus/Sorter/MergeSpillCursorReset/OWNERS.yml
- src/mongo/tla_plus/Sorter/MergeSpillCursorReset/README.md
- jstests/noPassthrough/merge_spill_wce_idempotency.js (147)
Model
- Actors: Merger (read offsets per spill + retry anchor) and WTSession (phases idle / writing / rolled_back)
- Actions: ReadHead, WCE, Resume, Commit, FlushFinal
- Invariants: NoElementLoss (terminal multiset equality), NoElementDuplication (step-wise)
- Parameter: ResetAffectsReadCursors ∈ BOOLEAN
TLC verdicts
| Cfg | ResetAffectsReadCursors | States | Verdict |
|---|---|---|---|
| Green | FALSE | 98 generated / 61 distinct / depth 13 | No error |
| Bug | TRUE | 30 generated / 28 distinct | NoElementDuplication violated; 5-state trace ReadHead → WCE → Resume → ReadHead → buffer=<<1,1>> |
jstest
Forces a $group pipeline to spill (per-doc batching, 1-byte group memory cap), runs a control aggregate, then configures the WTWriteConflictException failpoint with times: 4 and re-runs. Asserts bit-identical group count, per-group n, and content checksum across the two runs.
Owners
10gen/server-storage-execution + 10gen/server-external-sorter (best guess; re-route if a different reviewer pool is preferred).
- is related to
-
SERVER-124271 mergeSpills silently drops or duplicates elements when a write-conflict retry resets WiredTiger cursor positions
-
- Open
-