From 2edc4a4e70b9dcf6fc91ddcc07fd500b705de5d2 Mon Sep 17 00:00:00 2001 From: BarryBo Date: Fri, 22 Jul 2016 15:27:54 -0700 Subject: Run Boogie code on threads with large stacks Replace TaskScheduler.Default by a custom TaskScheduler. The .Default uses threadpool threads whose stack size is controlled by the host EXE header. The new ThreadTaskScheduler give Boogie control over the stack size, and defaults to 16mb. --- Source/ExecutionEngine/ThreadTaskScheduler.cs | 113 ++++++++++++++++++++++++++ 1 file changed, 113 insertions(+) create mode 100644 Source/ExecutionEngine/ThreadTaskScheduler.cs (limited to 'Source/ExecutionEngine/ThreadTaskScheduler.cs') diff --git a/Source/ExecutionEngine/ThreadTaskScheduler.cs b/Source/ExecutionEngine/ThreadTaskScheduler.cs new file mode 100644 index 00000000..0b2c8594 --- /dev/null +++ b/Source/ExecutionEngine/ThreadTaskScheduler.cs @@ -0,0 +1,113 @@ +using System; +using System.Collections.Generic; +using System.Collections.Concurrent; +using System.Diagnostics.Contracts; +using System.Linq; +using System.Text; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Boogie +{ + // Implementation of System.Threading.Tasks.TaskScheduler which creates a unique thread per + // task, and allows each thread to have its own custom stack size. The standard + // 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 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(); + 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 GetScheduledTasks() + { + IEnumerable r; + lock(tasklock) + { + r=tasks.ToArray(); + } + return r; + } + + protected override void QueueTask(Task task) + { + lock (tasklock) + { + tasks.Enqueue(task); + eventsWaiting.Set(); + } + } + + protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued) + { + 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; + TryExecuteTask(t); + } + } +} -- cgit v1.2.3 From 032e256aa5fd566b14c231bc5d794eaaec9c1dae Mon Sep 17 00:00:00 2001 From: BarryBo Date: Fri, 12 Aug 2016 17:03:01 -0700 Subject: 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. --- Source/ExecutionEngine/ThreadTaskScheduler.cs | 81 +++++---------------------- 1 file changed, 13 insertions(+), 68 deletions(-) (limited to 'Source/ExecutionEngine/ThreadTaskScheduler.cs') 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 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(); - 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 GetScheduledTasks() { - IEnumerable r; - lock(tasklock) - { - r=tasks.ToArray(); - } - return r; + // There is never a queue of scheduled, but not running, tasks. + // So return an empty list. + return new List(); } 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; -- cgit v1.2.3