How to solve the "UNKNOWN" result when CPAchecker checking multiple threads programs?

[Kaiwen Shi]

Hi CPAchecker developers,

I'm experimenting with CPAchecker to check the unreachability in multiple threads programs.

In the program "https://github.com/sosy-lab/sv-benchmarks/blob/master/c/pthread-complex/bounded_buffer.i", I found that if the program uses loops to create threads, CPAchecker returns "UNKNOWN" and goes error like:

        Error: Several exceptions occured during the analysis:

        -> line 1668: Unsupported feature (pthread_create): pthread_create(&((consumers[i]).pid), (void *)0, &consumer_routine, (void *)(&(consumers[i]))); (line was originally pthread_create(&consumers[i].pid, ((void *)0), consumer_routine, (void*)&consumers[i]);)

        -> line 1662: Unsupported feature (pthread_create): pthread_create(&((producers[i]).pid), (void *)0, &producer_routine, (void *)(&(producers[i]))); (line was originally pthread_create(&producers[i].pid, ((void *)0), producer_routine, (void*)&producers[i]);) (ParallelAlgorithm.handleFutureResults, SEVERE)

Then in the modified program "bounded_buffer_modified_1.i", I created threads respectively, not using loops. However, CPAchecker still returns "UNKNOWN" and goes error like:

        

        Error: line 1661: Unsupported feature (pthread_create): pthread_create(&((producers[0]).pid), (void *)0, &producer_routine, (void *)(&(producers[0]))); (line was originally pthread_create(&producers[0].pid, ((void *)0), producer_routine, (void*)&producers[0]);) (ParallelAlgorithm.handleFutureResults, SEVERE)

Then I considered if I change thread arrays to normal variables, things will get different. So I implemented it in the program "bounded_buffer_modified_2.i". Unfortunately, CPAchecker still returns "UNKNOWN" and goes error like:\

        Error: line 1661: Unsupported feature (pthread_create): pthread_create(&(producer1.pid), (void *)0, &producer_routine, (void *)(&producer1)); (line was originally pthread_create(&producer1.pid, ((void *)0), producer_routine, (void*)&producer1);) (ParallelAlgorithm.handleFutureResults, SEVERE)

How can I deal with these problems?

Best regards,

Kaiwen

[Karlheinz Friedberger]

Hi Kaiwen,

thank you for trying concurrency analysis with CPAchecker.
We know that this analysis is not yet as mature as other analyses,
thus there are some limitations in our framework.

# Short answer:
For this program, CPAchecker is currently unable to provide a valid verification process.

# Detailed explanation:
Your chosen configuration internally applies a BDD-based concurrency analysis to check reachability.
Having a loop in the program should not cause any problem. We support any reasonable control flow.
However in your case, the limitation is that we can only handle plain direct thread assignments,
i.e., no arrays or struct accesses for thread identifiers.
In your program you are using "consumer1.pid", which is an unsupported field access of a struct.
After solving this issue, there will be an additional limitation from the used BDD-based domain,
i.e., missing support for modeling structs and arrays, such as "bounded_buf_t".
I do currently not know whether CPAchecker just aborts the analysis (runs out of resources, maybe
StackOverflow in the BDD) or provides an imprecise result (false alarm) after several minutes.

Best,
Karlheinz



Am 09.07.20 um 03:44 schrieb Kaiwen Shi:

>
> Hi CPAchecker developers,
>
> I'm experimenting with CPAchecker to check the unreachability in multiple threads programs.
>

> In the program *"https://github.com/sosy-lab/sv-benchmarks/blob/master/c/pthread-complex/bounded_buffer.i"*, I found that if the program uses loops to create threads, CPAchecker returns "UNKNOWN" and goes error like:
>
> /        Error: Several exceptions occured during the analysis:/
> /        -> line 1668: Unsupported feature (pthread_create): pthread_create(&((consumers[i]).pid), (void *)0, &consumer_routine, (void *)(&(consumers[i]))); (line was originally pthread_create(&consumers[i].pid, ((void *)0), consumer_routine, (void*)&consumers[i]);)/
> /        -> line 1662: Unsupported feature (pthread_create): pthread_create(&((producers[i]).pid), (void *)0, &producer_routine, (void *)(&(producers[i]))); (line was originally pthread_create(&producers[i].pid, ((void *)0), producer_routine, (void*)&producers[i]);) (ParallelAlgorithm.handleFutureResults, SEVERE)/
> /
> /
> Then in the modified program *"bounded_buffer_modified_1.i",* I created threads respectively, not using loops. However, CPAchecker still returns "UNKNOWN" and goes error like:
>         
>        /Error: line 1661: Unsupported feature (pthread_create): pthread_create(&((producers[0]).pid), (void *)0, &producer_routine, (void *)(&(producers[0]))); (line was originally pthread_create(&producers[0].pid, ((void *)0), producer_routine, (void*)&producers[0]);) (ParallelAlgorithm.handleFutureResults, SEVERE)/
>
> Then I considered if I change thread arrays to normal variables, things will get different. So I implemented it in the program *"bounded_buffer_modified_2.i"*. Unfortunately, CPAchecker still returns "UNKNOWN" and goes error like:\
>
> /        Error: line 1661: Unsupported feature (pthread_create): pthread_create(&(producer1.pid), (void *)0, &producer_routine, (void *)(&producer1)); (line was originally pthread_create(&producer1.pid, ((void *)0), producer_routine, (void*)&producer1);) (ParallelAlgorithm.handleFutureResults, SEVERE)/

>
> How can I deal with these problems?
>
> Best regards,
>
> Kaiwen
>

> --
> 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/cce6642f-7bab-462b-a14a-ab7e8ff1d3d8o%40googlegroups.com <https://groups.google.com/d/msgid/cpachecker-users/cce6642f-7bab-462b-a14a-ab7e8ff1d3d8o%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Karlheinz Friedberger
Software and Computational Systems Lab
LMU Munich, Germany

[mzy...@gmail.com]

Hi Karlheinz，

Thanks for your timely response.

I'm Kaiwen's colleague.

According to your explanation, we modified our command-line parameter from "'-svcomp20" to "../config/bmc-incremental.properties", where the latter (i.e., bmc) does not use BDD in its analysis process.

Unfortunately, we also get the same ERROR report:

Error: line 1661: Unsupported feature (pthread_create): pthread_create(&(producer1.pid), (void *)0, &producer_routine, (void *)(&producer1)); (line was originally pthread_create(&producer1.pid, ((void *)0), producer_routine, (void*)&producer1);) (CallstackTransferRelation.getAbstractSuccessorsForEdge, SEVERE)

Therefore, apart from using BDD, is there any other reason why CPAchecker is unable to provide a valid verification process on the program.

Best,

Zhaoyi

[Karlheinz Friedberger]

Hi Zhaoyi,

currently there is no SMT-based analysis (like BMC) in CPAchecker
that can handle concurrent programs.
We are working on that feature, but it is not yet usable.

CPAchecker's limitation for concurrent programs are as follows:

- 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.
In the future, we plan additional support for SMT-based analyses like BMC or predicate analysis.

- 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.

Best,
Karlheinz


Am 09.07.20 um 09:14 schrieb mzy...@gmail.com:

>
> Hi Karlheinz，
>
> Thanks for your timely response.
> I'm Kaiwen's colleague.
>
> According to your explanation, we modified our command-line parameter from "'-svcomp20" to "../config/bmc-incremental.properties", where the latter (i.e., bmc) does not use BDD in its analysis process.
>
> Unfortunately, we also get the same ERROR report:

> /Error: line 1661: Unsupported feature (pthread_create): pthread_create(&(producer1.pid), (void *)0, &producer_routine, (void *)(&producer1)); (line was originally pthread_create(&producer1.pid, ((void *)0), producer_routine, (void*)&producer1);) (CallstackTransferRelation.getAbstractSuccessorsForEdge, SEVERE)
> /

> To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/2df2a768-5c0d-476e-b6c4-7392a17cdc01n%40googlegroups.com <https://groups.google.com/d/msgid/cpachecker-users/2df2a768-5c0d-476e-b6c4-7392a17cdc01n%40googlegroups.com?utm_medium=email&utm_source=footer>.