Pull-855[1] added the support of atomic_andnot() to the herd tool. Use
this to add the implementation in the LKMM. All of the ordering variants
are also added.
Here is a small litmus-test that uses this operation:
C andnot
{
atomic_t u = ATOMIC_INIT(7);
}
P0(atomic_t *u)
{
r0 = atomic_fetch_andnot(3, u);
r1 = READ_ONCE(*u);
}
exists (0:r0=7 /\ 0:r1=4)
Test andnot Allowed
States 1
0:r0=7; 0:r1=4;
Ok
Witnesses
Positive: 1 Negative: 0
Condition exists (0:r0=7 /\ 0:r1=4)
Observation andnot Always 1 0
Time andnot 0.00
Hash=78f011a0b5a0c65fa1cf106fcd62c845
[1] https://github.com/herd/herdtools7/pull/855
Signed-off-by: Puranjay Mohan <[email protected]>
---
This commit is based on the commit[1] that is adding `&`, `|`, and `^`.
Both of these patches should go together when the next version of herd7 is
released. I will update the "REQUIREMENTS" section when the new version is
released.
Later on, I will add some example litmus tests to showcase the usage of
these new operations.
[1] https://lore.kernel.org/all/[email protected]/
---
tools/memory-model/linux-kernel.def | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index d1f11930ec51..a12b96c547b7 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -70,6 +70,7 @@ 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); }
+atomic_andnot(V,X) { __atomic_op(X,&~,V); }
atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
@@ -138,3 +139,8 @@ atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0
atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0
atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0
atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0
+
+atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
+atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
+atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
+atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
--
2.40.1
> C andnot
>
> {
> atomic_t u = ATOMIC_INIT(7);
> }
>
> P0(atomic_t *u)
> {
>
> r0 = atomic_fetch_andnot(3, u);
> r1 = READ_ONCE(*u);
> }
>
> exists (0:r0=7 /\ 0:r1=4)
Fair enough for the changelog. If/when submitting proper tests, please
check their format using klitmus7 (besides herd7); say,
$ mkdir mymodule
$ klitmus7 -o mymodule <.litmus file>
$ cd mymodule ; make
$ sudo sh run.sh
Documentation/litmus-tests/ provides some examples litmus tests.
> Signed-off-by: Puranjay Mohan <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Andrea
On Tue, May 14, 2024 at 01:11:22PM +0200, Andrea Parri wrote:
> > C andnot
> >
> > {
> > atomic_t u = ATOMIC_INIT(7);
> > }
> >
> > P0(atomic_t *u)
> > {
> >
> > r0 = atomic_fetch_andnot(3, u);
> > r1 = READ_ONCE(*u);
> > }
> >
> > exists (0:r0=7 /\ 0:r1=4)
>
> Fair enough for the changelog. If/when submitting proper tests, please
> check their format using klitmus7 (besides herd7); say,
>
> $ mkdir mymodule
> $ klitmus7 -o mymodule <.litmus file>
> $ cd mymodule ; make
> $ sudo sh run.sh
>
> Documentation/litmus-tests/ provides some examples litmus tests.
>
>
> > Signed-off-by: Puranjay Mohan <[email protected]>
>
> Acked-by: Andrea Parri <[email protected]>
Queued and pushed, thank you both!
Again, I will hold off pushing this until herd7 releases a version
supporting this.
Thanx, Paul