Details
-
Improvement
-
Resolution: Fixed
-
Major - P3
-
None
-
None
-
None
-
Fully Compatible
-
Execution Team 2022-04-04
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.
Attachments
Issue Links
- documents
-
SERVER-64076 Fix deadlock when waiting for tickets
-
- Closed
-