StackOverflowError using MathSAT5

[baierd]

When using Mathsat with the following commandline on CPAchecker we end up with an StackOverflowError whos source is not entirely clear. We should investigate this.

scripts/cpa.sh -svcomp24 -stats -spec test/programs/benchmarks/properties/unreach-call.prp test/programs/benchmarks/bitvector/gcd_2.c

Exception in thread "main" java.lang.StackOverflowError
    at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve(Native Method)
    at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat(Mathsat5NativeApi.java:156)
    at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat(Mathsat5AbstractProver.java:103)
    at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.isUnsat(BasicProverEnvironmentView.java:61)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.checkInfeasabilityOfTrace(InterpolationManager.java:1097)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.buildCounterexampleTrace(InterpolationManager.java:973)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace0(InterpolationManager.java:446)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTrace$0(InterpolationManager.java:328)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:337)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace(InterpolationManager.java:327)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.interpolate(InterpolationManager.java:401)
    at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.interpolate(InterpolationManager.java:380)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.reachFixedPointByInterpolation(IMCAlgorithm.java:835)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.reachFixedPoint(IMCAlgorithm.java:763)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.interpolationModelChecking(IMCAlgorithm.java:588)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.run(IMCAlgorithm.java:530)
    at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:377)
    at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$3(ParallelAlgorithm.java:322)
    at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:131)
    at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:76)
    at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:82)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
    at java.base/java.lang.Thread.run(Thread.java:833)

[MartinSpiessl]

Information missing in the description: this assumes the svcomp24-parallel-portfolio-approach branch of CPAchecker is used, e.g. I was able to reproduce with revision 45052 (if I add -timelimit 900s, otherwise CPAchecker complains).

I guess the only thing we can do is create a MWE for mathsat and send this to the mathsat team.

I tried to run the component that seems to cause this (config/components/svcomp24--singleLoop-IMC.properties )alone
and that works fine. If I take out all components from the parallel portfolio except the IMC one then the bug is still triggerable. Looks like this might be due to the fact that the analysis runs in another thread?

[lembergerth]

Looks like this might be due to the fact that the analysis runs in another thread?

This is the case.

Currently, we generate the MathSAT solver instance in thread main, but then the IMC Algorithm accesses this solver instance from another thread (from a thread pool).

This leads to the StackOverflowError.
After changing the code in CPAchecker to generate the solver instance in the same thread that the IMC algorithm runs in, the exception is gone.

@baierd is it already known that you should not use a solver instance from a different thread than it was generated in? Or should this work?
If you need more information for a minimal working example, ping me.

[baierd]

@lembergerth this should work for all solvers except for Bitwuzla (which is not merged yet for this very reason). We even have tests for this.

Can you go into detail as to what the sequence of usage is that leads to this problem?

Don't get me wrong. I think that we should avoid doing this in general (speaking about CPAchecker here), as it makes debugging harder and it is easy to use the wrong solver instance by accident.

[baierd]

I just discussed with @daniel-raffler that we will add some tests to find problems regarding usage of JavaSMT/solver components on different threads.

[lembergerth]

Nice, thank you! :-)

[daniel-raffler]

I've added some tests to try and track down the bug, but so far no luck. I did stumble on bug #310 for CVC5, but was not able to reproduce this bug in my tests.

Some observations:

• The stacktrace is just too small for a StackOverflowError. This exception seems to be caught by a wrapper somewhere and is then printed to the screen, but I was unable to find its exact origin. If there's a problem in the MathSAT native code it should probably result in a segfault instead. And I couldn't find anything in the JNI bindings that would throw this exception directly.
• To fix the bug it is enough to move just the line final Algorithm algorithm = coreComponents.createAlgorithm(cpa, cfa, specification); into the closure. Everything else can be done in the main thread before the closure is created.
• If I increase the timeout in line 165 the program will just keep on spinning with no exception being thrown. Are we waiting for a crashed thread here? And why is the exception then suppressed?
• I did a diff of the (stderr) output of the original and the fixed version. However, I didn't notice anything remarkable. You can find the file here.

I suspect that this bug requires solver instances to be created recursively across several threads, and I'll add more tests later.

[baierd]

I did some investigating: the problem is not that isUnsat() throws a StackOverflowError (i catched it and it still occured). The issue lies deeper and is most likely caused by some memory corruption of the solver due to usage of the same context/formulas/prover in multiple threads (as the error does not occur when run in only 1 thread). There is nothing we can do on the side of JavaSMT.