-
Notifications
You must be signed in to change notification settings - Fork 114
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Use large threads for processing Boogie programs (#710)
* Use large threads for processing Boogie programs * Update nesting expect file to trigger stack overflow * Update Boogie version
- Loading branch information
1 parent
58ab092
commit ec72064
Showing
6 changed files
with
152 additions
and
22 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
69 changes: 69 additions & 0 deletions
69
Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| using System; | ||
| using System.Collections.Concurrent; | ||
| using System.Collections.Generic; | ||
| using System.Threading; | ||
| using System.Threading.Tasks; | ||
|
|
||
| namespace Microsoft.Boogie; | ||
|
|
||
| /// <summary> | ||
| /// Uses a thread pool of a configurable size, with threads with a configurable stack size, | ||
| /// to queue tasks. | ||
| /// </summary> | ||
| public class CustomStackSizePoolTaskScheduler : TaskScheduler, IDisposable | ||
| { | ||
| private readonly int threadCount; | ||
| private readonly AsyncQueue<Task> queue = new(); | ||
| private readonly Thread[] threads; | ||
|
|
||
| public static CustomStackSizePoolTaskScheduler Create(int stackSize, int threadCount) | ||
| { | ||
| return new CustomStackSizePoolTaskScheduler(stackSize, threadCount); | ||
| } | ||
|
|
||
| private CustomStackSizePoolTaskScheduler(int stackSize, int threadCount) | ||
| { | ||
| this.threadCount = threadCount; | ||
|
|
||
| threads = new Thread[this.threadCount]; | ||
| for (int i = 0; i < threads.Length; i++) | ||
| { | ||
| threads[i] = new Thread(WorkLoop, stackSize) { IsBackground = true }; | ||
| threads[i].Start(); | ||
| } | ||
| } | ||
|
|
||
| protected override void QueueTask(Task task) | ||
| { | ||
| queue.Enqueue(task); | ||
| } | ||
|
|
||
| protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued) | ||
| { | ||
| return TryExecuteTask(task); | ||
| } | ||
|
|
||
| public override int MaximumConcurrencyLevel => threadCount; | ||
|
|
||
| protected override IEnumerable<Task> GetScheduledTasks() | ||
| { | ||
| return queue.Items; | ||
| } | ||
|
|
||
| private void WorkLoop() | ||
| { | ||
| while (true) | ||
| { | ||
| var task = queue.Dequeue(CancellationToken.None).Result; | ||
| TryExecuteTask(task); | ||
| } | ||
| } | ||
|
|
||
| public void Dispose() | ||
| { | ||
| foreach (var thread in threads) | ||
| { | ||
| thread.Join(); | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,21 +1,21 @@ | ||
| nesting.bpl(46,35): Error: this assertion could not be proved | ||
| nesting.bpl(88,35): Error: this assertion could not be proved | ||
| Execution trace: | ||
| nesting.bpl(18,3): anon0 | ||
| nesting.bpl(19,5): anon17_Then | ||
| nesting.bpl(20,7): anon18_Then | ||
| nesting.bpl(21,9): anon19_Then | ||
| nesting.bpl(22,11): anon20_Then | ||
| nesting.bpl(23,13): anon21_Then | ||
| nesting.bpl(24,15): anon22_Then | ||
| nesting.bpl(25,17): anon23_Then | ||
| nesting.bpl(26,19): anon24_Then | ||
| nesting.bpl(27,21): anon25_Then | ||
| nesting.bpl(28,23): anon26_Then | ||
| nesting.bpl(29,25): anon27_Then | ||
| nesting.bpl(30,27): anon28_Then | ||
| nesting.bpl(31,29): anon29_Then | ||
| nesting.bpl(32,31): anon30_Then | ||
| nesting.bpl(33,33): anon31_Then | ||
| nesting.bpl(46,35): anon32_Then | ||
| nesting.bpl(60,3): anon0 | ||
| nesting.bpl(61,5): anon17_Then | ||
| nesting.bpl(62,7): anon18_Then | ||
| nesting.bpl(63,9): anon19_Then | ||
| nesting.bpl(64,11): anon20_Then | ||
| nesting.bpl(65,13): anon21_Then | ||
| nesting.bpl(66,15): anon22_Then | ||
| nesting.bpl(67,17): anon23_Then | ||
| nesting.bpl(68,19): anon24_Then | ||
| nesting.bpl(69,21): anon25_Then | ||
| nesting.bpl(70,23): anon26_Then | ||
| nesting.bpl(71,25): anon27_Then | ||
| nesting.bpl(72,27): anon28_Then | ||
| nesting.bpl(73,29): anon29_Then | ||
| nesting.bpl(74,31): anon30_Then | ||
| nesting.bpl(75,33): anon31_Then | ||
| nesting.bpl(88,35): anon32_Then | ||
|
|
||
| Boogie program verifier finished with 0 verified, 1 error |