summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar BarryBo <barrybo@microsoft.com>2016-07-22 15:27:54 -0700
committerGravatar BarryBo <barrybo@microsoft.com>2016-07-22 15:27:54 -0700
commit2edc4a4e70b9dcf6fc91ddcc07fd500b705de5d2 (patch)
tree3d06ac193219915b2f43320bd91402115b44fa05 /Source
parent0632d3956b7cd10cdc4975cdfc669b73892a121d (diff)
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.
Diffstat (limited to 'Source')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs4
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.csproj1
-rw-r--r--Source/ExecutionEngine/ThreadTaskScheduler.cs113
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);
+ }
+ }
+}