339 stackoverflowerror using mathsat5 #345
Conversation
…le upon bug #310 for CVC5.
…en MathSat returns a "user-requested termination" error.
… a test for bug #339 in MathSAT.
…gered when MathSat returns a "user-requested termination" error." This reverts commit 4003c34.
…eceral failed tests in TimoutTest.java
…eneds when formulas are used outside of their context.
…support one thread per ProverEnvironment anyway.
…sues has been solved.
src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java
Outdated
Show resolved
Hide resolved
src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java
Outdated
Show resolved
Hide resolved
…re the test may fail if calculating interpolants took too long.
…when trying to create a new solver context. See #345 (comment)
… termination test directly in isUnsat and isUnsatWithAssumptions. This was suggested in #345 (comment)
|
Hello Philipp, |
|
I guess Daniel will do a full review, I just stumbled upon this because I was interested in this issue (good find btw.!) and left comments where I noticed something. I guess you could get rid of the |
This commit unifies the level of abstraction for registering a shutdown-callback and removing the callback afterwards.
And fix a typo.
There was a problem hiding this comment.
The bugfix is a great outcome, well done! The tests are well written, too.
The steps for debugging and narrowing the problem (cf. commit history of this PR) are very interesting.
👍
@daniel-raffler or @baierd : Who has the honor and would like to merge this?
|
Thanks for your help, Karlheinz! I've talked to Daniel and he will merge the branch in the next few days. |
…d to create the ProverEnvironment on the thread. The other version also fails, but for different reasons and this somehow got mixed up earlier.
…when trying to create a new solver context. See #345 (comment)
… termination test directly in isUnsat and isUnsatWithAssumptions. This was suggested in #345 (comment)
Hello everyone,
this is my fix for bug #339. The issue was in the implementation of the termination call back for MathSAT in our JNI bindings. In order to check whether the shutdown manager has been triggered we need to provide MathSAT with a way of calling back our Java code. For this the current Jenv pointer is stored when a new prover environment instance is created. Unfortunately this pointer is only valid for the current thread, and if isUnsat is later called from any other thread we get a StackOverflowError. The solution is to only install the callback right before the native call to MathSAT in isUnsat. This way we can be sure to be on the right thread when the JEnv is saved. Once MathSAT returns we can then remove the callback again.
In addition to the bug fix this pull request also includes a new test class "SolverThreadLocalityTest" that is meant to find similar errors in other solvers.