concurrency analysis with CPAchecker
lingqiu huang
Dear CPAChecker developers,
I have a question regarding concurrency analysis with CPAchecker.
here is test sample code, modified from [1] Figure 1.
When I use the config/bddAnalysis-concurrency.properties or config/valueAnalysis-concurrency.properties, I receive an ERROR report. 
Fortunately, when I use config/bmc-concurrency.properties or config/predicateAnalysis-concurrency.properties, I get a TRUE result.
My question is, how do I choose between these four concurrency properties? What are the differences among them?
In the discussion at https://groups.google.com/g/cpachecker-users/c/7m19sJrJaeo/m/fC4d9nYNAgAJ , it was mentioned that there are limitations for concurrent programs:
- domain-specific limitations:
Only BDD-based or explicit-value-based analyses are usable for analysing concurrent programs.
Structs, arrays, pointers can not be analysed precisely with these domains.
- threading-specific limitations:
The program should not use complex assignments for thread identifiers.
In other words, CPAchecker supports the analyis of concurrent programs
that are pointer-free and use only simple thread assignments.
In the newest version 2.2, are there any improvements or updates regarding limitations for concurrent programs? Does it now support pointer analysis with multi-threads?
[1] https://www.sosy-lab.org/research/pub/2016-MEMICS.A_Light-Weight_Approach_for_Verifying_Multi-Threaded_Programs_with_CPAchecker.pdf
Best regards,
Ling
Karlheinz Friedberger
thanks for using CPAchecker.
The expressiveness of the concurrency analysis in CPAchecker depends on various factors,
such as domain, exploration order, and partial order reduction.
The support for analyzing and encoding pointers, structs, and arrays in multi-threaded programs
is supported up to a certain point, mostly depending on the same factors.
Let's go into details:
- There is currently no support for thread-related management with pointers,
such as tracking thread-ids or mutex-locks assigned via pointers.
In such cases, the analysis will terminate with an error-message.
For other pointer-operations, such as local/global variables as in the given program,
the analysis result and performance depends on the used domain.
- The BDD-based domain does not encode pointer operations, but ignores such assignments.
This makes the analysis sound, but imprecise.
The BDD-analysis was optimized for performance on simple integer-based programs.
It can encode large state-spaces with reasonable memory consumption.
For the given program, CPAchecker will report the property violation.
- The value-domain has limited support for pointer-handling.
In complex cases, it might also over-approximate the program and ignore assignments.
This makes the analysis sound, but imprecise.
The value-analysis was also optimized for performance on simple integer-based programs.
It should be able to detect property-violations quite fast.
For the given program, it might be possible to configure CPAchecker with value-analysis
such that the given program is solved as expected (if not yet working out-of-the-box already).
- The SMT-based analysis (BMC or predicate analysis) uses a SMT-solver as backend.
While BDD- and value-domains are initially added and described in a publication [1],
the support for solving concurrent programs with a SMT-based domain was added later [2].
(I currently do not know in which version of CPAchecker we added this feature.)
The encoding is based on the default predicate-analysis (used for sequential programs without threads),
where CPAchecker can analyze a wide range of pointer operations on larger scale.
Thus, the encoding supports most pointer operations in program variables, including structs and (partially) arrays.
However, if pointer-operations are present, our heuristics for partial order reduction can not be applied.
Without an efficient reduction strategy for the multi-threaded state-space,
SMT-based program encoding is quite expensive and formulas get large fast.
I hope that answers some of your questions.
Best
Karlheinz
[1] https://www.sosy-lab.org/research/pub/2016-MEMICS.A_Light-Weight_Approach_for_Verifying_Multi-Threaded_Programs_with_CPAchecker.pdf
[2] https://www.sosy-lab.org/research/bsc/2020.Kolesnykov.SMT-Based_Model_Checking_of_Concurrent_Programs.pdf
Am 10.08.23 um 10:17 schrieb lingqiu huang:
>
> I have a question regarding concurrency analysis with CPAchecker. here is test sample code, modified from [1] Figure 1.
> When I use the config/bddAnalysis-concurrency.properties or config/valueAnalysis-concurrency.properties, I receive an ERROR report.
> Fortunately, when I use config/bmc-concurrency.properties or config/predicateAnalysis-concurrency.properties, I get a TRUE result.
>
> My question is, how do I choose between these four concurrency properties? What are the differences among them?
>
> In the discussion at https://groups.google.com/g/cpachecker-users/c/7m19sJrJaeo/m/fC4d9nYNAgAJ , it was mentioned that there are limitations for concurrent programs:
>
> - domain-specific limitations:
> Only BDD-based or explicit-value-based analyses are usable for analysing concurrent programs.
> - threading-specific limitations:
> The program should not use complex assignments for thread identifiers.
>
> In other words, CPAchecker supports the analyis of concurrent programs
> that are pointer-free and use only simple thread assignments.
>
> In the newest version 2.2, are there any improvements or updates regarding limitations for concurrent programs? Does it now support pointer analysis with multi-threads?
>
> [1] https://www.sosy-lab.org/research/pub/2016-MEMICS.A_Light-Weight_Approach_for_Verifying_Multi-Threaded_Programs_with_CPAchecker.pdf
>
> Best regards,
> Ling
>
> You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com <mailto:cpachecker-use...@googlegroups.com>.
> To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/272cbf56-5402-4239-a53b-54389a2e6c3cn%40googlegroups.com <https://groups.google.com/d/msgid/cpachecker-users/272cbf56-5402-4239-a53b-54389a2e6c3cn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
Karlheinz Friedberger