Relational mutex-meet unsound on ConcurrencySafety-Main

[sim642]

During #1394 I implemented ghost witness generation for relational mutex-meet. The benchmarks revealed unsoundness which is also present on master (2fa4f55e682da3ad937e394fe20449eeef4c9634) in:

• [x] ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil (#1444)
• [x] ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil (#1444)
• [ ] pthread-driver-races/char_generic_nvram_read_nvram_write_nvram
• [x] weaver/popl20-more-buffer-mult.wvr (does not use locks but only __VERIFIER_atomic_*()) (#1441)
• [x] weaver/popl20-more-buffer-series.wvr (does not use locks but only __VERIFIER_atomic_*()) (#1441)

The unsoundness only reveals itself when activating the Apron analysis unconditionally.

For example

./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/weaver/popl20-more-buffer-mult.wvr.c --set ana.activated[+] apron

has 60/100 lines dead. Without unconditional apron, it has 1/104 lines dead. Oddly, if loop unrolling is disabled, things are also sound.

[michael-schwarz]

For pthread-driver-races/char_generic_nvram_read_nvram_write_nvram we get:

[Error][Analyzer][Unsound] both branches over condition '*ppos >= (loff_t )nvram_len' are dead (../../sv-comp/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i:6715:6-6715:24)
[Error][Analyzer][Unsound] both branches over condition '*ppos >= (loff_t )nvram_len' are dead (../../sv-comp/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i:6732:6-6732:24)
SV-COMP result: true

[michael-schwarz]

At first glance, it seems that for pthread-driver-races/char_generic_nvram_read_nvram_write_nvram our result is correct, as the parameter ppos points to whoop_loff_t for which a blob is allocated but never initialized. I'll try to do a detailed write-up tomorrow.

[michael-schwarz]

In pthread-driver-races/char_generic_nvram_read_nvram_write_nvram there are only three references to whoo_loff_t.

• A declaration: loff_t *whoop_loff_t;

• In main: whoop_loff_t = (loff_t *) malloc(sizeof(loff_t));

• Passed as last argument (*ppos) to write_nvram, read_nvram

• main starts two threads pthread_t_write_nvram and pthread_t_read_nvram that start with whoop_wrapper_write_nvram and whoop_wrapper_read_nvram respectively. These then call write_nvram and read_nvram respectively.

• read_nvram dereference the pointer ( ssize_t lppos = *ppos;)

Thus, this tasks seems to have UB. Interestingly, fixing this does not fix the UB issues. For this to work, one needs to remove the __VERIFIER_atomic_*.

[sim642]

This is with just mutex-meet, not the experimental mutex-meet-atomic, so there should be no special handling of SV-COMP atomics. The same behavior should be observable when replacing them with a single normal pthread mutex I think.

[michael-schwarz]

Hmm, the problem seems to indeed be with the handling of atomic. I extracted this from pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.

https://github.com/goblint/analyzer/blob/fa62bdd392ffbed5b32ae92df435a6826cb5ee04/tests/regression/29-svcomp/35-atomic.c#L1-L26

Everything after __VERIFIER_atomic_begin is reported as dead here. (The mutexes are only to demonstrate that they do not cause any issues and can be removed).

As I do not use __VERIFIER_atomic_* in the programs for my thesis, I need to focus on those benchmarks currently and cannot investigate the cause right now. But hopefully this already points in the right direction.

[michael-schwarz]

I extracted the problem in the issue_1140 branch.

[sim642]

Thanks for the minimized test case, it indeed highlights the problem. Turns out it's the same issue as https://github.com/goblint/analyzer/pull/1407#issuecomment-2037220588, but now with soundness consequences. I'll see if a quick fix to change the type would help.

[sim642]

The remaining task here was also mentioned in #1498, which should be fixed by #1492. Its initialization issue should be fixed in sv-benchmarks (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1551), but that is unrelated to our unsoundness here.