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 https://github.com/goblint/analyzer/issues/1057 it might be useful to look into those.

I implemented some library functions https://github.com/goblint/analyzer/pull/1198/commits/18a1733dc41bbea8178bc7b481c4de48abe43970 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 https://github.com/goblint/analyzer/pull/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.