summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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);
+ }
+ }
+}