fix: Cancellation tokens to cancel and restart checkers #497

keyboardDrummer · 2022-02-10T13:33:04Z

This PR enables Boogie's execution engine to effectively kill verification on demand, and recycle killed checkers/SMTLib processes

Changes

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.

Issues it fixes

This PR should be able to fix the following bugs:
dafny-lang/ide-vscode#119
dafny-lang/ide-vscode#114
dafny-lang/ide-vscode#96

How it has been tested

Add a unit test InferAndVerifyCanBeCancelledWhileWaitingForProver
Dafny tests
fix: "Stuck on Verifying..." dafny-lang/dafny#1771
It takes a program which is hard to verify, and two changes that makes it easy to verify and then a parse error.
Without this PR, the test fails and loops indefinitely on the first program.
With this PR, the tests succeeds and all the changes are taken into account.

Source/VCGeneration/CheckerPool.cs

…e into cancellationToken2

This reverts commit cbecd05.

…edException

…nd do not let SMTLibProcess have cancellation support

…e into cancellationToken2

cpitclaudel

I don't have enough context to do a sufficient review, but this looks very nice. Can you say why you can ignore the CancelledException early on?

cpitclaudel · 2022-02-11T16:31:45Z

Source/Provers/SMTLib/SMTLibProcess.cs

+      lock (this) {
+        if (outputReceivers.TryDequeue(out var source)) {
+          source.SetResult(null);
+        }


Could there be more than one item in the queue here? Is it safe to remove just one?

There's a while so it should remove all of them. I guess you reviewed an older version with just an if :)

There cannot be two things waiting for it in our current code be because we always prefix the calls to getProverResponse with await. However, as a safeguard for future problems that are unlikely to happend, we added the comment that this class is not thread-safe, meaning it should be also used only with one thread (which is what happens, it is owned by a Checker that runs the prover on only one thread.)

I guess you reviewed an older version with just an if :)

!! Precisely right :)

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

cpitclaudel · 2022-02-11T16:36:19Z

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -632,12 +644,12 @@ private void RecoverIfProverCrashedAfterReset()

    public override void FullReset(VCExpressionGenerator gen)
    {
-      if (options.Solver == SolverKind.Z3)
+      if (options.Solver == SolverKind.Z3 || options.Solver == SolverKind.NoOpWithZ3Options)


cpitclaudel · 2022-02-11T16:37:34Z

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

+      }
+      SendThisVC("(push 1)");
+      var result = action();
+      popLater = true;


This function always set poplater to true, right?

I'm not a fan of this API and its out popLater parameter, but I'm fine with sticking with what the code used to do.

cpitclaudel · 2022-02-11T16:39:46Z

Source/VCGeneration/Checker.cs

-        hasOutput = true;
-        proverRunTime = DateTime.UtcNow - proverStart;
+      switch (outcome)
+      {


This would be a good use case for a dictionary

I can't find the code on which you made this comment, so I don't know how to reply.

I think it's the switch that converts the outcome to a string..

The code is the switch on outcome in WaitForOutput. But since all that this PR does to it is reindent it, it's probably not worth changing it.

atomb

I think this looks great, and seems to simplify code and add functionality at the same time. I'd just like to confirm that issue #487 (fixed in PR #488) doesn't reappear.

atomb · 2022-02-11T23:05:58Z

Source/VCGeneration/ConditionGeneration.cs

@@ -39,8 +39,6 @@ public ConditionGenerationContracts(Program p, CheckerPool checkerPool)
  [ContractClass(typeof(ConditionGenerationContracts))]
  public abstract class ConditionGeneration : IDisposable
  {
-    protected internal object CheckerCommonState;
-


atomb · 2022-02-11T23:07:37Z

Source/VCGeneration/ProverInterface.cs

-  public virtual string[] CalculatePath(int controlFlowConstant)
-  {
-    throw new System.NotImplementedException();
-  }


Oh, nice! This doesn't need to be here?

Not for https://github.com/boogie-org/boogie, but possibly for a consumer of https://github.com/boogie-org/boogie, although I don't see why you would want to override this. For APIs that are [unexpectedly] used outside of Boogie, we should document the use-case and mark the API with an annotation, like [PublicAPI], otherwise it'll be impossible to make changes to Boogie without fear of breaking a consumer.

atomb · 2022-02-11T23:10:45Z

Source/VCGeneration/SplitAndVerifyWorker.cs

        split.ReleaseChecker();
-        throw;


Have you tested this against a badly-behaved prover? I'm worried that this could undo the fix from #488.

Since we don't catch the exception, we also don't have to rethrow it since it's thrown up automatically. Where does your concern come from?

Ah, right, the change from catch to finally should avoid it. And there is a test that would be failing if this change did undo that fix. 👍

atomb · 2022-02-11T23:35:32Z

Source/VCGeneration/Checker.cs

-    /// </summary>
-    public Checker(CheckerPool pool, VC.ConditionGeneration vcgen, Program prog, string /*?*/ logFilePath, bool appendLogFile,
-      Split split, ProverContext ctx = null)
+    public Checker(CheckerPool pool, string /*?*/ logFilePath, bool appendLogFile)


I like that Checker is no longer initialized with program-specific data.

cpitclaudel · 2022-02-14T20:45:28Z

Source/Provers/SMTLib/SMTLibProcess.cs

+      while (true) {
+        var exprs = await ParseSExprs(true).ToListAsync();
+        Contract.Assert(exprs.Count <= 1);
+        if (exprs.Count == 0) {
          return null;
        }

        var resp = exprs[0];


The existing code ignores possible malformed output from the underlying prover, right? I guess it's OK since it was already like that.

Source/Provers/SMTLib/SMTLibProcess.cs

cpitclaudel · 2022-02-14T20:47:48Z

Source/Provers/SMTLib/SMTLibProcess.cs

-          HandleError(error);
-          errorCnt++;
-          error = null;
+      lock (this) {


Do you want external clients to be able take this lock? If not I'd use a private object.

Oh but I see below that the code was already like this, sorry

Ah, good point. Never thought of that. Is it worth the extra code though? External clients taking the lock seems like only a theoretical issue.

cpitclaudel · 2022-02-14T20:49:44Z

Source/Provers/SMTLib/SMTLibProcess.cs

-      {
-        if (e.Data != null)
+      lock (this) {
+        if (e.Data == null)


In the method above you moved the e.data test out of the lock, but not here. Could you do the same here? It would avoid taking the lock when e.Data is null

cpitclaudel

LGTM, none of my comments are blocking

keyboardDrummer added 4 commits February 9, 2022 14:47

Enable cancelling in SplitAndVerifyWorker

e4d2c11

Push cancellationToken down into SMTLibProcessTheoremProver

d120ed0

Push CancellationToken into SMTLibProcess

5ebf252

Kill process if it doesn't become idle

cef3205

keyboardDrummer mentioned this pull request Feb 10, 2022

feat: Ability to kill verification #491

Closed

keyboardDrummer commented Feb 10, 2022

View reviewed changes

Source/VCGeneration/CheckerPool.cs Show resolved Hide resolved

Checker waiters can continue with a fresh new checker.

cbecd05

MikaelMayer assigned keyboardDrummer and MikaelMayer Feb 10, 2022

MikaelMayer added the bug label Feb 10, 2022

MikaelMayer changed the title ~~Cancellation token2~~ fix: Cancellation tokens to cancel checkers Feb 10, 2022

MikaelMayer changed the title ~~fix: Cancellation tokens to cancel checkers~~ fix: Cancellation tokens to cancel and restart checkers Feb 10, 2022

keyboardDrummer added 13 commits February 11, 2022 11:55

Add test

8b3f264

Merge branch 'cancellationToken2' of github.com:keyboardDrummer/boogi…

5df1ae2

…e into cancellationToken2

Revert "Checker waiters can continue with a fresh new checker."

d12b905

This reverts commit cbecd05.

Stop Checker.WaitForOutput correctly from swallowing OperationCancell…

5ed982b

…edException

Correctly handle dead checkers

efe44ee

Record a cancelled pipeline outcome

88be748

Use log variable

3320ffb

Refactoring and allow checkers to be recycled

e003b78

Let SMTLibProcess wait for the solver using a TaskCompletionSource, a…

ccdfd34

…nd do not let SMTLibProcess have cancellation support

Shorten test program

6dac526

Small tweaks

71144bc

Fix rename feature

5e3111f

Fix off by one error

7a30748

keyboardDrummer marked this pull request as ready for review February 11, 2022 15:19

keyboardDrummer added 2 commits February 11, 2022 17:33

Refactoring

2f1c0b5

Make sure we don't run into issues with an aggregateException

840d12d

keyboardDrummer requested a review from atomb February 11, 2022 16:36

Refactoring to remove code duplication

c926f8f

Merge branch 'cancellationToken2' of github.com:keyboardDrummer/boogi…

7014ead

…e into cancellationToken2

cpitclaudel reviewed Feb 11, 2022

View reviewed changes

atomb requested changes Feb 11, 2022

View reviewed changes

keyboardDrummer requested review from atomb and cpitclaudel February 14, 2022 11:17

atomb approved these changes Feb 14, 2022

View reviewed changes

cpitclaudel reviewed Feb 14, 2022

View reviewed changes

Source/Provers/SMTLib/SMTLibProcess.cs Show resolved Hide resolved

cpitclaudel reviewed Feb 14, 2022

View reviewed changes

cpitclaudel approved these changes Feb 14, 2022

View reviewed changes

keyboardDrummer merged commit 241dfcd into boogie-org:master Feb 14, 2022

keyboardDrummer deleted the cancellationToken2 branch February 14, 2022 21:21

keyboardDrummer mentioned this pull request Feb 14, 2022

VS Code extension hangs on last method dafny-lang/ide-vscode#140

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix: Cancellation tokens to cancel and restart checkers #497

fix: Cancellation tokens to cancel and restart checkers #497

keyboardDrummer commented Feb 10, 2022 •

edited

Loading

cpitclaudel left a comment

cpitclaudel Feb 11, 2022

keyboardDrummer Feb 11, 2022 •

edited

Loading

MikaelMayer Feb 11, 2022

cpitclaudel Feb 11, 2022

cpitclaudel Feb 11, 2022

cpitclaudel Feb 11, 2022

keyboardDrummer Feb 14, 2022

cpitclaudel Feb 14, 2022

cpitclaudel Feb 11, 2022

keyboardDrummer Feb 14, 2022

MikaelMayer Feb 14, 2022

cpitclaudel Feb 14, 2022

atomb left a comment

atomb Feb 11, 2022

atomb Feb 11, 2022

keyboardDrummer Feb 14, 2022

atomb Feb 11, 2022

keyboardDrummer Feb 14, 2022

atomb Feb 14, 2022

atomb Feb 11, 2022

cpitclaudel Feb 14, 2022

cpitclaudel Feb 14, 2022 •

edited

Loading

cpitclaudel Feb 14, 2022

keyboardDrummer Feb 15, 2022

cpitclaudel Feb 14, 2022

cpitclaudel left a comment

fix: Cancellation tokens to cancel and restart checkers #497

fix: Cancellation tokens to cancel and restart checkers #497

Conversation

keyboardDrummer commented Feb 10, 2022 • edited Loading

Changes

Issues it fixes

How it has been tested

cpitclaudel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Feb 11, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel Feb 14, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Feb 10, 2022 •

edited

Loading

keyboardDrummer Feb 11, 2022 •

edited

Loading

cpitclaudel Feb 14, 2022 •

edited

Loading