SERVER-74778 Refactor and improve performance of PriorityTicketHolder

2 files changed, 202 insertions, 271 deletions

diff --git a/src/mongo/tla_plus/PriorityTicketHolder/MCPriorityTicketHolder.tla b/src/mongo/tla_plus/PriorityTicketHolder/MCPriorityTicketHolder.tla
index bdcf64f6687..96c18afa487 100644
--- a/src/mongo/tla_plus/PriorityTicketHolder/MCPriorityTicketHolder.tla
+++ b/src/mongo/tla_plus/PriorityTicketHolder/MCPriorityTicketHolder.tla
@@ -6,8 +6,5 @@ TicketsAreAtMostTheInitialNumber ==
 ticketsAvailable <= InitialNumberOfTicketsAvailable /\ ticketsAvailable >= 0
 
 AllTicketsAvailableImpliesNoWaiters ==
-ticketsAvailable = InitialNumberOfTicketsAvailable => (numQueuedProc[1] + numQueuedProc[2] = 0)
-
-NumQueuedAlwaysGreaterOrEqualTo0 ==
-    numQueuedProc[1] >= 0 /\ numQueuedProc[2] >= 0
+ticketsAvailable = InitialNumberOfTicketsAvailable => (queuedProcs = {})
 =============================================================================
diff --git a/src/mongo/tla_plus/PriorityTicketHolder/PriorityTicketHolder.tla b/src/mongo/tla_plus/PriorityTicketHolder/PriorityTicketHolder.tla
index 33be98e774f..77a85e03179 100644
--- a/src/mongo/tla_plus/PriorityTicketHolder/PriorityTicketHolder.tla
+++ b/src/mongo/tla_plus/PriorityTicketHolder/PriorityTicketHolder.tla
@@ -8,15 +8,24 @@ EXTENDS Integers, Sequences, TLC, FiniteSets
 CONSTANT InitialNumberOfTicketsAvailable
 CONSTANT MaximumNumberOfWorkers
 
+\* These are the possible futex values of TicketWaiter::State
+None == -1
+Waiting == 0
+Acquired == 1
+TimedOut == 2
+
 (* --algorithm TicketHolder {
 
 variables
     Proc = 1..MaximumNumberOfWorkers,
-    QueueIndexes = {1, 2},
     ticketsAvailable = InitialNumberOfTicketsAvailable,
     mutexLocked = FALSE,
-    queuedProcs = <<{}, {}>>,
-    numQueuedProc = <<0, 0>>,
+    \* Queue of just pids. Order is implementation-defined anyways so we can use a set.
+    queuedProcs = {},
+    \* This functions as a map of pids to waiter state. This must be manually initialized to have
+    \* MaximumNumberOfWorkers elements.
+    procState = <<None, None, None>>,
+    \* This is the set of pids that are eligible for being signaled to timeout.
     procsForTimeout = {};
 
 macro Lock() {
@@ -29,10 +38,9 @@ macro Unlock() {
 }
 
 procedure Acquire(pid)
-variables 
+variables
     hasTicket = FALSE,
     hasTimedOut = FALSE,
-    procQueue = -1 ;
 {
     \* This is the tryAcquire() method inlined.
     tryAcquire:
@@ -45,7 +53,6 @@ variables
     
     enqueue:
         while (~hasTicket) {
-    acquireEnqueuerLock:
             Lock();
     innerMutexTry:
             if (ticketsAvailable > 0) {
@@ -54,11 +61,8 @@ variables
                 return;
             };
     registerAsWaiter:
-            with (chosen \in QueueIndexes) {
-                procQueue := chosen;
-            };
-            numQueuedProc[procQueue] := numQueuedProc[procQueue] + 1;
-            queuedProcs[procQueue] := queuedProcs[procQueue] \union {pid};
+            queuedProcs := queuedProcs \union {pid};
+            procState[pid] := Waiting;
     doneRegistering:
             Unlock();
             \* We register the process as available for a random timeout. This set is modified
@@ -66,25 +70,25 @@ variables
             procsForTimeout := procsForTimeout \union {pid};
     waitForTicketHandedOver:
             \* Wait until given a ticket (1st condition) or has timed out (2nd condition)
-            await ~(pid \in queuedProcs[procQueue]) \/ ~(pid \in procsForTimeout);
+            await (procState[pid] = Acquired) \/ ~(pid \in procsForTimeout);
             hasTimedOut := ~(pid \in procsForTimeout);
             \* We've woken up, remove ourselves as available for timeout.
             procsForTimeout := procsForTimeout \ {pid};
-    unregisterAsWaiter:
+    checkForTicketAfterTimeout:
             if (hasTimedOut) {
-    lockForUnregister:
-                Lock();
-    actualUnregister:
-                hasTicket := ~(pid \in queuedProcs[procQueue]);
+                hasTicket := (procState[pid] = Acquired);
                 if (~hasTicket) {
-                    numQueuedProc[procQueue] := numQueuedProc[procQueue] - 1;
+                    \* We let the releasers know that we have timed out so that they do not give
+                    \* us a ticket. They will remove us from the queue.
+                    procState[pid] := TimedOut;
                 };
-                queuedProcs[procQueue] := queuedProcs[procQueue] \ {pid};
-    unlockForUnregister:
-                Unlock();
-            } else {
+            }
+            else {
     ticketCheck:
-                hasTicket := ~(pid \in queuedProcs[procQueue]);
+                hasTicket := (procState[pid] = Acquired);
+                if (hasTicket) {
+                    queuedProcs := queuedProcs \ {pid};
+                };
             };
         };
     done:
@@ -92,46 +96,50 @@ variables
 };
 
 procedure Release()
-variables triedQueues = {},
-          chosenQueue = -1 ;
+variables chosenPid = -1;
 {
-    disableEnqueueing:
-        Lock();
+    whileNonTimedOutWaiter:
+        while (TRUE) {
+            Lock();
     dequeueProc:
-        while (triedQueues # QueueIndexes) {
-            with (queueChosen \in (QueueIndexes \ triedQueues)) {
-                chosenQueue := queueChosen;
-            };
-    checkWoken:
-            if (numQueuedProc[chosenQueue] > 0) {
-                numQueuedProc[chosenQueue] := numQueuedProc[chosenQueue] - 1;
-                with (chosenPid \in queuedProcs[chosenQueue]) {
-                    queuedProcs[chosenQueue] := queuedProcs[chosenQueue] \ {chosenPid};
+            if (queuedProcs # {}) {
+                with (aPid \in queuedProcs) {
+                    chosenPid := aPid;
+                    queuedProcs := queuedProcs \ {chosenPid};
+                };
+    doneDequeueing:
+                Unlock();
+    notifyIfNotTimedOut:
+                if (procState[chosenPid] /= TimedOut) {
+                    procState[chosenPid] := Acquired;
+                    return;
                 };
-                goto done;
+            }
+            else {
+    releaseTicket:
+                ticketsAvailable := ticketsAvailable + 1;
+                Unlock();
+                return;
             };
-    failedToDequeue:
-            triedQueues := triedQueues \union {chosenQueue};           
         };
-    releaseTicket:
-        ticketsAvailable := ticketsAvailable + 1;
     done:
-        Unlock();
         return;
 };
 
-fair process (Timeout = 0) {
+fair process (Timeout = 0)
+{
     timeoutLoop:
         while (TRUE) {
     acquirePid:
-            if (procsForTimeout # {}) {
-                with (queuedPid \in procsForTimeout) {
+            if (queuedProcs # {}) {
+                with (queuedPid \in queuedProcs) {
                     procsForTimeout := procsForTimeout \ {queuedPid};
                 };
             };
         };
 };
 
+
 fair process (P \in Proc)
 variable shouldContinue = TRUE ;
 {
@@ -150,36 +158,32 @@ variable shouldContinue = TRUE ;
         };
 };
 } *)
-\* BEGIN TRANSLATION (chksum(pcal) = "8055c5bb" /\ chksum(tla) = "1c77803b")
-\* Label done of procedure Acquire at line 91 col 9 changed to done_
+\* BEGIN TRANSLATION (chksum(pcal) = "3ca56f9e" /\ chksum(tla) = "ba80db81")
+\* Label done of procedure Acquire at line 95 col 9 changed to done_
 CONSTANT defaultInitValue
-VARIABLES Proc, QueueIndexes, ticketsAvailable, mutexLocked, queuedProcs, 
-          numQueuedProc, procsForTimeout, pc, stack, pid, hasTicket, 
-          hasTimedOut, procQueue, triedQueues, chosenQueue, shouldContinue
+VARIABLES Proc, ticketsAvailable, mutexLocked, queuedProcs, procState, 
+          procsForTimeout, pc, stack, pid, hasTicket, hasTimedOut, chosenPid, 
+          shouldContinue
 
-vars == << Proc, QueueIndexes, ticketsAvailable, mutexLocked, queuedProcs, 
-           numQueuedProc, procsForTimeout, pc, stack, pid, hasTicket, 
-           hasTimedOut, procQueue, triedQueues, chosenQueue, shouldContinue
-        >>
+vars == << Proc, ticketsAvailable, mutexLocked, queuedProcs, procState, 
+           procsForTimeout, pc, stack, pid, hasTicket, hasTimedOut, chosenPid, 
+           shouldContinue >>
 
 ProcSet == {0} \cup (Proc)
 
 Init == (* Global variables *)
         /\ Proc = 1..MaximumNumberOfWorkers
-        /\ QueueIndexes = {1, 2}
         /\ ticketsAvailable = InitialNumberOfTicketsAvailable
         /\ mutexLocked = FALSE
-        /\ queuedProcs = <<{}, {}>>
-        /\ numQueuedProc = <<0, 0>>
+        /\ queuedProcs = {}
+        /\ procState = <<None, None, None>>
         /\ procsForTimeout = {}
         (* Procedure Acquire *)
         /\ pid = [ self \in ProcSet |-> defaultInitValue]
         /\ hasTicket = [ self \in ProcSet |-> FALSE]
         /\ hasTimedOut = [ self \in ProcSet |-> FALSE]
-        /\ procQueue = [ self \in ProcSet |-> -1]
         (* Procedure Release *)
-        /\ triedQueues = [ self \in ProcSet |-> {}]
-        /\ chosenQueue = [ self \in ProcSet |-> -1]
+        /\ chosenPid = [ self \in ProcSet |-> -1]
         (* Process P *)
         /\ shouldContinue = [self \in Proc |-> TRUE]
         /\ stack = [self \in ProcSet |-> << >>]
@@ -192,39 +196,25 @@ tryAcquire(self) == /\ pc[self] = "tryAcquire"
                                /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
                                /\ hasTicket' = [hasTicket EXCEPT ![self] = Head(stack[self]).hasTicket]
                                /\ hasTimedOut' = [hasTimedOut EXCEPT ![self] = Head(stack[self]).hasTimedOut]
-                               /\ procQueue' = [procQueue EXCEPT ![self] = Head(stack[self]).procQueue]
                                /\ pid' = [pid EXCEPT ![self] = Head(stack[self]).pid]
                                /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
                           ELSE /\ pc' = [pc EXCEPT ![self] = "enqueue"]
                                /\ UNCHANGED << ticketsAvailable, stack, pid, 
-                                               hasTicket, hasTimedOut, 
-                                               procQueue >>
-                    /\ UNCHANGED << Proc, QueueIndexes, mutexLocked, 
-                                    queuedProcs, numQueuedProc, 
-                                    procsForTimeout, triedQueues, chosenQueue, 
-                                    shouldContinue >>
+                                               hasTicket, hasTimedOut >>
+                    /\ UNCHANGED << Proc, mutexLocked, queuedProcs, procState, 
+                                    procsForTimeout, chosenPid, shouldContinue >>
 
 enqueue(self) == /\ pc[self] = "enqueue"
                  /\ IF ~hasTicket[self]
-                       THEN /\ pc' = [pc EXCEPT ![self] = "acquireEnqueuerLock"]
+                       THEN /\ mutexLocked = FALSE
+                            /\ mutexLocked' = TRUE
+                            /\ pc' = [pc EXCEPT ![self] = "innerMutexTry"]
                        ELSE /\ pc' = [pc EXCEPT ![self] = "done_"]
-                 /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                 mutexLocked, queuedProcs, numQueuedProc, 
-                                 procsForTimeout, stack, pid, hasTicket, 
-                                 hasTimedOut, procQueue, triedQueues, 
-                                 chosenQueue, shouldContinue >>
-
-acquireEnqueuerLock(self) == /\ pc[self] = "acquireEnqueuerLock"
-                             /\ mutexLocked = FALSE
-                             /\ mutexLocked' = TRUE
-                             /\ pc' = [pc EXCEPT ![self] = "innerMutexTry"]
-                             /\ UNCHANGED << Proc, QueueIndexes, 
-                                             ticketsAvailable, queuedProcs, 
-                                             numQueuedProc, procsForTimeout, 
-                                             stack, pid, hasTicket, 
-                                             hasTimedOut, procQueue, 
-                                             triedQueues, chosenQueue, 
-                                             shouldContinue >>
+                            /\ UNCHANGED mutexLocked
+                 /\ UNCHANGED << Proc, ticketsAvailable, queuedProcs, 
+                                 procState, procsForTimeout, stack, pid, 
+                                 hasTicket, hasTimedOut, chosenPid, 
+                                 shouldContinue >>
 
 innerMutexTry(self) == /\ pc[self] = "innerMutexTry"
                        /\ IF ticketsAvailable > 0
@@ -233,220 +223,172 @@ innerMutexTry(self) == /\ pc[self] = "innerMutexTry"
                                   /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
                                   /\ hasTicket' = [hasTicket EXCEPT ![self] = Head(stack[self]).hasTicket]
                                   /\ hasTimedOut' = [hasTimedOut EXCEPT ![self] = Head(stack[self]).hasTimedOut]
-                                  /\ procQueue' = [procQueue EXCEPT ![self] = Head(stack[self]).procQueue]
                                   /\ pid' = [pid EXCEPT ![self] = Head(stack[self]).pid]
                                   /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
                              ELSE /\ pc' = [pc EXCEPT ![self] = "registerAsWaiter"]
                                   /\ UNCHANGED << ticketsAvailable, 
                                                   mutexLocked, stack, pid, 
-                                                  hasTicket, hasTimedOut, 
-                                                  procQueue >>
-                       /\ UNCHANGED << Proc, QueueIndexes, queuedProcs, 
-                                       numQueuedProc, procsForTimeout, 
-                                       triedQueues, chosenQueue, 
+                                                  hasTicket, hasTimedOut >>
+                       /\ UNCHANGED << Proc, queuedProcs, procState, 
+                                       procsForTimeout, chosenPid, 
                                        shouldContinue >>
 
 registerAsWaiter(self) == /\ pc[self] = "registerAsWaiter"
-                          /\ \E chosen \in QueueIndexes:
-                               procQueue' = [procQueue EXCEPT ![self] = chosen]
-                          /\ numQueuedProc' = [numQueuedProc EXCEPT ![procQueue'[self]] = numQueuedProc[procQueue'[self]] + 1]
-                          /\ queuedProcs' = [queuedProcs EXCEPT ![procQueue'[self]] = queuedProcs[procQueue'[self]] \union {pid[self]}]
+                          /\ queuedProcs' = (queuedProcs \union {pid[self]})
+                          /\ procState' = [procState EXCEPT ![pid[self]] = Waiting]
                           /\ pc' = [pc EXCEPT ![self] = "doneRegistering"]
-                          /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                          mutexLocked, procsForTimeout, stack, 
-                                          pid, hasTicket, hasTimedOut, 
-                                          triedQueues, chosenQueue, 
+                          /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                                          procsForTimeout, stack, pid, 
+                                          hasTicket, hasTimedOut, chosenPid, 
                                           shouldContinue >>
 
 doneRegistering(self) == /\ pc[self] = "doneRegistering"
                          /\ mutexLocked' = FALSE
                          /\ procsForTimeout' = (procsForTimeout \union {pid[self]})
                          /\ pc' = [pc EXCEPT ![self] = "waitForTicketHandedOver"]
-                         /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                         queuedProcs, numQueuedProc, stack, 
-                                         pid, hasTicket, hasTimedOut, 
-                                         procQueue, triedQueues, chosenQueue, 
+                         /\ UNCHANGED << Proc, ticketsAvailable, queuedProcs, 
+                                         procState, stack, pid, hasTicket, 
+                                         hasTimedOut, chosenPid, 
                                          shouldContinue >>
 
 waitForTicketHandedOver(self) == /\ pc[self] = "waitForTicketHandedOver"
-                                 /\ ~(pid[self] \in queuedProcs[procQueue[self]]) \/ ~(pid[self] \in procsForTimeout)
+                                 /\ (procState[pid[self]] = Acquired) \/ ~(pid[self] \in procsForTimeout)
                                  /\ hasTimedOut' = [hasTimedOut EXCEPT ![self] = ~(pid[self] \in procsForTimeout)]
                                  /\ procsForTimeout' = procsForTimeout \ {pid[self]}
-                                 /\ pc' = [pc EXCEPT ![self] = "unregisterAsWaiter"]
-                                 /\ UNCHANGED << Proc, QueueIndexes, 
-                                                 ticketsAvailable, mutexLocked, 
-                                                 queuedProcs, numQueuedProc, 
-                                                 stack, pid, hasTicket, 
-                                                 procQueue, triedQueues, 
-                                                 chosenQueue, shouldContinue >>
-
-unregisterAsWaiter(self) == /\ pc[self] = "unregisterAsWaiter"
-                            /\ IF hasTimedOut[self]
-                                  THEN /\ pc' = [pc EXCEPT ![self] = "lockForUnregister"]
-                                  ELSE /\ pc' = [pc EXCEPT ![self] = "ticketCheck"]
-                            /\ UNCHANGED << Proc, QueueIndexes, 
-                                            ticketsAvailable, mutexLocked, 
-                                            queuedProcs, numQueuedProc, 
-                                            procsForTimeout, stack, pid, 
-                                            hasTicket, hasTimedOut, procQueue, 
-                                            triedQueues, chosenQueue, 
-                                            shouldContinue >>
-
-lockForUnregister(self) == /\ pc[self] = "lockForUnregister"
-                           /\ mutexLocked = FALSE
-                           /\ mutexLocked' = TRUE
-                           /\ pc' = [pc EXCEPT ![self] = "actualUnregister"]
-                           /\ UNCHANGED << Proc, QueueIndexes, 
-                                           ticketsAvailable, queuedProcs, 
-                                           numQueuedProc, procsForTimeout, 
-                                           stack, pid, hasTicket, hasTimedOut, 
-                                           procQueue, triedQueues, chosenQueue, 
-                                           shouldContinue >>
-
-actualUnregister(self) == /\ pc[self] = "actualUnregister"
-                          /\ hasTicket' = [hasTicket EXCEPT ![self] = ~(pid[self] \in queuedProcs[procQueue[self]])]
-                          /\ IF ~hasTicket'[self]
-                                THEN /\ numQueuedProc' = [numQueuedProc EXCEPT ![procQueue[self]] = numQueuedProc[procQueue[self]] - 1]
-                                ELSE /\ TRUE
-                                     /\ UNCHANGED numQueuedProc
-                          /\ queuedProcs' = [queuedProcs EXCEPT ![procQueue[self]] = queuedProcs[procQueue[self]] \ {pid[self]}]
-                          /\ pc' = [pc EXCEPT ![self] = "unlockForUnregister"]
-                          /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                          mutexLocked, procsForTimeout, stack, 
-                                          pid, hasTimedOut, procQueue, 
-                                          triedQueues, chosenQueue, 
-                                          shouldContinue >>
-
-unlockForUnregister(self) == /\ pc[self] = "unlockForUnregister"
-                             /\ mutexLocked' = FALSE
-                             /\ pc' = [pc EXCEPT ![self] = "enqueue"]
-                             /\ UNCHANGED << Proc, QueueIndexes, 
-                                             ticketsAvailable, queuedProcs, 
-                                             numQueuedProc, procsForTimeout, 
-                                             stack, pid, hasTicket, 
-                                             hasTimedOut, procQueue, 
-                                             triedQueues, chosenQueue, 
-                                             shouldContinue >>
+                                 /\ pc' = [pc EXCEPT ![self] = "checkForTicketAfterTimeout"]
+                                 /\ UNCHANGED << Proc, ticketsAvailable, 
+                                                 mutexLocked, queuedProcs, 
+                                                 procState, stack, pid, 
+                                                 hasTicket, chosenPid, 
+                                                 shouldContinue >>
+
+checkForTicketAfterTimeout(self) == /\ pc[self] = "checkForTicketAfterTimeout"
+                                    /\ IF hasTimedOut[self]
+                                          THEN /\ hasTicket' = [hasTicket EXCEPT ![self] = (procState[pid[self]] = Acquired)]
+                                               /\ IF ~hasTicket'[self]
+                                                     THEN /\ procState' = [procState EXCEPT ![pid[self]] = TimedOut]
+                                                     ELSE /\ TRUE
+                                                          /\ UNCHANGED procState
+                                               /\ pc' = [pc EXCEPT ![self] = "enqueue"]
+                                          ELSE /\ pc' = [pc EXCEPT ![self] = "ticketCheck"]
+                                               /\ UNCHANGED << procState, 
+                                                               hasTicket >>
+                                    /\ UNCHANGED << Proc, ticketsAvailable, 
+                                                    mutexLocked, queuedProcs, 
+                                                    procsForTimeout, stack, 
+                                                    pid, hasTimedOut, 
+                                                    chosenPid, shouldContinue >>
 
 ticketCheck(self) == /\ pc[self] = "ticketCheck"
-                     /\ hasTicket' = [hasTicket EXCEPT ![self] = ~(pid[self] \in queuedProcs[procQueue[self]])]
+                     /\ hasTicket' = [hasTicket EXCEPT ![self] = (procState[pid[self]] = Acquired)]
+                     /\ IF hasTicket'[self]
+                           THEN /\ queuedProcs' = queuedProcs \ {pid[self]}
+                           ELSE /\ TRUE
+                                /\ UNCHANGED queuedProcs
                      /\ pc' = [pc EXCEPT ![self] = "enqueue"]
-                     /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                     mutexLocked, queuedProcs, numQueuedProc, 
-                                     procsForTimeout, stack, pid, hasTimedOut, 
-                                     procQueue, triedQueues, chosenQueue, 
-                                     shouldContinue >>
+                     /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                                     procState, procsForTimeout, stack, pid, 
+                                     hasTimedOut, chosenPid, shouldContinue >>
 
 done_(self) == /\ pc[self] = "done_"
                /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
                /\ hasTicket' = [hasTicket EXCEPT ![self] = Head(stack[self]).hasTicket]
                /\ hasTimedOut' = [hasTimedOut EXCEPT ![self] = Head(stack[self]).hasTimedOut]
-               /\ procQueue' = [procQueue EXCEPT ![self] = Head(stack[self]).procQueue]
                /\ pid' = [pid EXCEPT ![self] = Head(stack[self]).pid]
                /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
-               /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                               mutexLocked, queuedProcs, numQueuedProc, 
-                               procsForTimeout, triedQueues, chosenQueue, 
-                               shouldContinue >>
+               /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                               queuedProcs, procState, procsForTimeout, 
+                               chosenPid, shouldContinue >>
 
-Acquire(self) == tryAcquire(self) \/ enqueue(self)
-                    \/ acquireEnqueuerLock(self) \/ innerMutexTry(self)
+Acquire(self) == tryAcquire(self) \/ enqueue(self) \/ innerMutexTry(self)
                     \/ registerAsWaiter(self) \/ doneRegistering(self)
                     \/ waitForTicketHandedOver(self)
-                    \/ unregisterAsWaiter(self) \/ lockForUnregister(self)
-                    \/ actualUnregister(self) \/ unlockForUnregister(self)
+                    \/ checkForTicketAfterTimeout(self)
                     \/ ticketCheck(self) \/ done_(self)
 
-disableEnqueueing(self) == /\ pc[self] = "disableEnqueueing"
-                           /\ mutexLocked = FALSE
-                           /\ mutexLocked' = TRUE
-                           /\ pc' = [pc EXCEPT ![self] = "dequeueProc"]
-                           /\ UNCHANGED << Proc, QueueIndexes, 
-                                           ticketsAvailable, queuedProcs, 
-                                           numQueuedProc, procsForTimeout, 
-                                           stack, pid, hasTicket, hasTimedOut, 
-                                           procQueue, triedQueues, chosenQueue, 
-                                           shouldContinue >>
+whileNonTimedOutWaiter(self) == /\ pc[self] = "whileNonTimedOutWaiter"
+                                /\ mutexLocked = FALSE
+                                /\ mutexLocked' = TRUE
+                                /\ pc' = [pc EXCEPT ![self] = "dequeueProc"]
+                                /\ UNCHANGED << Proc, ticketsAvailable, 
+                                                queuedProcs, procState, 
+                                                procsForTimeout, stack, pid, 
+                                                hasTicket, hasTimedOut, 
+                                                chosenPid, shouldContinue >>
 
 dequeueProc(self) == /\ pc[self] = "dequeueProc"
-                     /\ IF triedQueues[self] # QueueIndexes
-                           THEN /\ \E queueChosen \in (QueueIndexes \ triedQueues[self]):
-                                     chosenQueue' = [chosenQueue EXCEPT ![self] = queueChosen]
-                                /\ pc' = [pc EXCEPT ![self] = "checkWoken"]
+                     /\ IF queuedProcs # {}
+                           THEN /\ \E aPid \in queuedProcs:
+                                     /\ chosenPid' = [chosenPid EXCEPT ![self] = aPid]
+                                     /\ queuedProcs' = queuedProcs \ {chosenPid'[self]}
+                                /\ pc' = [pc EXCEPT ![self] = "doneDequeueing"]
                            ELSE /\ pc' = [pc EXCEPT ![self] = "releaseTicket"]
-                                /\ UNCHANGED chosenQueue
-                     /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                     mutexLocked, queuedProcs, numQueuedProc, 
-                                     procsForTimeout, stack, pid, hasTicket, 
-                                     hasTimedOut, procQueue, triedQueues, 
-                                     shouldContinue >>
-
-checkWoken(self) == /\ pc[self] = "checkWoken"
-                    /\ IF numQueuedProc[chosenQueue[self]] > 0
-                          THEN /\ numQueuedProc' = [numQueuedProc EXCEPT ![chosenQueue[self]] = numQueuedProc[chosenQueue[self]] - 1]
-                               /\ \E chosenPid \in queuedProcs[chosenQueue[self]]:
-                                    queuedProcs' = [queuedProcs EXCEPT ![chosenQueue[self]] = queuedProcs[chosenQueue[self]] \ {chosenPid}]
-                               /\ pc' = [pc EXCEPT ![self] = "done"]
-                          ELSE /\ pc' = [pc EXCEPT ![self] = "failedToDequeue"]
-                               /\ UNCHANGED << queuedProcs, numQueuedProc >>
-                    /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                    mutexLocked, procsForTimeout, stack, pid, 
-                                    hasTicket, hasTimedOut, procQueue, 
-                                    triedQueues, chosenQueue, shouldContinue >>
-
-failedToDequeue(self) == /\ pc[self] = "failedToDequeue"
-                         /\ triedQueues' = [triedQueues EXCEPT ![self] = triedQueues[self] \union {chosenQueue[self]}]
-                         /\ pc' = [pc EXCEPT ![self] = "dequeueProc"]
-                         /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                         mutexLocked, queuedProcs, 
-                                         numQueuedProc, procsForTimeout, stack, 
-                                         pid, hasTicket, hasTimedOut, 
-                                         procQueue, chosenQueue, 
-                                         shouldContinue >>
+                                /\ UNCHANGED << queuedProcs, chosenPid >>
+                     /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                                     procState, procsForTimeout, stack, pid, 
+                                     hasTicket, hasTimedOut, shouldContinue >>
+
+doneDequeueing(self) == /\ pc[self] = "doneDequeueing"
+                        /\ mutexLocked' = FALSE
+                        /\ pc' = [pc EXCEPT ![self] = "notifyIfNotTimedOut"]
+                        /\ UNCHANGED << Proc, ticketsAvailable, queuedProcs, 
+                                        procState, procsForTimeout, stack, pid, 
+                                        hasTicket, hasTimedOut, chosenPid, 
+                                        shouldContinue >>
+
+notifyIfNotTimedOut(self) == /\ pc[self] = "notifyIfNotTimedOut"
+                             /\ IF procState[chosenPid[self]] /= TimedOut
+                                   THEN /\ procState' = [procState EXCEPT ![chosenPid[self]] = Acquired]
+                                        /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
+                                        /\ chosenPid' = [chosenPid EXCEPT ![self] = Head(stack[self]).chosenPid]
+                                        /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
+                                   ELSE /\ pc' = [pc EXCEPT ![self] = "whileNonTimedOutWaiter"]
+                                        /\ UNCHANGED << procState, stack, 
+                                                        chosenPid >>
+                             /\ UNCHANGED << Proc, ticketsAvailable, 
+                                             mutexLocked, queuedProcs, 
+                                             procsForTimeout, pid, hasTicket, 
+                                             hasTimedOut, shouldContinue >>
 
 releaseTicket(self) == /\ pc[self] = "releaseTicket"
                        /\ ticketsAvailable' = ticketsAvailable + 1
-                       /\ pc' = [pc EXCEPT ![self] = "done"]
-                       /\ UNCHANGED << Proc, QueueIndexes, mutexLocked, 
-                                       queuedProcs, numQueuedProc, 
-                                       procsForTimeout, stack, pid, hasTicket, 
-                                       hasTimedOut, procQueue, triedQueues, 
-                                       chosenQueue, shouldContinue >>
+                       /\ mutexLocked' = FALSE
+                       /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
+                       /\ chosenPid' = [chosenPid EXCEPT ![self] = Head(stack[self]).chosenPid]
+                       /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
+                       /\ UNCHANGED << Proc, queuedProcs, procState, 
+                                       procsForTimeout, pid, hasTicket, 
+                                       hasTimedOut, shouldContinue >>
 
 done(self) == /\ pc[self] = "done"
-              /\ mutexLocked' = FALSE
               /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
-              /\ triedQueues' = [triedQueues EXCEPT ![self] = Head(stack[self]).triedQueues]
-              /\ chosenQueue' = [chosenQueue EXCEPT ![self] = Head(stack[self]).chosenQueue]
+              /\ chosenPid' = [chosenPid EXCEPT ![self] = Head(stack[self]).chosenPid]
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
-              /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                              queuedProcs, numQueuedProc, procsForTimeout, pid, 
-                              hasTicket, hasTimedOut, procQueue, 
-                              shouldContinue >>
+              /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, queuedProcs, 
+                              procState, procsForTimeout, pid, hasTicket, 
+                              hasTimedOut, shouldContinue >>
 
-Release(self) == disableEnqueueing(self) \/ dequeueProc(self)
-                    \/ checkWoken(self) \/ failedToDequeue(self)
+Release(self) == whileNonTimedOutWaiter(self) \/ dequeueProc(self)
+                    \/ doneDequeueing(self) \/ notifyIfNotTimedOut(self)
                     \/ releaseTicket(self) \/ done(self)
 
 timeoutLoop == /\ pc[0] = "timeoutLoop"
                /\ pc' = [pc EXCEPT ![0] = "acquirePid"]
-               /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                               mutexLocked, queuedProcs, numQueuedProc, 
-                               procsForTimeout, stack, pid, hasTicket, 
-                               hasTimedOut, procQueue, triedQueues, 
-                               chosenQueue, shouldContinue >>
+               /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                               queuedProcs, procState, procsForTimeout, stack, 
+                               pid, hasTicket, hasTimedOut, chosenPid, 
+                               shouldContinue >>
 
 acquirePid == /\ pc[0] = "acquirePid"
-              /\ IF procsForTimeout # {}
-                    THEN /\ \E queuedPid \in procsForTimeout:
+              /\ IF queuedProcs # {}
+                    THEN /\ \E queuedPid \in queuedProcs:
                               procsForTimeout' = procsForTimeout \ {queuedPid}
                     ELSE /\ TRUE
                          /\ UNCHANGED procsForTimeout
               /\ pc' = [pc EXCEPT ![0] = "timeoutLoop"]
-              /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                              mutexLocked, queuedProcs, numQueuedProc, stack, 
-                              pid, hasTicket, hasTimedOut, procQueue, 
-                              triedQueues, chosenQueue, shouldContinue >>
+              /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, queuedProcs, 
+                              procState, stack, pid, hasTicket, hasTimedOut, 
+                              chosenPid, shouldContinue >>
 
 Timeout == timeoutLoop \/ acquirePid
 
@@ -454,10 +396,9 @@ loop(self) == /\ pc[self] = "loop"
               /\ IF shouldContinue[self]
                     THEN /\ pc' = [pc EXCEPT ![self] = "acquire"]
                     ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
-              /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                              mutexLocked, queuedProcs, numQueuedProc, 
-                              procsForTimeout, stack, pid, hasTicket, 
-                              hasTimedOut, procQueue, triedQueues, chosenQueue, 
+              /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, queuedProcs, 
+                              procState, procsForTimeout, stack, pid, 
+                              hasTicket, hasTimedOut, chosenPid, 
                               shouldContinue >>
 
 acquire(self) == /\ pc[self] = "acquire"
@@ -466,41 +407,34 @@ acquire(self) == /\ pc[self] = "acquire"
                                                              pc        |->  "release",
                                                              hasTicket |->  hasTicket[self],
                                                              hasTimedOut |->  hasTimedOut[self],
-                                                             procQueue |->  procQueue[self],
                                                              pid       |->  pid[self] ] >>
                                                          \o stack[self]]
                  /\ hasTicket' = [hasTicket EXCEPT ![self] = FALSE]
                  /\ hasTimedOut' = [hasTimedOut EXCEPT ![self] = FALSE]
-                 /\ procQueue' = [procQueue EXCEPT ![self] = -1]
                  /\ pc' = [pc EXCEPT ![self] = "tryAcquire"]
-                 /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                 mutexLocked, queuedProcs, numQueuedProc, 
-                                 procsForTimeout, triedQueues, chosenQueue, 
-                                 shouldContinue >>
+                 /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                                 queuedProcs, procState, procsForTimeout, 
+                                 chosenPid, shouldContinue >>
 
 release(self) == /\ pc[self] = "release"
                  /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "Release",
                                                           pc        |->  "maybeFinish",
-                                                          triedQueues |->  triedQueues[self],
-                                                          chosenQueue |->  chosenQueue[self] ] >>
+                                                          chosenPid |->  chosenPid[self] ] >>
                                                       \o stack[self]]
-                 /\ triedQueues' = [triedQueues EXCEPT ![self] = {}]
-                 /\ chosenQueue' = [chosenQueue EXCEPT ![self] = -1]
-                 /\ pc' = [pc EXCEPT ![self] = "disableEnqueueing"]
-                 /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                 mutexLocked, queuedProcs, numQueuedProc, 
-                                 procsForTimeout, pid, hasTicket, hasTimedOut, 
-                                 procQueue, shouldContinue >>
+                 /\ chosenPid' = [chosenPid EXCEPT ![self] = -1]
+                 /\ pc' = [pc EXCEPT ![self] = "whileNonTimedOutWaiter"]
+                 /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                                 queuedProcs, procState, procsForTimeout, pid, 
+                                 hasTicket, hasTimedOut, shouldContinue >>
 
 maybeFinish(self) == /\ pc[self] = "maybeFinish"
                      /\ \/ /\ shouldContinue' = [shouldContinue EXCEPT ![self] = TRUE]
                         \/ /\ shouldContinue' = [shouldContinue EXCEPT ![self] = FALSE]
                      /\ pc' = [pc EXCEPT ![self] = "loop"]
-                     /\ UNCHANGED << Proc, QueueIndexes, ticketsAvailable, 
-                                     mutexLocked, queuedProcs, numQueuedProc, 
-                                     procsForTimeout, stack, pid, hasTicket, 
-                                     hasTimedOut, procQueue, triedQueues, 
-                                     chosenQueue >>
+                     /\ UNCHANGED << Proc, ticketsAvailable, mutexLocked, 
+                                     queuedProcs, procState, procsForTimeout, 
+                                     stack, pid, hasTicket, hasTimedOut, 
+                                     chosenPid >>
 
 P(self) == loop(self) \/ acquire(self) \/ release(self)
               \/ maybeFinish(self)