linux-arch.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [PATCH] tools/memory-model: Add atomic_andnot() with its variants
@ 2024-05-14  9:46 Puranjay Mohan
  2024-05-14 11:11 ` Andrea Parri
  0 siblings, 1 reply; 3+ messages in thread
From: Puranjay Mohan @ 2024-05-14  9:46 UTC (permalink / raw)
  To: Alan Stern, Andrea Parri, Will Deacon, Peter Zijlstra,
	Boqun Feng, Nicholas Piggin, David Howells, Jade Alglave,
	Luc Maranget, Paul E. McKenney, Akira Yokosawa, Daniel Lustig,
	Joel Fernandes, linux-kernel, linux-arch
  Cc: puranjay12

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 <puranjay@kernel.org>
---

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/20240508143400.36256-1-puranjay@kernel.org/

---
 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


^ permalink raw reply related	[flat|nested] 3+ messages in thread

* Re: [PATCH] tools/memory-model: Add atomic_andnot() with its variants
  2024-05-14  9:46 [PATCH] tools/memory-model: Add atomic_andnot() with its variants Puranjay Mohan
@ 2024-05-14 11:11 ` Andrea Parri
  2024-05-14 19:02   ` Paul E. McKenney
  0 siblings, 1 reply; 3+ messages in thread
From: Andrea Parri @ 2024-05-14 11:11 UTC (permalink / raw)
  To: Puranjay Mohan
  Cc: Alan Stern, Will Deacon, Peter Zijlstra, Boqun Feng,
	Nicholas Piggin, David Howells, Jade Alglave, Luc Maranget,
	Paul E. McKenney, Akira Yokosawa, Daniel Lustig, Joel Fernandes,
	linux-kernel, linux-arch, puranjay12

> 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 <puranjay@kernel.org>

Acked-by: Andrea Parri <parri.andrea@gmail.com>

  Andrea

^ permalink raw reply	[flat|nested] 3+ messages in thread

* Re: [PATCH] tools/memory-model: Add atomic_andnot() with its variants
  2024-05-14 11:11 ` Andrea Parri
@ 2024-05-14 19:02   ` Paul E. McKenney
  0 siblings, 0 replies; 3+ messages in thread
From: Paul E. McKenney @ 2024-05-14 19:02 UTC (permalink / raw)
  To: Andrea Parri
  Cc: Puranjay Mohan, Alan Stern, Will Deacon, Peter Zijlstra,
	Boqun Feng, Nicholas Piggin, David Howells, Jade Alglave,
	Luc Maranget, Akira Yokosawa, Daniel Lustig, Joel Fernandes,
	linux-kernel, linux-arch, puranjay12

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 <puranjay@kernel.org>
> 
> Acked-by: Andrea Parri <parri.andrea@gmail.com>

Queued and pushed, thank you both!

Again, I will hold off pushing this until herd7 releases a version
supporting this.

							Thanx, Paul

^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2024-05-14 19:02 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2024-05-14  9:46 [PATCH] tools/memory-model: Add atomic_andnot() with its variants Puranjay Mohan
2024-05-14 11:11 ` Andrea Parri
2024-05-14 19:02   ` Paul E. McKenney

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).