From 3e46a0ef81dfe95c11d9c5324fb86758b155363d Mon Sep 17 00:00:00 2001 From: Louis Williams Date: Tue, 28 Mar 2023 11:58:12 +0000 Subject: SERVER-74778 Refactor and improve performance of PriorityTicketHolder --- .../MCPriorityTicketHolder.tla | 5 +- .../PriorityTicketHolder/PriorityTicketHolder.tla | 468 +++++++++------------ 2 files changed, 202 insertions(+), 271 deletions(-) (limited to 'src/mongo/tla_plus') 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 = <>, + \* 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 = <> /\ 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) -- cgit v1.2.1