[SERVER-44458] Productionize RaftMongo TLA+ spec Created: 06/Nov/19  Updated: 29/Oct/23  Resolved: 16/Jan/20

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.3.3

Type: Task Priority: Major - P3
Reporter: Judah Schvimer Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
is depended on by SERVER-45415 Factor RaftMongo.tla with MongoReplRe... Backlog
Issue split
split from SERVER-43588 Select and update TLA+ specs for trac... Closed
Related
related to SERVER-46789 Make TLC wrapper script cross-platform Closed
Backwards Compatibility: Fully Compatible
Sprint: Repl 2019-11-18, Repl 2019-12-02, Repl 2019-12-16, Repl 2019-12-30, Repl 2020-01-13, Repl 2020-01-27
Participants:

 Description   

SERVER-43588 will choose other specs to productionize, but the highest value in the past has been RaftMongo so we will start with that.



 Comments   
Comment by Githook User [ 29/Jan/20 ]

Author:

{'username': 'ajdavis', 'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com'}

Message: SERVER-45558 Revert logging additions for TLA+ Trace Checker project

This is a combination of 6 commits.

Revert "SERVER-44458 Add RaftMongo.tla spec"

This reverts commit 88aaa47b815507e3ddd9a3a79f00d0eaca3ae071.

Revert "SERVER-45184 Ban TLA+ tracing with inMemory"

This reverts commit e57438bd024d04f82dcbcbe68fe223b3f3aec838.

Revert "SERVER-43589 Trace logging for RaftMongo.tla"

This reverts commit f515d2ad5494e64c3be80189e7ea6bceaf267421.

Revert "SERVER-44076 create TLA+ Trace Checking logging framework"

This reverts commit 744200de5f5667334457ee35abfa3747e2e26d55.

Revert "SERVER-43589 Failpoint to log TLA+ trace events"

This reverts commit eda99cf7ca668908e5eb0498845b0270265c44e7.

Revert "SERVER-45106 Add TLA+ log component to logv2"

This reverts commit a60ce00707f0ffdb5d2ec5c3a72993cc2b2d2978.

delete mode 100644 jstests/replsets/tla_plus_trace_checking.js
delete mode 100644 src/mongo/db/repl/replication_coordinator_impl_tla_plus_trace.cpp
delete mode 100644 src/mongo/db/repl/tla_plus_trace_repl.idl
delete mode 100644 src/mongo/util/tla_plus_trace.cpp
delete mode 100644 src/mongo/util/tla_plus_trace.h
delete mode 100644 src/mongo/util/tla_plus_trace.idl
Branch: master
https://github.com/mongodb/mongo/commit/bcae9e6777408882b3d391721dea262c1cdcd16e

Comment by Githook User [ 16/Jan/20 ]

Author:

{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com', 'username': 'ajdavis'}

Message: SERVER-44458 Model-checking files for RaftMongo.tla
Branch: master
https://github.com/mongodb/mongo/commit/90738ed5ec26818b06d521f6ce6e5c37b2ce7697

Comment by A. Jesse Jiryu Davis [ 14/Jan/20 ]

Before closing, I'll upload a model config so future developers can run TLC on this spec. (Making progress toward solving SERVER-45416.)

Comment by Githook User [ 14/Jan/20 ]

Author:

{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com', 'username': 'ajdavis'}

Message: SERVER-44458 Add RaftMongo.tla spec
Branch: master
https://github.com/mongodb/mongo/commit/88aaa47b815507e3ddd9a3a79f00d0eaca3ae071

Generated at Thu Feb 08 05:06:02 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.