Performance problem for certain queries, part 2
There are certain cmdlines, where PJBDD is much slower than JavaBDD.
Example:
scripts/cpa.sh -noout -heap 10000M -stack 20M -bddAnalysis -32 -timelimit 900s -stats \ -setprop bdd.package=JAVA \ -spec test/programs/benchmarks/properties/unreach-call.prp \ test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1.cil-2.c
and
scripts/cpa.sh -noout -heap 10000M -stack 20M -bddAnalysis -32 -timelimit 900s -stats \ -setprop bdd.package=PJBDD -setprop bdd.pjbdd.threads=1 -setprop bdd.synchronizeLibraryAccess=false \ -spec test/programs/benchmarks/properties/unreach-call.prp \ test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1.cil-2.c
JavaBDD needs 15s and 4G of memory, PJBDD needs more than 900s and also 4G of memory (and then runs out of time).
The problem might be an entailment-check. There is a hot-spot at:
... at org.sosy_lab.pjbdd.creator.bdd.BDDCreator.entailsUnblocking(BDDCreator.java:185) at org.sosy_lab.pjbdd.creator.bdd.BDDCreator.entailsUnblocking(BDDCreator.java:185) at org.sosy_lab.pjbdd.creator.bdd.BDDCreator.entailsUnblocking(BDDCreator.java:185) at org.sosy_lab.pjbdd.creator.bdd.BDDCreator.entailsUnblocking(BDDCreator.java:185) at org.sosy_lab.pjbdd.creator.bdd.BDDCreator.entails(BDDCreator.java:161) at org.sosy_lab.cpachecker.util.predicates.bdd.PJBDDRegionManager.entails(PJBDDRegionManager.java:79) at org.sosy_lab.cpachecker.util.predicates.regions.NamedRegionManager.entails(NamedRegionManager.java:206) at org.sosy_lab.cpachecker.cpa.bdd.BDDState.isLessOrEqual(BDDState.java:58) at org.sosy_lab.cpachecker.cpa.bdd.BDDState.isLessOrEqual(BDDState.java:38) ...
This problem results in an overall negative performance for benchmarks.
Edited by Karlheinz Friedberger