Summary

TLA+ spec + jstest for the SERVER-114326 root-cause race: after a rename commits but before FilteringMetadataClearer runs, the range deleter reads the updated RangeDeletionTask (new UUID) while metadataTracker → metadata → getUUID() still holds the old one. SERVER-113667 patched a symptom; the underlying TOCTOU is open.

Files

• src/mongo/tla_plus/Sharding/RangeDeletionRenameRace/RangeDeletionRenameRace.tla (253 lines) — rename-coordinator × range-deleter-op-observer × FilteringMetadataClearer race. Shared state: taskUUID, metadataUUID. Headline invariant RangeDeleterMetadataMatchesCollectionUUID + ObserverSnapshotsCoherent + PostRenameMetadataIsFresh. Bug toggle AllowCommitBeforeMetadataClear gates the observer.
• MCRangeDeletionRenameRace.tla / .cfg (green) + MCRangeDeletionRenameRace_bug.cfg
• OWNERS.yml → 10gen/server-sharding
• README.md (262 words)
• jstests/sharding/range_deletion_stale_metadata_after_rename.js (167 lines) — drives the 300ms TOCTOU via suspendRangeDeletion + hangBeforeFilteringMetadataClearerOnRename failpoints; asserts (a) in-window task carries the new UUID, (b) no mismatched-UUID invalidations logged, (c) no task retains the pre-rename UUID after completion.

TLC verdicts

• Green: 10 distinct states, depth 7, no errors; all 5 temporal branches pass.
• Bug: 5-state counterexample at depth 5 — invalidationMismatch=TRUE with taskUUID="uuid-new", metadataUUID="uuid-old", exactly the SERVER-114326 trace.

Note

The jstest references hangBeforeFilteringMetadataClearerOnRename; if no failpoint exists under that exact name, a one-line addition is needed in range_deleter_service_op_observer.cpp or the rename coordinator's metadata-clear path. Spec is failpoint-independent.