Re: [RFC 2/3] tools/memory-model: Add a litmus test for atomic_set()

From: Andrea Parri
Date: Fri Feb 14 2020 - 03:12:44 EST


> @@ -0,0 +1,24 @@
> +C Atomic-set-observable-to-RMW
> +
> +(*
> + * Result: Never
> + *
> + * Test of the result of atomic_set() must be observable to atomic RMWs.
> + *)
> +
> +{
> + atomic_t v = ATOMIC_INIT(1);
> +}
> +
> +P0(atomic_t *v)
> +{
> + (void)atomic_add_unless(v,1,0);

We blacklisted this primitive some time ago, cf. section "LIMITATIONS",
entry (6b) in tools/memory-model/README; the discussion was here:

https://lkml.kernel.org/r/20180829211053.20531-3-paulmck@xxxxxxxxxxxxxxxxxx

but unfortunately I can't remember other details at the moment: maybe
it is just a matter of or the proper time to update that section.

Thanks,
Andrea