Skip to content

Use atomic load / store instead of __VERIFIER_atomic for weaver benchmarks

Frank Schüssele requested to merge weaver-atomic into main

Many of the concurrency tasks contain many atomic block that just consist of one single statement to avoid data races, e.g.

__VERIFIER_atomic_begin();
x = 0;
__VERIFIER_atomic_end();

However, in C11 there is a library to access variables atomically, without the need for SV-COMP specific functions. In contrast to !1554 (merged) (where atomic types are used), this PR replaces such accesses with atomic_load and atomic_store for some of the weaver benchmarks. Since these benchmarks are already preprocessed, the atomic builtins of GCC are used (mostly __atomic_load_n and atomic_store_n). For example the code above, was just replaced by __atomic_store_n(&x, 0, 5) (the 5 indicates sequential consistency).

Note: In general, this replacement is not equivalent. An atomic block can contain multiple accesses (even in a single statement). For example

__VERIFIER_atomic_begin();
x = y;
__VERIFIER_atomic_end();

is not equivalent to __atomic_store_n(&x, __atomic_load_n(&y, 5), 5), as other threads might interfere between the load and the store (which is not possible using atomic blocks). However, for these (rather simple) benchmarks, such replacements were made anyway, as it should not influence the behaviour of the programs.

Merge request reports