summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar BarryBo <barrybo@microsoft.com>2016-08-12 17:03:01 -0700
committerGravatar BarryBo <barrybo@microsoft.com>2016-08-12 17:03:01 -0700
commit032e256aa5fd566b14c231bc5d794eaaec9c1dae (patch)
treed4053ed98fb53fa54bb1f105b4833ef2bb6e76a2
parent2edc4a4e70b9dcf6fc91ddcc07fd500b705de5d2 (diff)
Fix deadlock in the new thread scheduler
Fix deadlock where a Boogie task schedules a task and waits on it. The .NET threadpool creates more threads than cores, up to a limit, which hides the issue. The new policy did not account for recursion and caused the newly-created tasks to wait forever for the earlier ones to complete.
-rw-r--r--Source/ExecutionEngine/ThreadTaskScheduler.cs81
1 files changed, 13 insertions, 68 deletions
diff --git a/Source/ExecutionEngine/ThreadTaskScheduler.cs b/Source/ExecutionEngine/ThreadTaskScheduler.cs
index 0b2c8594..58c4c6d4 100644
--- a/Source/ExecutionEngine/ThreadTaskScheduler.cs
+++ b/Source/ExecutionEngine/ThreadTaskScheduler.cs
@@ -14,59 +14,34 @@ namespace Microsoft.Boogie
// scheduler uses the .NET threadpool, which in turn inherits stack size from the EXE.
public class ThreadTaskScheduler : TaskScheduler
{
- private object tasklock; // Guards acess to the "tasks" queue
- private Queue<Task> tasks;
-
- private Thread[] dispatchers;
- private ManualResetEvent eventsWaiting;
private int stackSize;
public ThreadTaskScheduler(int StackReserveSize)
{
- int MaxThreads = System.Environment.ProcessorCount;
- Initialize(StackReserveSize, MaxThreads);
- }
-
- public ThreadTaskScheduler(int StackReserveSize, int MaxThreads)
- {
- Initialize(StackReserveSize, MaxThreads);
- }
-
- void Initialize(int StackReserveSize, int MaxThreads)
- {
Contract.Requires(StackReserveSize >= 0);
- Contract.Requires(MaxThreads > 0);
- tasklock = new object();
- tasks = new Queue<Task>();
- eventsWaiting = new ManualResetEvent(false);
stackSize = StackReserveSize;
- dispatchers = new Thread[MaxThreads];
- for (int i = 0; i < MaxThreads; ++i)
- {
- dispatchers[i] = new Thread(new ThreadStart(DispatcherMain));
- dispatchers[i].IsBackground = true;
- dispatchers[i].Start();
- }
}
protected override IEnumerable<Task> GetScheduledTasks()
{
- IEnumerable<Task> r;
- lock(tasklock)
- {
- r=tasks.ToArray<Task>();
- }
- return r;
+ // There is never a queue of scheduled, but not running, tasks.
+ // So return an empty list.
+ return new List<Task>();
}
protected override void QueueTask(Task task)
{
- lock (tasklock)
- {
- tasks.Enqueue(task);
- eventsWaiting.Set();
- }
+ // Each queued task runs on a newly-created thread with the required
+ // stack size. The default .NET task scheduler is built on the .NET
+ // ThreadPool. Its policy allows it to create thousands of threads
+ // if it chooses.
+ //
+ // Boogie creates tasks which in turn create tasks and wait on them.
+ // So throttling tasks via a queue risks deadlock.
+
+ Thread th = new Thread(TaskMain, stackSize);
+ th.Start(task);
}
protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
@@ -74,36 +49,6 @@ namespace Microsoft.Boogie
return false;
}
- private void DispatcherMain()
- {
- while (true)
- {
- Task t = null;
- lock (tasklock)
- {
- if (tasks.Count > 0)
- {
- t = tasks.Dequeue();
- if (tasks.Count == 0)
- {
- eventsWaiting.Reset();
- }
- }
- }
-
- if (t != null)
- {
- Thread th = new Thread(TaskMain, stackSize);
- th.Start(t);
- th.Join();
- }
- else
- {
- eventsWaiting.WaitOne();
- }
- }
- }
-
private void TaskMain(object data)
{
Task t = (Task)data;