Add Prover Based ShutdownManager #489

baierd · 2025-05-30T19:01:06Z

Most solvers allow either re-usable shutdown or we use shared environments that are created per prover, making them isolated enough to be shut down without stopping the context.

This PR adds a controlled way of shutting down only a single prover with the manager returned by our API IFF it is supported by the solver. These prover shutdown managers are all children of the context given shutdown manager.

This should only be merged after #501, is this branch is merged here.

This reverts commit 3a62853.

kfriedberger

Overall, I find the idea good. It matches our architectural guidelines and solves a clear problem. The PR needs some minor improvements.

kfriedberger · 2025-06-01T13:21:14Z

src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java

+   *     ProverEnvironment}.
+   * @throws UnsupportedOperationException if the solver does not support prover specific shutdown.
+   */
+  ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException;


Due to API change, better provide a default implementation that throws the UnsupportedException.

Additionally, his method is a plain getter. Why does a plain getter throw such an exception? The getter itself does not depend on solver-features that could be unsupported, but only on JavaSMT-internal code. Perhaps just remove the exception from signature.

Thanks for the feedback! I removed the exception from the signature and added a default implementation.

kfriedberger · 2025-06-01T13:24:05Z

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

+    return getShutdownManagerForProverImpl();
+  }
+
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {


As this method is not generic, we do not need it. just use inline it in the normal getShutdoenManagerForProver.
With a default implementation in the API, we can even remove this implmentation completely and just mark the overridden method as abstract.

True. I imagined that i need more solver specific code, but i didn't. I removed it. Thanks for the feedback!

kfriedberger · 2025-06-01T13:37:40Z

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

+          return proverShutdownManager
+              .getNotifier()
+              .shouldShutdown(); // shutdownNotifer is defined in the
+          // superclass


The comment is formatted ugly, and it might not be understandable, please rephrase.

Is getNotifier() a "fast" method call or does it construct any objects? The callback is expected to be executed quite often from native solver code. We could store the notifier directly within the class and just reuse it.

Addtiionally, we already have a method for getting the manager. Why do we then use direct access here? Please use the getter.

I removed the comment, as the new default should be obvious.

getNotifier() does not construct any objects, it just returns the notifier that is created when the ShutdownManager is created. You can argue that it is faster to have the reference directly, but this is built once when the prover is created. I changed it so that the notifier is generally accessible directly in the superclass.

Thanks for the feedback!

kfriedberger · 2025-06-01T13:38:44Z

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -119,7 +123,8 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
      return false;
    } else if (resultValue == Result.UNSAT) {
      return true;
-    } else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) {
+    } else if (resultValue == Result.UNKNOWN
+        && proverShutdownManager.getNotifier().shouldShutdown()) {


Is it guaranteed that the manager always returns the same notifier-instance and the notifier always returns the same flag?

Yes! The notifier is created final and only once, see here: private final ShutdownNotifier notifier = new ShutdownNotifier(this); The flag can not be changed once a shutdown is triggered.

Referencing some existing source code is no "guarantee".
The guarantee would be a JavaDoc specification for the ShutdownManager-API, which is missing:
https://sosy-lab.github.io/java-common-lib/api/org/sosy_lab/common/ShutdownManager.html#getNotifier()

A user can provide his own implementation of the shutdown-manager and change its behaviour.
I really would prefer to keep a local reference to this notifier.

There is no intention of a guarantee that getNotifier() always returns the same instance, but there is definitively the intention that this does not matter and that all notifiers handed out by a manager always return the shutdown state of the manager, and that shouldShutdown() will keep returning true forever after it has returned true once.

Since the split in separate manager and notifier classes this was not fully written down in the JavaDoc, but I improved this now: sosy-lab/java-common-lib@108faa6

@PhilippWendler i just noticed that there is/can be a delay in between the shutdown being requested and the children being informed. See the 2 tests here. Is this intentional?

I am not sure what exactly you are referring to. But if you have multi-threaded code, then you can of course never be sure when each of the threads is scheduled in relation to the others.

Yes, but i would have expected that the chain of signals in the shutdown notifiers/managers is built in such a way that they are all informed in a synchronized way.

What do you mean with "synchronized way"? "synchronized" is not some magic global property, one can only synchronize against specific things.

If you want help, you need to be more specific. What is the sequence of operations that you are observing and that is unexpected/unwanted?

I was merely curious ;D
We discussed this offline sufficiently. Thank you!

kfriedberger · 2025-06-01T13:39:33Z

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }


One could move this method higher up in the hierarchy and just provide it in the abstract super-class.

I removed it completely, as we didn't really need it.

kfriedberger · 2025-06-01T13:41:53Z

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -49,7 +49,7 @@ protected BoolectorAbstractProver(
    this.manager = manager;
    this.creator = creator;
    this.btor = btor;
-    terminationCallback = shutdownNotifier::shouldShutdown;
+    terminationCallback = proverShutdownManager.getNotifier()::shouldShutdown;


Just for comparison to above: Here, we keep the same notifier and reuse it for all callback-calls.

We build a new manager in every prover creation (see here) and then use this new managers notifier to request shutdowns. So we always use the one notifier bound to the one manager of the prover (that is a child of the contexts ShutdownNotifier)

This is now outdated due to the changes.

kfriedberger · 2025-06-01T13:47:05Z

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

+   */
+  private TerminationCallback getTerminationTest() {
+    return () -> {
+      proverShutdownManager.getNotifier().shutdownIfNecessary();


We could extract the reference to the notifier and just reuse.

Might look like this:

final ShutdownNotifier notifier = getShutdownManagerForProver().getNotifier() return () -> { notifier.shutdownIfNecessary(); return false; };

Done! Thanks for the hint.

kfriedberger · 2025-06-01T13:53:45Z

src/org/sosy_lab/java_smt/test/TimeoutTest.java

+      t.start();
+      assertThrows(InterruptedException.class, pe::isUnsat);
+    }
+  }


None of the tests checks whether the solver is usable after a shutdown.
None of the tests checks that, out of multiple parallel instances, if one is terminated, then all other provers remain running and deliver results.

Could you add such tests?

I was just writing some tests and noticed that we do not really define how a solver (context and prover) should behave after a context-wide shutdown is requested.
Should prover creation throw a exception if the context is already shut down?
What operations are still usable and guaranteed to be correct/safe after a shutdown in your current prover?

kfriedberger · 2025-06-01T13:58:12Z

This PR might provide a solution for a quite old issue: #100 :-)

… shut-down etc.) and add more shutdown checks in the abstract prover

kfriedberger · 2025-06-02T11:20:04Z

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -119,7 +123,8 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
      return false;
    } else if (resultValue == Result.UNSAT) {
      return true;
-    } else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) {
+    } else if (resultValue == Result.UNKNOWN
+        && proverShutdownManager.getNotifier().shouldShutdown()) {


Referencing some existing source code is no "guarantee".
The guarantee would be a JavaDoc specification for the ShutdownManager-API, which is missing:
https://sosy-lab.github.io/java-common-lib/api/org/sosy_lab/common/ShutdownManager.html#getNotifier()

A user can provide his own implementation of the shutdown-manager and change its behaviour.
I really would prefer to keep a local reference to this notifier.

kfriedberger · 2025-06-02T11:21:37Z

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

      result = smtEngine.checkSat();
    }
-    shutdownNotifier.shutdownIfNecessary();
+    proverShutdownManager.getNotifier().shutdownIfNecessary();


I would prefer to avoid calling getNotifier() more than once here.

I just forgot to push everything. Should be removed now. Sorry for the delay.

- test context interrupt with subsequent prover usage - test prover interrupt with subsequent feature usage (ignored because unfinished)

src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java

…(do we have this already elsewhere?)

…e() etc. so that interrupts and common prerequisites are uniformly handled

baierd · 2025-06-02T15:13:40Z

I cleaned up the default behavior of the prover API (isUnsat(), getModel(), getUnsatCore() etc.) so that they share the common prerequisites and no inconsistencies within the solver implementations exist.

I found 2 things i want to discuss:

The JavaDoc of unsatCoreOverAssumptions() states that: Returns an UNSAT core (if it exists, otherwise {@code Optional.empty()}), over the chosen assumptions. Does NOT require the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work. But we have and check for the option GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS. So i guess the JavaDoc should be updated?
the 2 public methods getSeqInterpolants0() and getTreeInterpolants0() are not named well in my opinion. I suggest better names like getSingletonSeqInterpolants)? (i am happy about better name suggestions ;D)

…ptions()

…r shutdown notifier + default implementation

…ronment

… to delegates

…ception

PhilippWendler · 2025-07-07T07:21:45Z

src/org/sosy_lab/java_smt/api/SolverContext.java

+   * @implNote If the SMT solver is able to handle satisfiability tests with assumptions please
+   *     consider implementing the {@link InterpolatingProverEnvironment} interface, and return an
+   *     Object of this type here.


I don't understand this comment. The return type of the method is InterpolatingProverEnvironment, one always needs to return such an instance. What does this have to do with "solving with assumptions"?

This is a comment for developers (e.g. students) so that they get info what to implement. We have this at several locations and for example helped me back in my bachelors thesis.

Sure, having @implNotes is good. But what does this one want to say? Isn't InterpolatingProverEnvironment always required, and what does implementing it have to do with "satisfiability tests with assumptions"?

No it is not always required. The default impl throws a UnsupportedOperationException.
It is meant to lead the developer to the conclusion that this needs to be implemented if you want to interpolate. Usually students (in my experience) notice once they run the tests that things are missing ;D

Ok, but then the comment should still refer to interpolation and not satisfiability tests with assumptions.

…h ShutdownNotifiers

…llegalArgumentException for msat_model_create_iterator()

…n as Throwable (due to Z3)

…tedException to it

… the Model

…nymore

… Philipp

…iterator into branch feature_prover_based_shutdown

…rruptedException for assumption removal and just throw it

…rruptedException and just throw it, including getUnsatCore()

…n in TimeoutTest.java

baierd · 2025-07-31T15:20:57Z

@kfriedberger @PhilippWendler i now merged #501 into this to get the Solver/InterruptedExceptions for the model and prover API. I also added them to getUnsatCore(). So now nearly every method in the prover throws both. This allows us to remove all that special handling for the exceptions (except iterator() ;D).

…rover checkInterpolationArguments()

PhilippWendler · 2025-07-31T15:28:52Z

I just realized that ca14eff was even more important than I thought before.

If the intention of checkShutdownState() was "the method must not be called with shutdown already being triggered before", then this is not even possible. The following sequence can always happen:

Caller checks that no shutdown is triggered and decides to call a method like getUnsatCore.
Other thread triggers shutdown, e.g., due to timeout.
checkShutdownState() is called and throws.

This means that no matter what an application does, if it uses the shutdown interface as it is intended, it would randomly crash with IllegalStateException, which would be a bug.

So the only way to handle shutdown requests properly can be to throw InterruptedException, as it is done now I guess?

But note that it is unnecessary to check for shutdown immediately when entering a method. Because of the asynchronicity no method can and needs to guarantee that it always notices a shutdown. The only place where one needs to check for shutdowns is in loops that execute for potentially long time.

…ion with shutdown notifiers

…ific one

baierd · 2025-07-31T17:10:25Z

I just realized that ca14eff was even more important than I thought before.

If the intention of checkShutdownState() was "the method must not be called with shutdown already being triggered before", then this is not even possible. The following sequence can always happen:
1. Caller checks that no shutdown is triggered and decides to call a method like `getUnsatCore`.

2. Other thread triggers shutdown, e.g., due to timeout.

3. `checkShutdownState()` is called and throws.
This means that no matter what an application does, if it uses the shutdown interface as it is intended, it would randomly crash with IllegalStateException, which would be a bug.

So the only way to handle shutdown requests properly can be to throw InterruptedException, as it is done now I guess?

But note that it is unnecessary to check for shutdown immediately when entering a method. Because of the asynchronicity no method can and needs to guarantee that it always notices a shutdown. The only place where one needs to check for shutdowns is in loops that execute for potentially long time.

Oh wow! Good catch! This means that all the API changes are actually fully justified.

…eeded

…ceptions as the new API changes do not need this anymore

Revert "Revert changes supposed to be on a feature branch"

b8ccbe0

This reverts commit 3a62853.

baierd requested review from kfriedberger and daniel-raffler May 30, 2025 19:01

baierd self-assigned this May 30, 2025

kfriedberger reviewed Jun 1, 2025

View reviewed changes

BaierD added 6 commits June 2, 2025 12:07

Reduce complexity of prover based shutdown getter

7422f4c

Reduce complexity of prover based shutdown getter even more

a43d183

Remove unnecessary comment in BitwuzlaTheoremProver

5af69e6

Allow and use direct access to prover specific ShutdownNotifier

2b81ac8

Add Int and BV test for context shutdown and prover reuse afterward

92f2f60

Add default implementation of isUnsat() to centralize checks (closed,…

b048f56

… shut-down etc.) and add more shutdown checks in the abstract prover

kfriedberger reviewed Jun 2, 2025

View reviewed changes

Add more timeout/shutdown tests:

e73b889

- test context interrupt with subsequent prover usage - test prover interrupt with subsequent feature usage (ignored because unfinished)

PhilippWendler reviewed Jun 2, 2025

View reviewed changes

src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java Outdated Show resolved Hide resolved

BaierD added 6 commits June 2, 2025 15:38

Add a model test that checks error when requesting a model for UNSAT …

ba6c2bc

…(do we have this already elsewhere?)

Remove unnecessary exceptions from test methods in TimeoutTest

28d5648

Format TimeoutTest

5de5971

Add default handling for basic prover API like isUnsat(), getUnsatCor…

0f8e757

…e() etc. so that interrupts and common prerequisites are uniformly handled

Remove unnecessary final modifiers in AbstractProver

1b6f52b

Add more uniform handling of prerequisites of interpolation API

77ab3d6

BaierD added 8 commits June 2, 2025 17:15

Add clarification JavaDoc for getShutdownManagerForProver()

223624c

Add clarification JavaDoc about needed options for unsatCoreOverAssum…

55f8e08

…ptions()

Add more internal information about shutdown re-use for Z3 and Bitwuzla

6613b21

Format JavaDoc

843b0ee

Add API for requesting new prover environments with a dedicated prove…

e6587bd

…r shutdown notifier + default implementation

Remove old getter for created shutdown manager in the BasicProverEnvi…

418bc8b

…ronment

Add new prover environments with a dedicated prover shutdown notifier…

c85042b

… to delegates

Add dedicated prover shutdown notifier to abstract provers

2fe5c2b

BaierD added 3 commits June 30, 2025 19:23

Make common Strings used in provers static

f16f77d

Re-add default impl of getModelAssignments()

1ab6955

Re-throw exception when clearing assumptions, and it's not another ex…

fc323b9

…ception

PhilippWendler reviewed Jul 7, 2025

View reviewed changes

BaierD added 17 commits July 21, 2025 17:25

Improve JavaDoc of constructor methods of new prover environments wit…

1b268a3

…h ShutdownNotifiers

Add warning for sneaky SolverExceptions in Model JavaDoc

c4a7a65

Throw sneaky SolverExceptions in Mathsat Model instead of confusing I…

b7da958

…llegalArgumentException for msat_model_create_iterator()

Add more sneaky throw warnings to API that may throw a SolverExceptio…

50094eb

…n as Throwable (due to Z3)

Remove sneaky throw of SolverException from Mathsat native call

89837d5

Remove sneaky throw of SolverException from Z3 model and add Interrup…

dbbdc31

…tedException to it

Add SolverException and InterruptedException to many calls related to…

b0e7b44

… the Model

Remove sneaky throws for Z3 specific code entirely

0ca8d4f

Add Solver- and InterruptedException to push() and addConstraint() API

cd51b02

Remove warnings about sneaky throws where they can't happen anymore

898832d

Format: remove warnings about sneaky throws where they can't happen a…

c900399

…nymore

Rename exception variable to fit naming schema

2166410

Improve warning for sneaky throws in model iterator() as suggested by…

64b21b3

… Philipp

Merge feature branch 481-mathsat5-returns-null-for-msat_model_create_…

cd3ef20

…iterator into branch feature_prover_based_shutdown

Remove special handling of interrupts for API that did not throw Inte…

477efd0

…rruptedException for assumption removal and just throw it

Remove special handling of interrupts for API that did not throw Inte…

ca14eff

…rruptedException and just throw it, including getUnsatCore()

Switch all expected exceptions after interrupt to InterruptedExceptio…

4b429db

…n in TimeoutTest.java

Remove toString() in lazy evaluation to be actually lazy in AbstractP…

d447902

…rover checkInterpolationArguments()

BaierD added 2 commits July 31, 2025 18:30

Move JavaDoc from throws to general info for prover environment creat…

22bc811

…ion with shutdown notifiers

Use dummy ShutdownNotifier instead of null if there is no prover spec…

a75ec8a

…ific one

baierd added this to the Release 6.0.0 milestone Jul 31, 2025

BaierD added 2 commits August 4, 2025 16:42

Remove null checks for prover based ShutdownNotifier when no longer n…

5f30d42

…eeded

Remove Z3 specific code for throwing checked exceptions as runtime ex…

b8c9a06

…ceptions as the new API changes do not need this anymore

Add Prover Based ShutdownManager #489

Are you sure you want to change the base?

Add Prover Based ShutdownManager #489

Uh oh!

Conversation

baierd commented May 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kfriedberger left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

baierd Jun 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kfriedberger commented Jun 1, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

baierd commented Jun 2, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

baierd commented May 30, 2025 •

edited

Loading

kfriedberger left a comment •

edited

Loading

baierd Jun 2, 2025 •

edited

Loading