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/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<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