diff --git a/src/mg/sch/TaskScheduler.cpp b/src/mg/sch/TaskScheduler.cpp index 8eadfe38..934c835e 100644 --- a/src/mg/sch/TaskScheduler.cpp +++ b/src/mg/sch/TaskScheduler.cpp @@ -130,10 +130,13 @@ namespace sch { // ------------------------------------------------------- // Handle front tasks. - mySignalFront.Receive(); // Popping the front queue takes linear time due to how the multi-producer queue // is implemented. It is not batched so far, but even for millions of tasks it is // a few milliseconds tops. + // Note, the front signal is not received, because under a high load the queue is + // rarely expected to be empty. So receiving this signal would be pointless. At + // the same time, if the queue does become empty for a while, the front signal is + // received when the scheduler has nothing to do and goes to sleep on that signal. t = myQueueFront.PopAll(tail); myQueuePending.Append(t, tail); batch = 0; diff --git a/tla/TaskScheduler.tla b/tla/TaskScheduler.tla index 1567b985..e90e84a9 100644 --- a/tla/TaskScheduler.tla +++ b/tla/TaskScheduler.tla @@ -516,15 +516,10 @@ SchedCheckFront(wid) == \* --- /\ LET tid == FrontQueue[1] t == Tasks[tid] IN /\ IF ArrLen(FrontQueue) = 1 THEN - \* The entire front queue is consumed. Consume the signal too. This - \* should be done before the queue becomes empty. Otherwise a new task - \* might arrive after the last task was popped and just before the front - \* signal is consumed. Then the queue would be non-empty but without - \* this signal and that would be a deadlock. - /\ IsFrontSignaled' = FALSE + \* The entire front queue is consumed. Switch to the next state. /\ WorkerThreads' = ArrSetState(wid, "sched_wait_front", WorkerThreads) ELSE - /\ UNCHANGED<> + /\ UNCHANGED<> /\ FrontQueue' = ArrPopHead(FrontQueue) \* Status check + change can be done via atomic compare-exchange. \* The 'wait' flag does not need to be atomic. It is never accessed by more @@ -545,7 +540,7 @@ SchedCheckFront(wid) == /\ UNCHANGED<> /\ WaitingQueue' = WaitingQueue \ {tid} /\ ReadyQueue' = ArrAppend(tid, ReadyQueue) - /\ UNCHANGED<> + /\ UNCHANGED<> \* If has no ready tasks then wait until anything comes to the front or the \* closest task-deadline expires. Keep the scheduler role during that. Other