Change logic related to disposed checkerPools (#941)

boogie-org · Aug 19, 2024 · 16c53d9 · 16c53d9
1 parent e7a229e
commit 16c53d9
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs
@@ -89,6 +89,8 @@ public void Cancel() {
 
     StartRun(cancellationSource.Token).ToObservable().
       Catch<IVerificationStatus, OperationCanceledException>(_ => Observable.Return(new Stale())).
+      Catch<IVerificationStatus, ObjectDisposedException>(e => cancellationSource.IsCancellationRequested 
+        ? Observable.Return(new Stale()) : Observable.Throw<IVerificationStatus>(e)).
       Subscribe(next => {
         status.OnNext(next);
       }, e => {
@@ -115,8 +117,8 @@ public void Cancel() {
 
   private async IAsyncEnumerable<IVerificationStatus> 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
@@ -23,10 +23,6 @@ public CheckerPool(VCGenOptions options)
 
     public async Task<Checker> FindCheckerFor(Program program, Split? split, CancellationToken cancellationToken)
     {
-      if (disposed) {
-        throw new Exception("CheckerPool was already disposed");
-      }
-
       await checkersSemaphore.WaitAsync(cancellationToken);
       try {
         if (!availableCheckers.TryPop(out var checker)) {
@@ -43,6 +39,11 @@ public async Task<Checker> FindCheckerFor(Program program, Split? split, Cancell
     private int createdCheckers;
     private Checker CreateNewChecker()
     {
+      if (disposed)
+      {
+        throw new ObjectDisposedException(nameof(CheckerPool));
+      }
+
       var log = Options.ProverLogFilePath;
       var index = Interlocked.Increment(ref createdCheckers) - 1;
       if (log != null && !log.Contains("@PROC@") && index > 0) {
@@ -57,6 +58,7 @@ public void Dispose()
       lock(availableCheckers)
       {
         disposed = true;
+        checkersSemaphore.Dispose();
         while (availableCheckers.TryPop(out var checker)) {
           checker.Close();
         }