-
Type: Improvement
-
Resolution: Fixed
-
Priority: Major - P3
-
Affects Version/s: None
-
Component/s: None
-
Labels:None
-
Fully Compatible
-
Execution Team 2022-04-04
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.
- documents
-
SERVER-64076 Fix deadlock when waiting for tickets
- Closed