3 files changed, 63 insertions, 2 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 b0f77125..c715a631 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -8,7 +8,7 @@
     <OutputType>Library</OutputType>
     <AppDesignerFolder>Properties</AppDesignerFolder>
     <RootNamespace>ExecutionEngine</RootNamespace>
-    <AssemblyName>ExecutionEngine</AssemblyName>
+    <AssemblyName>BoogieExecutionEngine</AssemblyName>
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
     <FileAlignment>512</FileAlignment>
     <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">
@@ -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..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);
+    }
+  }
+}