herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
219 stars 56 forks source link

herd: Linux: atomic_and, atomic_or, atomic_xor instructions. #849

Closed puranjaymohan closed 4 months ago

puranjaymohan commented 4 months ago

Add the remaining atomic instructions used by the linux kernel.

Tested by applying following diff to the linux-kernel.def in the kernel:

diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index 88a39601f525..ae07e9acdff1 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -65,6 +65,9 @@ atomic_set_release(X,V) { smp_store_release(X,V); }

atomic_add(V,X) { atomic_op(X,+,V); } atomic_sub(V,X) { atomic_op(X,-,V); } +atomic_and(V,X) { atomic_op(X,&,V); } +atomic_or(V,X) { atomic_op(X,|,V); } +atomic_xor(V,X) { atomic_op(X,^,V); } atomic_inc(X) { atomic_op(X,+,1); } atomic_dec(X) { __atomic_op(X,-,1); }

and created basic litmus tests of the kind:

C atomics

{ atomic_t t = ATOMIC_INIT(15); }

P0(atomic_t t) { r0 = t; atomic_xor(0, t); r1 = *t; }

exists (0:r0=15 /\ 0:r1=15)

to individually test each operation.

maranget commented 4 months ago

Thanks for your contribution @puranjaymohan.