bugfix: clear wsqueue when return to sched

MPLLang · Oct 2, 2023 · b6e21de · b6e21de
1 parent d741bab
commit b6e21de
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/basis-library/schedulers/hybrid/Scheduler.sml b/basis-library/schedulers/hybrid/Scheduler.sml
@@ -501,7 +501,10 @@ struct
       val myId = myWorkerId ()
       val {queue, ...} = vectorSub (workerLocalData, myId)
     in
-      Queue.clear queue
+      if Queue.size queue > 0 then
+        die (fn _ => "scheduler bug: clear on non-empty queue")
+      else
+        Queue.clear queue
     end
 
   fun popDiscard () =
@@ -1186,6 +1189,7 @@ struct
               ;*) Queue.setDepth myQueue depth
               ; threadSwitch thread
               ; afterReturnToSched ()
+              ; clear ()
               ; Queue.setDepth myQueue 1
               ; acquireWork ()
               )
@@ -1202,6 +1206,7 @@ struct
                 (* dbgmsg' (fn _ => "switch to new task thread"); *)
                 threadSwitch taskThread;
                 afterReturnToSched ();
+                clear ();
                 Queue.setDepth myQueue 1;
                 acquireWork ()
               end