From 2edc4a4e70b9dcf6fc91ddcc07fd500b705de5d2 Mon Sep 17 00:00:00 2001
From: BarryBo <barrybo@microsoft.com>
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/ExecutionEngine.cs     |   4 +-
 Source/ExecutionEngine/ExecutionEngine.csproj |   1 +
 Source/ExecutionEngine/ThreadTaskScheduler.cs | 113 ++++++++++++++++++++++++++
 3 files changed, 117 insertions(+), 1 deletion(-)
 create mode 100644 Source/ExecutionEngine/ThreadTaskScheduler.cs

(limited to 'Source')

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);
+    }
+  }
+}
-- 
cgit v1.2.3