Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use large threads for processing Boogie programs #710

Merged
merged 10 commits into from
Mar 31, 2023
Merged

Use large threads for processing Boogie programs #710

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
29befa8
Use large threads for processing Boogie programs
keyboardDrummer Mar 29, 2023
f033292
Merge remote-tracking branch 'origin/master' into largeThreads
keyboardDrummer Mar 29, 2023
fa566bf
Update nesting expect file to trigger stack overflow
keyboardDrummer Mar 29, 2023
bf9e673
Update Boogie version
keyboardDrummer Mar 29, 2023
d8783c0
Add comment to test file
keyboardDrummer Mar 29, 2023
9e8fc99
Add license and attribution
keyboardDrummer Mar 29, 2023
1aab6f6
Use hand written custom stack size pool task scheduler
keyboardDrummer Mar 30, 2023
1c05ad4
Refactoring
keyboardDrummer Mar 30, 2023
ca0e62c
Use AsyncQueue instead of SemaphoreSlim and ConcurrentQueue
keyboardDrummer Mar 31, 2023
b0b2d0b
Limit amount of large threads to configured amount
keyboardDrummer Mar 31, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions Source/Core/AsyncQueue.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,17 @@ public void Enqueue(T value)
}
}

public IEnumerable<T> Items
{
get
{
lock (myLock)
{
return items.ToArray();
}
}
}

public Task<T> Dequeue(CancellationToken cancellationToken)
{
lock (myLock) {
Expand Down
2 changes: 1 addition & 1 deletion Source/Directory.Build.props
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

<!-- Target framework and package configuration -->
<PropertyGroup>
<Version>2.16.3</Version>
<Version>2.16.4</Version>
<TargetFramework>net6.0</TargetFramework>
<GeneratePackageOnBuild>false</GeneratePackageOnBuild>
<Authors>Boogie</Authors>
Expand Down
69 changes: 69 additions & 0 deletions Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
View file
Open in desktop
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();
}
}
}
14 changes: 11 additions & 3 deletions Source/ExecutionEngine/ExecutionEngine.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,15 @@ public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {

public class ExecutionEngine : IDisposable
{
/// <summary>
/// Boogie traverses the Boogie and VCExpr AST using the call-stack,
/// so it needs to use a large stack to prevent stack overflows.
/// </summary>
private readonly TaskFactory largeThreadTaskFactory;

static int autoRequestIdCount;

static readonly string AutoRequestIdPrefix = "auto_request_id_";
private const string AutoRequestIdPrefix = "auto_request_id_";

public static string FreshRequestId() {
var id = Interlocked.Increment(ref autoRequestIdCount);
Expand Down Expand Up @@ -63,6 +68,9 @@ public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache c
Cache = cache;
checkerPool = new CheckerPool(options);
verifyImplementationSemaphore = new SemaphoreSlim(Options.VcsCores);

var largeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, Options.VcsCores);
largeThreadTaskFactory = new(CancellationToken.None, TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, largeThreadScheduler);
}

public static ExecutionEngine CreateWithoutSharedCache(ExecutionEngineOptions options) {
Expand Down Expand Up @@ -870,7 +878,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
var verificationResult = new VerificationResult(impl, programId);

var batchCompleted = new Subject<(Split split, VCResult vcResult)>();
var completeVerification = Task.Run(async () =>
var completeVerification = largeThreadTaskFactory.StartNew(async () =>
{
var vcgen = new VCGen(processedProgram.Program, checkerPool);
vcgen.CachingActionCounts = stats.CachingActionCounts;
Expand Down Expand Up @@ -931,7 +939,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc

batchCompleted.OnCompleted();
return new Completed(verificationResult);
}, cancellationToken);
}, cancellationToken).Unwrap();

return batchCompleted.Select(t => new BatchCompleted(t.split, t.vcResult)).Merge<IVerificationStatus>(Observable.FromAsync(() => completeVerification));
}
Expand Down
42 changes: 42 additions & 0 deletions Test/stackoverflow/nesting.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
// RUN: %parallel-boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

type Ref;
type Field A B;
type HeapType = <A, B> [Ref, Field A B]B; // Using type parameters and the ==> operator can trigger the OpTypeEraser visitor which can cause stack overflows.

procedure foo(n: int)
requires true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true
|| true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true ||
Expand All @@ -14,6 +19,43 @@ procedure foo(n: int)
true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true
|| true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true ||
n == 2;
requires true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true;

{
if (n == 2) {
if (n == 2) {
Expand Down
36 changes: 18 additions & 18 deletions Test/stackoverflow/nesting.bpl.expect
View file
Open in desktop
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