When a collection has both a TTL index and a change-stream watcher, the ordering between (a) the TTL monitor's delete and (b) the change-stream's emission of insert/delete events relative to in-flight user writes matters for downstream-consumer correctness. A consumer maintaining derivative state keyed by document identity (caches, materialized views, audit logs) can observe a delete event for a document whose corresponding insert event was never emitted — a violation of causal ordering — if the TTL deleter and the oplog committer race against an uncommitted write.

The existing src/mongo/tla_plus/ corpus has no spec covering TTL or change-stream ordering. This ticket proposes adding a new specification at src/mongo/tla_plus/ChangeStreams/TTLEmissionOrdering/ that models the actor interleaving and proves three ordering invariants under the production-correct path.

Scope

• Pure addition to src/mongo/tla_plus/ChangeStreams/TTLEmissionOrdering/:
  • TTLEmissionOrdering.tla (~478 lines) — three actors (USER_WRITER / TTL_MONITOR / STREAM_CONSUMER), five safety invariants + two liveness properties
  • MCTTLEmissionOrdering.tla (~48 lines) — finite-constant instantiation
  • MCTTLEmissionOrdering.cfg — green-mode cfg (both bug knobs FALSE)
  • MCTTLEmissionOrderingBug.cfg — bug-mode cfg used to demonstrate counterexample
  • OWNERS.yml
  • README.md
• No C++ source changes.
• No test changes outside the TLA+ corpus.

Model

• Actors: USER_WRITER (insert with createdAt; staged→committed), TTL_MONITOR (deletes when createdAt+expireAfter ≤ now), STREAM_CONSUMER (reads oplog through a $match on createdAt).
• Bug knobs (both default FALSE in the production cfg):
  • AllowTTLBeforeCommit — if TRUE, TTL_MONITOR may operate on staged uncommitted docs.
  • AllowOutOfOrderEmit — if TRUE, StreamEmit may shuffle the oplog tail before buffering.
• Invariants (all hold green-mode):
  • TypeOK, OplogMonotonic, CausalOrdering, NoOrphanDelete, NoDeleteBeforeInsertInOplog.
• Liveness: TTLNoSkip, EventuallyDrained.

TLC verdicts

• Green cfg (AllowTTLBeforeCommit=FALSE, AllowOutOfOrderEmit=FALSE):
  • 140,808 states generated / 66,264 distinct / depth 19 / ~9s wall.
  • All 5 safety invariants + 2 liveness properties hold.
• Bug cfg (AllowTTLBeforeCommit=TRUE):
  • NoDeleteBeforeInsertInOplog violated in 5 steps (counterexample reproducible).

Run

cd src/mongo/tla_plus
./model-check.sh ChangeStreams/TTLEmissionOrdering

To reproduce the bug counterexample, swap to the bug-mode cfg per the README.

Acceptance criteria

• Files land under src/mongo/tla_plus/ChangeStreams/TTLEmissionOrdering/.
• ./model-check.sh ChangeStreams/TTLEmissionOrdering (green cfg) completes without errors.
• Bug-cfg invocation reproduces the documented counterexample.
• Owners file routes the spec to the appropriate team.

Related work

No prior TLA+ spec covers TTL or change streams in this repo. Adjacent in spirit:

• src/mongo/tla_plus/Sharding/RangeDeletionsSecondaryNodes/ — same background-deleter idiom.
• src/mongo/tla_plus/Replication/RaftMongo/ — oplog-as-shared-log idiom.

Implementation status

Draft of all six files authored and TLC-verified locally (both cfgs). Forbidden-term review complete. PR to follow on this ticket.