diff options
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 4 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.csproj | 1 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ThreadTaskScheduler.cs | 58 | ||||
| -rw-r--r-- | Test/civl/ticket.bpl | 25 | ||||
| -rw-r--r-- | Test/civl/ticket.bpl.expect | 2 |
5 files changed, 81 insertions, 9 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..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); + } + } +} diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl index df19aae4..2e0c6cd1 100644 --- a/Test/civl/ticket.bpl +++ b/Test/civl/ticket.bpl @@ -7,7 +7,7 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); type X; const nil: X; -var {:layer 0,2} t: int; +var {:layer 0,1} t: int; var {:layer 0,2} s: int; var {:layer 0,2} cs: X; var {:layer 0,2} T: [int]bool; @@ -41,14 +41,15 @@ ensures {:layer 1} {:layer 2} xl != nil; } procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) -requires {:layer 2} xls' == MapConstBool(true); +requires {:layer 1} Inv1(T, t); +requires {:layer 2} xls' == MapConstBool(true) && Inv2(T, s, cs); { var {:linear "tid"} tid: X; var {:linear "tid"} xls: [X]bool; - yield; + par Yield1() | Yield2(); - call Init(xls'); + call InitAbstract(xls'); xls := xls'; par Yield1() | Yield2(); @@ -96,10 +97,20 @@ ensures {:layer 2} Inv2(T, s, cs) && cs == tid; par Yield1() | Yield2() | YieldSpec(tid); } +procedure {:yields} {:layer 1,2} InitAbstract({:linear "tid"} xls:[X]bool) +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T, t); +ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; s := 0; T := RightOpen(0); return true; }|; +{ + par Yield1(); + call Init(xls); + par Yield1(); +} + procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int) requires {:layer 1} Inv1(T, t); ensures {:layer 1} Inv1(T, t); -ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|; +ensures {:right} |{ A: havoc m; assume !T[m]; T[m] := true; return true; }|; { par Yield1(); call m := GetTicket(tid); @@ -130,7 +141,7 @@ ensures {:layer 1} Inv1(T,t); assert {:layer 1} Inv1(T,t); } -procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool); +procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool); ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int); @@ -140,7 +151,7 @@ procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int); ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); -ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; +ensures {:atomic} |{ A: assert cs == tid; s := s + 1; cs := nil; return true; }|; procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); ensures {:atomic} |{ A: assume xl != nil; return true; }|; diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect index dc45a0ee..6696bdbd 100644 --- a/Test/civl/ticket.bpl.expect +++ b/Test/civl/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 24 verified, 0 errors +Boogie program verifier finished with 26 verified, 0 errors |