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.

1 files changed, 113 insertions, 0 deletions

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<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;
+    }
+
+    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);
+    }
+  }
+}