diff options
Diffstat (limited to 'Source/ExecutionEngine/ThreadTaskScheduler.cs')
-rw-r--r-- | Source/ExecutionEngine/ThreadTaskScheduler.cs | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/Source/ExecutionEngine/ThreadTaskScheduler.cs b/Source/ExecutionEngine/ThreadTaskScheduler.cs new file mode 100644 index 00000000..58c4c6d4 --- /dev/null +++ b/Source/ExecutionEngine/ThreadTaskScheduler.cs @@ -0,0 +1,58 @@ +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 int stackSize; + + public ThreadTaskScheduler(int StackReserveSize) + { + Contract.Requires(StackReserveSize >= 0); + + stackSize = StackReserveSize; + } + + protected override IEnumerable<Task> GetScheduledTasks() + { + // 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) + { + // 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) + { + return false; + } + + private void TaskMain(object data) + { + Task t = (Task)data; + TryExecuteTask(t); + } + } +} |