Open sim642 opened 1 year ago
There's now progress in sv-benchmarks to replace some __VERIFIER_atomic
s with C11/GCC atomics:
I haven't checked how much it affects our results, but we might have to also adapt a bit to not lose our edge for superficial reasons.
There are multiple families of atomic operations:
__sync
builtins: https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html.There are three aspects in which to improve precision:
_Atomic
, but not the__sync
builtins used by various benchmarks. There should probably still be access events for them, but with an additional atomicity flag to exclude them from racing.