Merge pull request #41 from BarryBo/master

Run Boogie code on threads with large stacks

3 files changed, 117 insertions, 1 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 9bc855be..5a22cc15 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -443,6 +443,8 @@ namespace Microsoft.Boogie
 
     static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
 
+    static ThreadTaskScheduler Scheduler = new ThreadTaskScheduler(16 * 1024 * 1024);
+
     public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)
     {
       Contract.Requires(cce.NonNullElements(fileNames));
@@ -977,7 +979,7 @@ namespace Microsoft.Boogie
               {                  
                   break;
               }
-              tasks[j].Start(TaskScheduler.Default);
+              tasks[j].Start(Scheduler);
           }
 
           // Don't wait for tasks that haven't been started yet.
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index b17b1139..c715a631 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -131,6 +131,7 @@
   <ItemGroup>
     <Compile Include="ExecutionEngine.cs" />
     <Compile Include="Properties\AssemblyInfo.cs" />
+    <Compile Include="ThreadTaskScheduler.cs" />
     <Compile Include="VerificationResultCache.cs" />
   </ItemGroup>
   <ItemGroup>
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);
+    }
+  }
+}