Closed baierd closed 10 months ago
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?
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.
@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.
I just discussed with @daniel-raffler that we will add some tests to find problems regarding usage of JavaSMT/solver components on different threads.
Nice, thank you! :-)
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:
I suspect that this bug requires solver instances to be created recursively across several threads, and I'll add more tests later.
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.
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