Summary

Add a TLA+ specification covering the change-stream V2 shard-targeter and topology-change state machine: (Coordinator, Shard, Consumer) × (addShard, removeShard, getMore, readPreference, stepdown). The spec catches the SERVER-48386 / SERVER-124540 race shape as a model-checked counterexample.

Scope

• New directory: src/mongo/tla_plus/Sharding/ChangeStreamTopologyChange/
• Owner: 10gen/server-query-streams
• Reference implementation: src/mongo/db/exec/agg/change_stream_handle_topology_change_stage.cpp

Model

• Actors: Coordinator (issues addShard / removeShard / stepdown, ticks cluster time); Shards (append oplog entries, carry an epoch bumped on stepdown); Consumer (opens stream at a startAtOperationTime that may be in the future, holds per-shard cursors, advances a high-water-mark resume token via post-batch getMore).
• State: coordinatorTime, activeShards, per-shard oplog sequences, per-shard shardCursor (openedAt, epoch, pos), consumerResumeToken, consumerHWM, consumerDelivered.
• Actions: Tick, WriteOnShard, AddShard, RemoveShard, Stepdown, ConsumerGetMore.
• Abstractions: resume tokens collapsed to their clusterTime field; $mergeCursors merge-ordering modelled as a per-shard cursor + scalar HWM; replication / oplog hole-filling omitted; writes commit instantaneously.

Properties

• Safety: NoEventBeforeResumeToken (no delivered event has clusterTime < consumerResumeToken) and MonotonicHighWatermark.
• Liveness: EventuallyDelivered (every committed event on an active shard at or above the resume token is eventually delivered).

TLC verdicts

• Green mode (AllowNewShardCursorBelowResumeToken = FALSE): completed clean; 33,057 distinct states, depth 16, <2s wall on 10 workers.
• Bug mode (AllowNewShardCursorBelowResumeToken = TRUE): NoEventBeforeResumeToken violated at depth 4. Trace: AddShard at coordinatorTime=2 opens new-shard cursor at openedAt=3; WriteOnShard at ts=3; ConsumerGetMore delivers [shard: s3, ts: 3] while consumerResumeToken=5. Exact SERVER-48386 / SERVER-124540 shape: shardAddedTime + 1 < startAtOperationTime causes pre-future events to leak past the resume token.

Run

cd src/mongo/tla_plus
./download-tlc.sh
./model-check.sh Sharding/ChangeStreamTopologyChange

Flip AllowNewShardCursorBelowResumeToken to TRUE in MCChangeStreamTopologyChange.cfg to reproduce the counterexample.

Acceptance criteria

• Green-mode TLC run completes with no invariant violation under default constants.
• Bug-mode TLC run reports Invariant NoEventBeforeResumeToken is violated with a trace mapping onto the SERVER-48386 race shape.
• OWNERS.yml routes review to 10gen/server-query-streams.

Related

• SERVER-48386 — adding a new shard while awaiting a future startAtOperationTime
• SERVER-124540 — ensure ChangeStreamHandleTopologyChange opens new-shard cursor at max(shardAddedTime + 1, startAtOperationTime)
• SERVER-121834 — readPreference respect after elections (landed → reverted → re-landed)
• Existing template: src/mongo/tla_plus/Sharding/MoveRange/MoveRange.tla