diff options
Diffstat (limited to 'Source/ExecutionEngine')
-rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 4 | ||||
-rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.csproj | 1 | ||||
-rw-r--r-- | Source/ExecutionEngine/ThreadTaskScheduler.cs | 113 |
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); + } + } +} |