-
Type:
Task
-
Resolution: Unresolved
-
Priority:
Major - P3
-
None
-
Affects Version/s: None
-
Component/s: None
-
None
-
Catalog and Routing
-
CAR Team 2026-04-13
-
200
-
None
-
None
-
None
-
None
-
None
-
None
-
None
SERVER-122680 generated concerns about the current implementation of the OrderedTicketSemaphore, considering that the currently committed testing was unable to capture the issue. In order to increase confidence in the implementation, we should model the current implementation with TLA+, the idea would be:
- Prove the issue with the model
- Prove the fix
- Ensure that there are not any other issues with the queue
- is related to
-
SERVER-122680 OrderedTicketSemaphore might queue operations with tickets available
-
- Closed
-
- related to
-
SERVER-120543 Change TicketSemaphore acquire to enqueue directly instead of trying tryAcquire first
-
- Closed
-