Use large threads for processing Boogie programs #710
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,78 @@ | ||
| 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 ConcurrentQueue<Task> queue = new(); | ||
| private readonly SemaphoreSlim isWorkAvailable = new(0); | ||
| 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); | ||
| isWorkAvailable.Release(1); | ||
| } | ||
|
|
||
| protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued) | ||
| { | ||
| return TryExecuteTask(task); | ||
| } | ||
|
|
||
| public override int MaximumConcurrencyLevel => threadCount; | ||
|
|
||
| protected override IEnumerable<Task> GetScheduledTasks() | ||
| { | ||
| return queue; | ||
| } | ||
|
|
||
| private void WorkLoop() | ||
| { | ||
| while (true) | ||
| { | ||
| var task = BlockUntilTaskIsAvailable(); | ||
| TryExecuteTask(task); | ||
| } | ||
| } | ||
|
|
||
| private Task BlockUntilTaskIsAvailable() | ||
| { | ||
| isWorkAvailable.Wait(); | ||
| queue.TryDequeue(out var task); | ||
| return 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -26,10 +26,14 @@ public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) { | |
|
|
||
| public class ExecutionEngine : IDisposable | ||
| { | ||
| private static readonly CustomStackSizePoolTaskScheduler largeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, Environment.ProcessorCount); | ||
|
There was a problem hiding this comment. Worth a quick comment stating why we need such a deep stack, maybe point to #711 |
||
| private static readonly TaskFactory largeThreadTaskFactory = new( | ||
| CancellationToken.None, TaskCreationOptions.DenyChildAttach, | ||
| TaskContinuationOptions.None, largeThreadScheduler); | ||
|
|
||
| static int autoRequestIdCount; | ||
|
|
||
| private const string AutoRequestIdPrefix = "auto_request_id_"; | ||
|
|
||
| public static string FreshRequestId() { | ||
| var id = Interlocked.Increment(ref autoRequestIdCount); | ||
|
|
@@ -870,7 +874,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc | |
| var verificationResult = new VerificationResult(impl, programId); | ||
|
|
||
| var batchCompleted = new Subject<(Split split, VCResult vcResult)>(); | ||
| var completeVerification = largeThreadTaskFactory.StartNew(async () => | ||
| { | ||
| var vcgen = new VCGen(processedProgram.Program, checkerPool); | ||
| vcgen.CachingActionCounts = stats.CachingActionCounts; | ||
|
|
@@ -931,7 +935,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc | |
|
|
||
| batchCompleted.OnCompleted(); | ||
| return new Completed(verificationResult); | ||
| }, cancellationToken).Unwrap(); | ||
|
|
||
| return batchCompleted.Select(t => new BatchCompleted(t.split, t.vcResult)).Merge<IVerificationStatus>(Observable.FromAsync(() => completeVerification)); | ||
| } | ||
|
|
||
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(88,35): Error: this assertion could not be proved | ||
| Execution trace: | ||
| 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 |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Worth a comment saying we don't need to check the return value or if
taskis null because of the separate semaphore (too badConcurrentQueuedoesn't have a plain blockingDequeuemethod).There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Changed the implementation to use
AsyncQueue, which has the behavior you were hoping for fromConcurrentQueue.