GitLab

Currently it is not possible to use PredicateCPA with ThreadingCPA to verify multi-threaded tasks. This issue is just a documentation about the things to do. This issue is not related to ParallelBAM (conceptually we cannot combine BAM with ThreadingCPA).

PredicateCPA has some internal dependencies and assumptions that fail with multi-threaded tasks. The following is an initial (incomplete) list:

• one program location per abstract state. ThreadingCPA has more locations per abstract state.
• one program location per predicate in the precision. Might even work, if the abstraction uses predicates if any location matches.
• determine most efficient block size. SBE should work, LBE might be a problem due to heavy branching and merging. The block operator does not consider multiple locations per abstract state. Best solution so far: use existing block operator and compute abstractions whenever any of the available locations triggers a block-end.
• at most two outgoing branches in counterexamples. This seems to only print a warning, maybe not a problem.

We need to take a look at them, and then check whether and how we can weaken them.

As an initial step, BMC could be extended to support concurrent programs. This could be used to enable counterexample checking for our current analyses of concurrent programs.