nidhugg (atomic operations support)

[karoliineh]

I stumbled upon this nidhugg repository when reading a PLDI article about Deagle. There are a bunch of benchmarks using atomic operations, so when one starts to implement goblint/analyzer#1057 it might be useful to look into those.

I implemented some library functions goblint/analyzer@18a1733 and ran Goblint on these benchmarks.

Results

Goblint failed on the benchmarks which included asserts as this is not implemented. For other benchmarks, it either found races or successfully ignored them due to _Atomic variables.

benchmark	race	assert
lastzero.c	no race
opt_lock.c	no race
parker_c11.c		x
parker.c		x
fib_bench.c		x
floating_read.c		x
lamport.c		x
lastwrite.c	no race
ainc.c	no race
binc.c	no race
casrot.c	race due to symbolic thread ID (array)
casw.c	race due to symbolic thread ID (array)
readers.c	no race
circular_buffer.c		x
reorder_c11_bad.c		x
reorder_c11_good.c	no race
alpha1.c	race due to symbolic thread ID (array)
alpha2.c	race due to symbolic thread ID (array)
bakery.c	race due to symbolic thread ID (array)	x
burns.c	race due to symbolic thread ID (array)	x
CO-2+2W.c	race due to symbolic thread ID (array)	x
CO-MP.c	race due to symbolic thread ID (array)
CO-R.c	race due to symbolic thread ID (array)
CO-S.c	race due to symbolic thread ID (array)
co1.c	race due to symbolic thread ID (array)
co4.c	race due to symbolic thread ID (array)
co10.c	race due to symbolic thread ID (array)
control_flow.c	no race
coRR2.c	race due to symbolic thread ID (array)
dijkstra.c	race due to symbolic thread ID (array)	x
exponential_bug.c	no race
fib_one_variable.c		x
filesystem.c	race due to symbolic thread ID (array) and success with all accs in main thread
myexample.c	race due to symbolic thread ID (array)
n_writers_a_reader	no race
n_writes_a_read_two_threads.c	race due to symbolic thread ID (array, only 2 indexes and threads, though) and one success, due to mhp
peterson.c		x
pgsql.c	race due to symbolic thread ID (array)	x
redundant_co.c	no race

Edit: ignoring _Atomic types in race analysis does work with array types after goblint/analyzer#1198. I reran the benchmarks and updated the results table accordingly. Most remaining races are now due to not having symbolic thread IDs for arrays.

[michael-schwarz]

Maybe we should add the library functions you already specified to Goblint already? I don't think there's any harm in having them...

[sim642]

Maybe we should add the library functions you already specified to Goblint already? I don't think there's any harm in having them...

The __atomic_fetch ones should also read their ptr argument, but otherwise yes, they could just be added directly on Goblint master.