From 44f0dff3c149b34998e541cd9c278eae74b440f2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 12 Aug 2024 20:18:10 -0500 Subject: [PATCH 1/2] Fix: Spurious message of checkerpool already disposed. Looking at the CI result of https://github.com/dafny-lang/dafny/actions/runs/10330235840/job/28615735562?pr=5675, I see like often: ``` System.Exception: CheckerPool was already disposed at VC.CheckerPool.FindCheckerFor(Program program, Split split, CancellationToken cancellationToken) at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken cancellationToken)+MoveNext() at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken ``` This PR hopefully fixes this message --- Source/ExecutionEngine/VerificationTask.cs | 2 +- Source/VCGeneration/CheckerPool.cs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 297d7619d..267dd7f27 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -116,7 +116,7 @@ public void Cancel() { private async IAsyncEnumerable StartRun([EnumeratorCancellation] CancellationToken cancellationToken) { var timeout = Split.Run.Implementation.GetTimeLimit(Split.Options); - var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, CancellationToken.None); + var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, cancellationToken); if (!checkerTask.IsCompleted) { yield return new Queued(); } diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs index b75744377..2978ad229 100644 --- a/Source/VCGeneration/CheckerPool.cs +++ b/Source/VCGeneration/CheckerPool.cs @@ -23,12 +23,12 @@ public CheckerPool(VCGenOptions options) public async Task FindCheckerFor(Program program, Split? split, CancellationToken cancellationToken) { - if (disposed) { - throw new Exception("CheckerPool was already disposed"); - } - await checkersSemaphore.WaitAsync(cancellationToken); try { + if (disposed) { // Now that should not happen + throw new Exception("CheckerPool was already disposed"); + } + if (!availableCheckers.TryPop(out var checker)) { checker ??= CreateNewChecker(); } From ab87a4ff1b92a5ab0c95bace721e966375461171 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 12 Aug 2024 21:27:52 -0500 Subject: [PATCH 2/2] Map the disposed issue to OperationCanceledException, which should be captured. --- Source/ExecutionEngine/VerificationTask.cs | 2 +- Source/VCGeneration/CheckerPool.cs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 267dd7f27..297d7619d 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -116,7 +116,7 @@ public void Cancel() { private async IAsyncEnumerable StartRun([EnumeratorCancellation] CancellationToken cancellationToken) { var timeout = Split.Run.Implementation.GetTimeLimit(Split.Options); - var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, cancellationToken); + var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, CancellationToken.None); if (!checkerTask.IsCompleted) { yield return new Queued(); } diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs index 2978ad229..a1c962948 100644 --- a/Source/VCGeneration/CheckerPool.cs +++ b/Source/VCGeneration/CheckerPool.cs @@ -23,12 +23,12 @@ public CheckerPool(VCGenOptions options) public async Task FindCheckerFor(Program program, Split? split, CancellationToken cancellationToken) { + if (disposed) { + throw new OperationCanceledException("CheckerPool was already disposed"); + } + await checkersSemaphore.WaitAsync(cancellationToken); try { - if (disposed) { // Now that should not happen - throw new Exception("CheckerPool was already disposed"); - } - if (!availableCheckers.TryPop(out var checker)) { checker ??= CreateNewChecker(); }