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