fix: Cancellation tokens to cancel and restart checkers (#497)

- Enable cancellation while waiting for input from the solver - Only recycle a `Checker` if its associated prover is responsive - Return a `PipelineOutcome.Cancelled` outcome if a request was cancelled. Co-authored-by: Mikael Mayer <[email protected]>
boogie-org · Feb 14, 2022 · 241dfcd · 241dfcd
1 parent 0b9f14d
commit 241dfcd
Show file tree

Hide file tree

Showing 20 changed files with 444 additions and 377 deletions.
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -204,6 +204,7 @@ public enum PipelineOutcome
     TypeCheckingError,
     ResolvedAndTypeChecked,
     FatalError,
+    Cancelled,
     VerificationCompleted
   }
 
@@ -1053,6 +1054,7 @@ public static PipelineOutcome InferAndVerify(Program program,
 
           if (e is OperationCanceledException)
           {
+            outcome = PipelineOutcome.Cancelled;
             return true;
           }
 
@@ -1148,7 +1150,7 @@ private static void CleanupCheckers(string requestId)
       {
         if (RequestIdToCancellationTokenSource.IsEmpty)
         {
-          checkerPool.Dispose();
+          checkerPool?.Dispose();
           checkerPool = null;
         }
       }
@@ -1207,16 +1209,14 @@ private static void VerifyImplementation(Program program, PipelineStatistics sta
             CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
           }
 
-          try
-          {
-            verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);
-            if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)
-            {
+          try {
+            var cancellationToken = RequestIdToCancellationTokenSource[requestId].Token;
+            verificationResult.Outcome =
+              vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId, cancellationToken);
+            if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null) {
               var vcg = vcgen as VCGen;
-              if (vcg != null)
-              {
-                for (int i = 0; i < verificationResult.Errors.Count; i++)
-                {
+              if (vcg != null) {
+                for (int i = 0; i < verificationResult.Errors.Count; i++) {
                   verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name,
                     program, extractLoopMappingInfo);
                 }

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
@@ -5,6 +5,7 @@
 using Microsoft.BaseTypes;
 using VC;
 using System.Linq;
+using System.Threading;
 
 namespace Microsoft.Boogie.Houdini
 {
@@ -256,7 +257,7 @@ public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionar
 
       VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);
       proverInterface.BeginCheck(descriptiveName, vc, handler);
-      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit);
+      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit, CancellationToken.None).Result;
 
       double queryTime = (DateTime.UtcNow - now).TotalSeconds;
       stats.proverTime += queryTime;
@@ -388,8 +389,8 @@ public void Explain(ProverInterface proverInterface,
       do
       {
         hardAssumptions.Add(controlExprNoop);
-        outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out var unsatisfiedSoftAssumptions,
-          handler);
+        (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, 
+          handler, CancellationToken.None).Result;
         hardAssumptions.RemoveAt(hardAssumptions.Count - 1);
 
         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
@@ -423,9 +424,8 @@ public void Explain(ProverInterface proverInterface,
           hardAssumptions.Add(softAssumptions[i]);
         }
 
-        var unsatisfiedSoftAssumptions2 = new List<int>();
-        outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2,
-          handler);
+        (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, 
+          handler, CancellationToken.None).Result;
 
         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
             outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined)
@@ -506,7 +506,7 @@ public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Variable
         assumptionExprs.Add(exprTranslator.LookupVariable(v));
       }
 
-      ProverInterface.Outcome tmp = proverInterface.CheckAssumptions(assumptionExprs, out var unsatCore, handler);
+      (ProverInterface.Outcome tmp, var unsatCore) = proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None).Result;
       System.Diagnostics.Debug.Assert(tmp == ProverInterface.Outcome.Valid);
       unsatCoreSet = new HashSet<Variable>();
       foreach (int i in unsatCore)

diff --git a/Source/Provers/SMTLib/NoopSolver.cs b/Source/Provers/SMTLib/NoopSolver.cs
@@ -1,4 +1,6 @@
 using System;
+using System.Threading;
+using System.Threading.Tasks;
 
 namespace Microsoft.Boogie.SMTLib;
 
@@ -34,11 +36,11 @@ public override void Send(string cmd)
     }
   }
 
-  public override SExpr GetProverResponse()
+  public override Task<SExpr> GetProverResponse()
   {
     var result = response;
     response = null;
-    return result;
+    return Task.FromResult(result);
   }
 
   public override void NewProblem(string descriptiveName)

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
@@ -15,4 +15,8 @@
     <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Include="System.Linq.Async" Version="6.0.1" />
+  </ItemGroup>
+
 </Project>