Can't use shutdownmanager more than once

[Zomono]

Hi, I'm very happy with this project and it saved me a lot of work. Thank you so much!

In my current project I need to do a lot of satisfiability checks. Because for some formulas the Z3 Prover runs infinitely long, I am using the ShutdownManager to stop the Z3 after a given timeout. But this works only for the first time. I can't use the Shutdownmanager a second time for the same context.

What I have done:

• I create one context like it is done in your example
• For every sat-check I create a new ProverEnvironment and use the ShutdownManager from a different thread if the Prover runs to long.

The problem is, that the ShutdownNotifier ignores additional calls to requestShutdown. I also tried to close the context and create a new on for each sat-check, but this results immediately to a native InterruptException and has a bad effect on the performance.

So what should I do to stop every sat-check (if needed)?

[kfriedberger]

Hi Zerlono, the ShutdownManager has an internal state and can only be used once, afterwards it will always terminate when used. Maybe you can use your own implementation of ShutdownManager wrapping an instance of a real ShutdownManager, which you can reset (or re-instantiate) after calling the shutdown method (and waiting for the solvers termination). Then the internal state would be reset to running and should only terminate when requestShutdown is called again later.

[PhilippWendler]

ShutdownManager is not resettable on purpose because it could not be guaranteed that libraries like the SMT solver leave everything in a clean state when being interrupted. This problem would not be solved by implementing an own resettable replacement.

I would expect, however, that separate contexts are not affected by previous contexts' shutdown managers, and if this happens it should be treated as a bug and be solved. Can you provide some code that reproduces this problem?

[Zomono]

The ShutdownManger has a private constructor anyway and can't be extended. Is a new context really needed for every call? This may has a performance impact due to the amount of sat-check calls done within my program.

Because I don't do any thing special compared to the given examples, one of the example is maybe enough to reproduce it. Here is the code used within my project:

package uniks.sct.solver.subsolver.quantifier;

import lombok.extern.slf4j.Slf4j;
import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.*;

import java.util.Collections;
import java.util.Set;
import java.util.concurrent.Executors;
import java.util.concurrent.ScheduledExecutorService;
import java.util.concurrent.ScheduledFuture;
import java.util.concurrent.TimeUnit;

@Slf4j
public class SMTSolver implements AutoCloseable {

    private SolverContext solverContext;
    private ShutdownManager shutdownManager;
    private int timeOutInMs;
    private final ScheduledExecutorService executor;

    public SMTSolver(int timeOutInMs) throws SolverException {
        this.timeOutInMs = timeOutInMs;
        executor = Executors.newScheduledThreadPool(1);
        createSolver();
    }

    private void createSolver() throws SolverException {
        try {
            shutdownManager = ShutdownManager.create();
            solverContext = SolverContextFactory.createSolverContext(
                Configuration.defaultConfiguration(),
                LogManager.createTestLogManager(),
                shutdownManager.getNotifier(),
                SolverContextFactory.Solvers.Z3
            );
        } catch (InvalidConfigurationException e) {
            close();
            throw new SolverException(e.getMessage(), e);
        }
    }

    /**
     * @param booleanFormula check satisfiability for this formula
     * @return true if <b>booleanFormula</b> is satisfiable false otherwise.
     */
    public boolean checkSat(BooleanFormula booleanFormula) throws SolverException {
        return checkSat(Collections.singleton(booleanFormula));
    }

    /**
     * @param booleanFormulas check satisfiability for this formulas
     * @return true if all <b>booleanFormulas</b> are satisfiable false otherwise.
     */
    public boolean checkSat(Set<BooleanFormula> booleanFormulas) throws SolverException {
        try (ProverEnvironment proverEnv = solverContext.newProverEnvironment()) {
            //noinspection ResultOfMethodCallIgnored
            booleanFormulas.forEach(proverEnv::addConstraint);
            // This future will cancel the z3 after timeOutInMs
            Runnable runnable = () -> shutdownManager.requestShutdown("Timeout");
            ScheduledFuture<?> timeoutFuture = executor.schedule(runnable, timeOutInMs, TimeUnit.MILLISECONDS);
            boolean isUnsat = proverEnv.isUnsat();
            cancelTimeoutFuture(timeoutFuture);
            return !isUnsat;
        } catch (Exception e) {
            throw new SolverException(e.getMessage(), e);
        }
    }

    private void cancelTimeoutFuture(ScheduledFuture<?> timeoutFuture) {
        try {
            timeoutFuture.cancel(false);
            timeoutFuture.get();
        } catch (Throwable ignore) {}
    }

    @Override
    public void close() {
        if (solverContext != null) {
            shutdownManager.requestShutdown("Closed");
            solverContext.close();
        }
    }

    public FormulaManager getFormulaManager() {
        return solverContext.getFormulaManager();
    }
}

[cheshire]

@PhilippWendler it's an interesting point on whether solver state is usable after an interrupt. I highly suspect Z3 is.

I think we should investigate it on a per-solver basis; if they are usable, then many interrupts should be allowed, and otherwise creating many contexts can not be helped.

Also there is definitely an associated documentation issue, it should be stated that ShutdownNotifier is usable only once.

[Zomono]

So, is there work in progress to allow multiple interrupt-calls? What else can I do to work around that problem? The point is that I must stop the Z3 prover various times in the context of my application. It is an application with a GUI and it calculates solutions for the user's problems by a bunch of Z3-calls. It is ok if the Z3 fails, but in order to continue the main algorithm the Z3 Prover must be stopped somehow.

Thanks in advanced

[cheshire]

I would take a look, but that would be only after the end of January.

For now, i think the easiest workaround is to create a separate context per query.

On Jan 15, 2017 12:46 PM, "Zerlono" notifications@github.com wrote:

So, is there work in progress to allow multiple interrupt-calls? What else can I do to work around that problem? The point is that I must stop the Z3 prover various times in the context of my application. It is an application with a GUI and it calculates solutions for the user's problems by a bunch of Z3-calls. It is ok if the Z3 fails, but in order to continue the main algorithm the Z3 Prover must be stopped somehow.

Thanks in advanced

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/sosy-lab/java-smt/issues/100#issuecomment-272690031, or mute the thread https://github.com/notifications/unsubscribe-auth/AAVTHxUKP9ICbOjarJjoygooEV6to1dLks5rSgccgaJpZM4LiGJG .

[cheshire]

If you don't mind using hacks, you can also take the approach Karlheinz has suggested, using reflection to subclass ShutdownManager and to force the behavior you prefer (I think Z3 does behave in the expected way).

[Zomono]

For now I have implemented a hack that allows to trigger the interrupt manually and it seems that the Z3 Prover can handle it. But for the future it would be nice to have this feature integrated in Java-SMT without reflexion ;). Thanks for your help.

If someone else needs this feature right now, here is my code:

package uniks.sct.solver.subsolver.quantifier;

import org.sosy_lab.common.ShutdownNotifier.ShutdownRequestListener;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.api.SolverContext;

import java.lang.reflect.Field;

public class SMTContextHacks {    

    public static void shutdownHack(SolverContext context, String reason) {
        if (context.getSolverName() != SolverContextFactory.Solvers.Z3) {
            throw new RuntimeException("This hack is intended for Z3-Contexts only!");
        }

        try {
            Class z3SolverContextClass = context.getClass().getClassLoader().loadClass("org.sosy_lab.java_smt.solvers.z3.Z3SolverContext");
            Field interruptListenerField = z3SolverContextClass.getDeclaredField("interruptListener");
            interruptListenerField.setAccessible(true);
            ShutdownRequestListener interruptListener = (ShutdownRequestListener) interruptListenerField.get(context);
            interruptListener.shutdownRequested(reason);
        } catch (NoSuchFieldException | IllegalAccessException | ClassNotFoundException e) {
            System.out.println("Hacking the Z3SmtContext failed!");
            e.printStackTrace();
        }
    }

}

If you have improvement suggestions feel free to leave me a comment.

[cheshire]

Interestingly enough, the issue occurs only with Z3, as a different polling mechanism is used by Mathsat5 and SMTInterpol (they periodically call a user-provided function, terminating on non-zero output, as opposed to relying on the interrupt function being called from a different thread).

And yes, all solvers seem to support multiple interrupts, I am not sure why would we assume that they wouldn't leave the context in a consistent state (otherwise they should be just killing the context).

[cheshire]

@PhilippWendler I'll see whether it's possible to resolve the issue by changing the way we interrupt Z3. If not, a large change to the whole ShutdownNotifier system might be required (maybe a separate subclass which supports multiple interrupts?..).

[PhilippWendler]

Why do you believe that all solvers support multiple interrupts? Do you have any sources for this claim? What do you mean by "kill the context"? What exactly would you expect a solver to do?

Nevertheless, the first issue that should be investigated is that according to https://github.com/sosy-lab/java-smt/issues/100#issue-200447575 an interrupt on one context affects other contexts as well. If true, this is a bug and needs to be fixed anyway, regardless of how we proceed.

Redesigning the API to allow multiple interrupts is a different issue. The main problem is not that this is more difficult technically (implementation issues can be solved), but this is more complex conceptually. Because interrupts are not only pushed via listeners but can also be polled, we cannot simply distribute atomic interrupt events, but we need to keep a mutable boolean state whether we are currently interrupting or not. Client code needs to manually reset this, we cannot determine automatically when it is safe to reset to normal state. This means the API opens up a whole new range of potential problems if a ShutdownManager is used concurrently. Another issue would be that code like if (shouldShutdown()) { getReason() } could now fail with an exception. Altogether, an API for allowing multiple interrupts is more complex in all kinds of ways and more difficult to use correctly. This is why the current API was designed as it is: using it correctly should be trivial, and using it incorrectly should be as hard as possible.

If you want to change that in order to support new use cases, one would need to think very carefully how to design the new API and which use cases to support and which not. I won't be able to spend time on this. However, changing the meaning of the existing API should not be done (it guarantees that shutdown requests are never reset). This also includes that new subclasses cannot be added, as they would break the contract as well. So a new independent class would have to be written, and possibly an adapter for compatibility with existing code.

[stahlbauer]

What is the status of this ticket? I would also love to see this feature! And it basically is possible and would work for most solvers! Why don't we expose a feature that many solvers provide? The solver designers have thought about the problems that might arise from such interrupts! In case an interrupt is not possible or not implemented we could throw some kind of UnsupportedOperationException.

[stahlbauer]

I had also designed several solutions for the problem. One would be to work with several instances of ShutdownNotifier and something like a ShutdownNotifierProvider that gets queried for each new prover environment. Nevertheless, the name ShutdownNotifier could be one reason for the problems we discuss here (shutting down the process or application); introduce a class InterruptProvider or a separate interface for interrupting solver calls? The code that makes use of the solver (environment) can the use a ShutdownNotifer to provide the interrupts.

[PhilippWendler]

@stahlbauer What you describe seems to be something different than what this issue is about, right? This issue is about having a resettable ShutdownManager, but as far as I understand the ShutdownNotifierProvider idea, you would want to have one ShutdownNotifier per ProverEnvironment. If yes, maybe open a separate issue in order to not confuse this. Interrupting individual prover environments could be done even more easily by simply passing ShutdownNotifier instances to newProverEnvironment() instead of createSolverContext(). However, unfortunately Z3 does not support separate interrupts for each prover environment, only for the whole context. It seems that MathSAT would support it, though. For SMTInterpol it could be done as well, because we support only a single environment at the same time anyway.