Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion src/mg/sch/TaskScheduler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
11 changes: 3 additions & 8 deletions tla/TaskScheduler.tla
Original file line number Diff line number Diff line change
Expand Up @@ -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<<IsFrontSignaled, WorkerThreads>>
/\ UNCHANGED<<WorkerThreads>>
/\ 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
Expand All @@ -545,7 +540,7 @@ SchedCheckFront(wid) ==
/\ UNCHANGED<<Tasks>>
/\ WaitingQueue' = WaitingQueue \ {tid}
/\ ReadyQueue' = ArrAppend(tid, ReadyQueue)
/\ UNCHANGED<<IsReadySignaled, IsSchedulerTaken>>
/\ UNCHANGED<<IsFrontSignaled, IsReadySignaled, IsSchedulerTaken>>

\* 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
Expand Down