[SERVER-59026] Begin TLA+ spec for Merge Created: 02/Aug/21  Updated: 03/Mar/23  Resolved: 03/Mar/23

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

Type: Task Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: [DO NOT USE] Backlog - Server Serverless (Inactive)
Resolution: Won't Do Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
is depended on by SERVER-57991 Architecture Guide updates for PM-2353 Closed
Assigned Teams:
Serverless
Sprint: Server Serverless 2021-08-23, Server Serverless 2021-08-30, Server Serverless 2021-09-06, Server Serverless 2021-09-13, Server Serverless 2021-09-20, Server Serverless 2021-09-27, Server Serverless 2021-10-04
Participants:

 Description   

Copy and enhance MultiTenantMigrations.tla to specify the slice merge algorithm. For this ticket, we'll restrict ourselves to the protocol of the Begin Implementing Merge project; we'll add more details to the TLA+ spec as we design them in later Merge projects.



 Comments   
Comment by A. Jesse Jiryu Davis [ 02/Sep/21 ]

More PRs to come before we close this ticket.

Comment by Githook User [ 02/Sep/21 ]

Author:

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

Message: SERVER-59026 Start TLA+ spec for Slice Merge
Branch: master
https://github.com/mongodb/mongo/commit/3d43fc9b257186fdc6e11bd73f1c50c0a3baaccd

Comment by Githook User [ 04/Aug/21 ]

Author:

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

Message: SERVER-59026 Move TLA+ dir from repl/ to mongo/
Branch: master
https://github.com/mongodb/mongo/commit/35c2b631b6efa1af9909d1c6edaef10d7dbacc1e

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