[SERVER-64466] Store PlusCal model of ticketing system in the codebase Created: 14/Mar/22  Updated: 29/Oct/23  Resolved: 30/Mar/22

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

Type: Improvement Priority: Major - P3
Reporter: Jordi Olivares Provencio Assignee: Jordi Olivares Provencio
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Attachments: File ticketholder.tla    
Issue Links:
Documented
documents SERVER-64076 Fix deadlock when waiting for tickets Closed
Backwards Compatibility: Fully Compatible
Sprint: Execution Team 2022-04-04
Participants:

 Description   

With the work on SERVER-64076, to verify its correctness we created a PlusCal (TLA+) model of the ticketing system with a queue.

The ticket's work is thus to decide where we can store the attached model within our codebase to provide a reference to its correctness.

The procedures that document the implemented version are the ones with the Correct prefix.



 Comments   
Comment by Githook User [ 30/Mar/22 ]

Author:

{'name': 'Jordi Olivares Provencio', 'email': 'jordi.olivares-provencio@mongodb.com', 'username': 'jordiolivares'}

Message: SERVER-64466 Add PlusCal implementation for the ticketholder
Branch: master
https://github.com/mongodb/mongo/commit/7e527530c7f7a42f560f4a8f4273bac2f6560407

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