[RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Boqun Feng]

A recent discussion raises up the requirement for having test cases for
atomic APIs:

	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/

, and since we already have a way to generate a test module from a
litmus test with klitmus[1]. It makes sense that we add more litmus
tests for atomic APIs into memory-model.

So I begin to do this and the plan is to add the litmus tests we already
use in atomic_t.txt, ones from Paul's litmus collection[2], and any
other valuable litmus test we come up while adding the previous two
kinds of tests.

This patchset finishes the first part (adding atomic_t.txt litmus
tests). I also improve the atomic_t.txt to make it consistent with the
litmus tests.

One thing to note is patch #2 requires a modification to herd and I just
made a PR to Luc's repo:

	https://github.com/herd/herdtools7/pull/28

, so if this patchset looks good to everyone and someone plans to take
it (and I assume is Paul), please wait until that PR is settled. And
probably we need to bump the required herd version because of it.

Comments and suggesions are welcome!

Regards,
Boqun


[1]: http://diy.inria.fr/doc/litmus.html#klitmus
[2]: https://github.com/paulmckrcu/litmus/tree/master/manual/atomic

*** BLURB HERE ***

Boqun Feng (3):
  Documentation/locking/atomic: Fix atomic-set litmus test
  tools/memory-model: Add a litmus test for atomic_set()
  tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

 Documentation/atomic_t.txt                    | 14 ++++-----
 ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
 .../Atomic-set-observable-to-RMW.litmus       | 24 +++++++++++++++
 tools/memory-model/litmus-tests/README        |  8 +++++
 4 files changed, 68 insertions(+), 7 deletions(-)
 create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
 create mode 100644 tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus

-- 
2.25.0

[RFC 1/3] Documentation/locking/atomic: Fix atomic-set litmus test

[Boqun Feng]

Currently the litmus test "atomic-set" in atomic_t.txt has a few things
to be improved:

1)	The CPU/Processor numbers "P1,P2" are not only inconsistent with
	the rest of the document, which uses "CPU0" and "CPU1", but also
	unacceptable by the herd tool, which requires processors start
	at "P0".

2)	The initialization block uses a "atomic_set()", which is OK, but
	it's better to use ATOMIC_INIT() to make clear this is an
	initialization.

3)	The return value of atomic_add_unless() is discarded
	inexplicitly, which is OK for C language, but it will be helpful
	to the herd tool if we use a void cast to make the discard
	explicit.

Therefore fix these and this is the preparation for adding the litmus
test into memory-model litmus-tests directory so that people can
understand better about our requirements of atomic APIs and klitmus tool
can be used to generate tests.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
 Documentation/atomic_t.txt | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index 0ab747e0d5ac..ceb85ada378e 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -91,15 +91,15 @@ ops. That is:
   C atomic-set
 
   {
-    atomic_set(v, 1);
+    atomic_t v = ATOMIC_INIT(1);
   }
 
-  P1(atomic_t *v)
+  P0(atomic_t *v)
   {
-    atomic_add_unless(v, 1, 0);
+    (void)atomic_add_unless(v, 1, 0);
   }
 
-  P2(atomic_t *v)
+  P1(atomic_t *v)
   {
     atomic_set(v, 0);
   }
-- 
2.25.0

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

[Boqun Feng]

We already use a litmus test in atomic_t.txt to describe the behavior of
an atomic_set() with the an atomic RMW, so add it into the litmus-tests
directory to make it easily accessible for anyone who cares about the
semantics of our atomic APIs.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
 .../Atomic-set-observable-to-RMW.litmus       | 24 +++++++++++++++++++
 tools/memory-model/litmus-tests/README        |  3 +++
 2 files changed, 27 insertions(+)
 create mode 100644 tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus

diff --git a/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus b/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
new file mode 100644
index 000000000000..4326f56f2c1a
--- /dev/null
+++ b/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
@@ -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);
+}
+
+P1(atomic_t *v)
+{
+	atomic_set(v, 0);
+}
+
+exists
+(v=2)
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 681f9067fa9e..81eeacebd160 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -2,6 +2,9 @@
 LITMUS TESTS
 ============
 
+Atomic-set-observable-to-RMW.litmus
+	Test of the result of atomic_set() must be observable to atomic RMWs.
+
 CoRR+poonceonce+Once.litmus
 	Test of read-read coherence, that is, whether or not two
 	successive reads from the same variable are ordered.
-- 
2.25.0

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

[Andrea Parri]

> @@ -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@linux.vnet.ibm.com

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

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

[Boqun Feng]

On Fri, Feb 14, 2020 at 09:12:13AM +0100, Andrea Parri wrote:
> > @@ -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@linux.vnet.ibm.com
> 

And in an email replying to that email, you just tried and seemed
atomic_add_unless() works ;-)

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

I spend a few time looking into the changes in herd, the dependency
problem seems to be as follow:

For atomic_add_unless(ptr, a, u), the return value (true or false)
depends on both *ptr and u, this is different than other atomic RMW,
whose return value only depends on *ptr. Considering the following
litmus test:

	C atomic_add_unless-dependency

	{
		int y = 1;
	}

	P0(int *x, int *y, int *z)
	{
		int r0;
		int r1;
		int r2;

		r0 = READ_ONCE(*x);
		if (atomic_add_unless(y, 2, r0))
			WRITE_ONCE(*z, 42);
		else
			WRITE_ONCE(*z, 1);
	}

	P1(int *x, int *y, int *z)
	{
		int r0;

		r0 = smp_load_acquire(z);

		WRITE_ONCE(*x, 1);
	}

	exists
	(1:r0 = 1 /\ 0:r0 = 1)

, the exist-clause will never trigger, however if we replace
"atomic_add_unless(y, 2, r0)" with "atomic_add_unless(y, 2, 1)", the
write on *z and the read from *x on CPU 0 are not ordered, so we could
observe the exist-clause triggered.

I just tried with the latest herd, and herd can work out this
dependency. So I think we are good now and can change the limitation
section in the document. But I will wait for Luc's input for this. Luc,
did I get this correct? Is there any other limitation on
atomic_add_unless() now?

Regards,
Boqun

> Thanks,
>   Andrea

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

[Boqun Feng]

Luc,

Could you have a look at the problem Andrea and I discuss here? It seems
that you have done a few things in herd for atomic_add_unless() in
particular, and based on the experiments of Andrea and me, seems
atomic_add_unless() works correctly. So can you confirm that herd now
can handle atomic_add_unless() or there is still something missing?

Thanks!

Regards,
Boqun

On Fri, Feb 14, 2020 at 06:40:03PM +0800, Boqun Feng wrote:
> On Fri, Feb 14, 2020 at 09:12:13AM +0100, Andrea Parri wrote:
> > > @@ -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@linux.vnet.ibm.com
> > 
> 
> And in an email replying to that email, you just tried and seemed
> atomic_add_unless() works ;-)
> 
> > 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.
> > 
> 
> I spend a few time looking into the changes in herd, the dependency
> problem seems to be as follow:
> 
> For atomic_add_unless(ptr, a, u), the return value (true or false)
> depends on both *ptr and u, this is different than other atomic RMW,
> whose return value only depends on *ptr. Considering the following
> litmus test:
> 
> 	C atomic_add_unless-dependency
> 
> 	{
> 		int y = 1;
> 	}
> 
> 	P0(int *x, int *y, int *z)
> 	{
> 		int r0;
> 		int r1;
> 		int r2;
> 
> 		r0 = READ_ONCE(*x);
> 		if (atomic_add_unless(y, 2, r0))
> 			WRITE_ONCE(*z, 42);
> 		else
> 			WRITE_ONCE(*z, 1);
> 	}
> 
> 	P1(int *x, int *y, int *z)
> 	{
> 		int r0;
> 
> 		r0 = smp_load_acquire(z);
> 
> 		WRITE_ONCE(*x, 1);
> 	}
> 
> 	exists
> 	(1:r0 = 1 /\ 0:r0 = 1)
> 
> , the exist-clause will never trigger, however if we replace
> "atomic_add_unless(y, 2, r0)" with "atomic_add_unless(y, 2, 1)", the
> write on *z and the read from *x on CPU 0 are not ordered, so we could
> observe the exist-clause triggered.
> 
> I just tried with the latest herd, and herd can work out this
> dependency. So I think we are good now and can change the limitation
> section in the document. But I will wait for Luc's input for this. Luc,
> did I get this correct? Is there any other limitation on
> atomic_add_unless() now?
> 
> Regards,
> Boqun
> 
> > Thanks,
> >   Andrea

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

[Luc Maranget]

Hi,

As far as I can remember I have implemented atomic_add_unless in herd7.

As to your test, I have first run a slightly modified version of your test
as a kernel module (using klitmus7).

C atomic_add_unless-dependency
{
        atomic_t y = ATOMIC_INIT(1);
}
  P0(int *x, atomic_t *y, int *z)
{
        int r0;
        r0 = READ_ONCE(*x);
        if (atomic_add_unless((atomic_t *)y, 2, r0))
                WRITE_ONCE(*z, 42);
        else
                WRITE_ONCE(*z, 1);
}
  P1(int *x, int *z)
{
        int r0;
        r0 = smp_load_acquire(z);
        WRITE_ONCE(*x, 1);
}
locations [y]
exists
(1:r0 = 1 /\ 0:r0 = 1)


The test is also accepted by herd7, here producing teh same final values
as actual run on a raspberry PI4B.

--Luc

> Luc,
> 
> Could you have a look at the problem Andrea and I discuss here? It seems
> that you have done a few things in herd for atomic_add_unless() in
> particular, and based on the experiments of Andrea and me, seems
> atomic_add_unless() works correctly. So can you confirm that herd now
> can handle atomic_add_unless() or there is still something missing?
> 
> Thanks!
> 
> Regards,
> Boqun
> 
> On Fri, Feb 14, 2020 at 06:40:03PM +0800, Boqun Feng wrote:
> > On Fri, Feb 14, 2020 at 09:12:13AM +0100, Andrea Parri wrote:
> > > > @@ -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@linux.vnet.ibm.com
> > > 
> > 
> > And in an email replying to that email, you just tried and seemed
> > atomic_add_unless() works ;-)
> > 
> > > 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.
> > > 
> > 
> > I spend a few time looking into the changes in herd, the dependency
> > problem seems to be as follow:
> > 
> > For atomic_add_unless(ptr, a, u), the return value (true or false)
> > depends on both *ptr and u, this is different than other atomic RMW,
> > whose return value only depends on *ptr. Considering the following
> > litmus test:
> > 
> > 	C atomic_add_unless-dependency
> > 
> > 	{
> > 		int y = 1;
> > 	}
> > 
> > 	P0(int *x, int *y, int *z)
> > 	{
> > 		int r0;
> > 		int r1;
> > 		int r2;
> > 
> > 		r0 = READ_ONCE(*x);
> > 		if (atomic_add_unless(y, 2, r0))
> > 			WRITE_ONCE(*z, 42);
> > 		else
> > 			WRITE_ONCE(*z, 1);
> > 	}
> > 
> > 	P1(int *x, int *y, int *z)
> > 	{
> > 		int r0;
> > 
> > 		r0 = smp_load_acquire(z);
> > 
> > 		WRITE_ONCE(*x, 1);
> > 	}
> > 
> > 	exists
> > 	(1:r0 = 1 /\ 0:r0 = 1)
> > 
> > , the exist-clause will never trigger, however if we replace
> > "atomic_add_unless(y, 2, r0)" with "atomic_add_unless(y, 2, 1)", the
> > write on *z and the read from *x on CPU 0 are not ordered, so we could
> > observe the exist-clause triggered.
> > 
> > I just tried with the latest herd, and herd can work out this
> > dependency. So I think we are good now and can change the limitation
> > section in the document. But I will wait for Luc's input for this. Luc,
> > did I get this correct? Is there any other limitation on
> > atomic_add_unless() now?
> > 
> > Regards,
> > Boqun
> > 
> > > Thanks,
> > >   Andrea

More on reader-writer locks

[Alan Stern]

On Tue, 25 Feb 2020, Luc Maranget wrote:

> Hi,
> 
> As far as I can remember I have implemented atomic_add_unless in herd7.

Luc, have you considered whether we can use atomic_add_unless and
cmpxchg to implement reader-writer locks in the LKMM?  I don't think we
can handle them the same way we handle ordinary locks now.

Let's say that a lock variable holds 0 if it is unlocked, -1 if it is 
write-locked, and a positive value if it is read-locked (the value is 
the number of read locks currently in effect).  Then operations like 
write_lock, write_trylock, and so on could all be modeled using 
variants of atomic_add_unless, atomic_dec, and cmpxchg.

But will that work if the reads-from relation is computed by the cat 
code in lock.cat?  I suspect it won't.

How would you approach this problem?

Alan

Re: More on reader-writer locks

[Luc Maranget]

Hi all,

As far as I understand there is a contradiction between having a "platonic"
implementation of locks (à la lock.cat) and a concrete one (for ordinary locks
lock -> load acquire, unlock -> store release, + loop [difficult for herd]
or filter clause).

So if reader/writer locks are catified in a platonic way, we cannot
use various atomic primitives. Instead, we give them an abstract semantics
based upon some axiomatisation of their semantics, using cat means.
Such an axionatisation  does not seem straightforward because,
by constrast with locks, there is an integer count
hiddden, and not a simple boolean as for ordinary locks

Some idea would be first to partition reader crtical sections,
and then for each such partition, order elements of the partition and
writer critical section. For one such choice there are still many possible
rf relations...

--Luc

rf relation 
> On Tue, 25 Feb 2020, Luc Maranget wrote:
> 
> > Hi,
> > 
> > As far as I can remember I have implemented atomic_add_unless in herd7.
> 
> Luc, have you considered whether we can use atomic_add_unless and
> cmpxchg to implement reader-writer locks in the LKMM?  I don't think we
> can handle them the same way we handle ordinary locks now.
> 
> Let's say that a lock variable holds 0 if it is unlocked, -1 if it is 
> write-locked, and a positive value if it is read-locked (the value is 
> the number of read locks currently in effect).  Then operations like 
> write_lock, write_trylock, and so on could all be modeled using 
> variants of atomic_add_unless, atomic_dec, and cmpxchg.
> 
> But will that work if the reads-from relation is computed by the cat 
> code in lock.cat?  I suspect it won't.
> 
> How would you approach this problem?
> 
> Alan

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

[Boqun Feng]

On Tue, Feb 25, 2020 at 02:01:02PM +0100, Luc Maranget wrote:
> Hi,
> 
> As far as I can remember I have implemented atomic_add_unless in herd7.
> 
> As to your test, I have first run a slightly modified version of your test
> as a kernel module (using klitmus7).
> 
> C atomic_add_unless-dependency
> {
>         atomic_t y = ATOMIC_INIT(1);
> }
>   P0(int *x, atomic_t *y, int *z)
> {
>         int r0;
>         r0 = READ_ONCE(*x);
>         if (atomic_add_unless((atomic_t *)y, 2, r0))
>                 WRITE_ONCE(*z, 42);
>         else
>                 WRITE_ONCE(*z, 1);
> }
>   P1(int *x, int *z)
> {
>         int r0;
>         r0 = smp_load_acquire(z);
>         WRITE_ONCE(*x, 1);
> }
> locations [y]
> exists
> (1:r0 = 1 /\ 0:r0 = 1)
> 
> 
> The test is also accepted by herd7, here producing teh same final values
> as actual run on a raspberry PI4B.
> 

Thanks, so I'm planning to make the following change to README file in
memory-model

I will add a separate patch in my v3 patchset of atomic-tests.

Regards,
Boqun

----->8
diff --git a/tools/memory-model/README b/tools/memory-model/README
index fc07b52f2028..d974a96ad273 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -207,11 +207,15 @@ The Linux-kernel memory model (LKMM) has the following limitations:
 		case as a store release.
 
 	b.	The "unless" RMW operations are not currently modeled:
-		atomic_long_add_unless(), atomic_add_unless(),
-		atomic_inc_unless_negative(), and
-		atomic_dec_unless_positive().  These can be emulated
+		atomic_long_add_unless(), atomic_inc_unless_negative(),
+		and atomic_dec_unless_positive().  These can be emulated
 		in litmus tests, for example, by using atomic_cmpxchg().
 
+		One exception of this limitation is atomic_add_unless(),
+		which is provide directly by herd7 (so no corresponding
+		definition in linux-kernel.def). atomic_add_unless() is
+		modeled by herd7 therefore it can be used in litmus tests.
+
 	c.	The call_rcu() function is not modeled.  It can be
 		emulated in litmus tests by adding another process that
 		invokes synchronize_rcu() and the body of the callback

> --Luc
> 
> > Luc,
> > 
> > Could you have a look at the problem Andrea and I discuss here? It seems
> > that you have done a few things in herd for atomic_add_unless() in
> > particular, and based on the experiments of Andrea and me, seems
> > atomic_add_unless() works correctly. So can you confirm that herd now
> > can handle atomic_add_unless() or there is still something missing?
> > 
> > Thanks!
> > 
> > Regards,
> > Boqun
> > 
> > On Fri, Feb 14, 2020 at 06:40:03PM +0800, Boqun Feng wrote:
> > > On Fri, Feb 14, 2020 at 09:12:13AM +0100, Andrea Parri wrote:
> > > > > @@ -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@linux.vnet.ibm.com
> > > > 
> > > 
> > > And in an email replying to that email, you just tried and seemed
> > > atomic_add_unless() works ;-)
> > > 
> > > > 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.
> > > > 
> > > 
> > > I spend a few time looking into the changes in herd, the dependency
> > > problem seems to be as follow:
> > > 
> > > For atomic_add_unless(ptr, a, u), the return value (true or false)
> > > depends on both *ptr and u, this is different than other atomic RMW,
> > > whose return value only depends on *ptr. Considering the following
> > > litmus test:
> > > 
> > > 	C atomic_add_unless-dependency
> > > 
> > > 	{
> > > 		int y = 1;
> > > 	}
> > > 
> > > 	P0(int *x, int *y, int *z)
> > > 	{
> > > 		int r0;
> > > 		int r1;
> > > 		int r2;
> > > 
> > > 		r0 = READ_ONCE(*x);
> > > 		if (atomic_add_unless(y, 2, r0))
> > > 			WRITE_ONCE(*z, 42);
> > > 		else
> > > 			WRITE_ONCE(*z, 1);
> > > 	}
> > > 
> > > 	P1(int *x, int *y, int *z)
> > > 	{
> > > 		int r0;
> > > 
> > > 		r0 = smp_load_acquire(z);
> > > 
> > > 		WRITE_ONCE(*x, 1);
> > > 	}
> > > 
> > > 	exists
> > > 	(1:r0 = 1 /\ 0:r0 = 1)
> > > 
> > > , the exist-clause will never trigger, however if we replace
> > > "atomic_add_unless(y, 2, r0)" with "atomic_add_unless(y, 2, 1)", the
> > > write on *z and the read from *x on CPU 0 are not ordered, so we could
> > > observe the exist-clause triggered.
> > > 
> > > I just tried with the latest herd, and herd can work out this
> > > dependency. So I think we are good now and can change the limitation
> > > section in the document. But I will wait for Luc's input for this. Luc,
> > > did I get this correct? Is there any other limitation on
> > > atomic_add_unless() now?
> > > 
> > > Regards,
> > > Boqun
> > > 
> > > > Thanks,
> > > >   Andrea

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

[Alan Stern]

On Fri, 14 Feb 2020, Boqun Feng wrote:

> We already use a litmus test in atomic_t.txt to describe the behavior of
> an atomic_set() with the an atomic RMW, so add it into the litmus-tests
> directory to make it easily accessible for anyone who cares about the
> semantics of our atomic APIs.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  .../Atomic-set-observable-to-RMW.litmus       | 24 +++++++++++++++++++
>  tools/memory-model/litmus-tests/README        |  3 +++
>  2 files changed, 27 insertions(+)
>  create mode 100644 tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus

I don't like that name, or the corresponding sentence in atomic_t.txt:

	A subtle detail of atomic_set{}() is that it should be
	observable to the RMW ops.

"Observable" doesn't get the point across -- the point being that the
atomic RMW ops have to be _atomic_ with respect to all atomic store
operations, including atomic_set.

Suggestion: Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus, with 
corresponding changes to the comment in the litmus test and the entry 
in README.

Alan

> diff --git a/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus b/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
> new file mode 100644
> index 000000000000..4326f56f2c1a
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
> @@ -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);
> +}
> +
> +P1(atomic_t *v)
> +{
> +	atomic_set(v, 0);
> +}
> +
> +exists
> +(v=2)
> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 681f9067fa9e..81eeacebd160 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -2,6 +2,9 @@
>  LITMUS TESTS
>  ============
>  
> +Atomic-set-observable-to-RMW.litmus
> +	Test of the result of atomic_set() must be observable to atomic RMWs.
> +
>  CoRR+poonceonce+Once.litmus
>  	Test of read-read coherence, that is, whether or not two
>  	successive reads from the same variable are ordered.
> 

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

[Boqun Feng]

On Fri, Feb 14, 2020 at 10:47:48AM -0500, Alan Stern wrote:
> On Fri, 14 Feb 2020, Boqun Feng wrote:
> 
> > We already use a litmus test in atomic_t.txt to describe the behavior of
> > an atomic_set() with the an atomic RMW, so add it into the litmus-tests
> > directory to make it easily accessible for anyone who cares about the
> > semantics of our atomic APIs.
> > 
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > ---
> >  .../Atomic-set-observable-to-RMW.litmus       | 24 +++++++++++++++++++
> >  tools/memory-model/litmus-tests/README        |  3 +++
> >  2 files changed, 27 insertions(+)
> >  create mode 100644 tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
> 
> I don't like that name, or the corresponding sentence in atomic_t.txt:
> 
> 	A subtle detail of atomic_set{}() is that it should be
> 	observable to the RMW ops.
> 
> "Observable" doesn't get the point across -- the point being that the
> atomic RMW ops have to be _atomic_ with respect to all atomic store
> operations, including atomic_set.
> 
> Suggestion: Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus, with 
> corresponding changes to the comment in the litmus test and the entry 
> in README.
> 

I agree, and thanks for the suggestion! And I change the sentence in
atomic_t.txt with:

	A note for the implementation of atomic_set{}() is that it
	cannot break the atomicity of the RMW ops.

, since I think that part of the doc is more about the suggestion to
anyone who want to implement the atomic_set(). Peter, is that OK to you?

Regards,
Boqun

> Alan
> 
> > diff --git a/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus b/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
> > new file mode 100644
> > index 000000000000..4326f56f2c1a
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
> > @@ -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);
> > +}
> > +
> > +P1(atomic_t *v)
> > +{
> > +	atomic_set(v, 0);
> > +}
> > +
> > +exists
> > +(v=2)
> > diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> > index 681f9067fa9e..81eeacebd160 100644
> > --- a/tools/memory-model/litmus-tests/README
> > +++ b/tools/memory-model/litmus-tests/README
> > @@ -2,6 +2,9 @@
> >  LITMUS TESTS
> >  ============
> >  
> > +Atomic-set-observable-to-RMW.litmus
> > +	Test of the result of atomic_set() must be observable to atomic RMWs.
> > +
> >  CoRR+poonceonce+Once.litmus
> >  	Test of read-read coherence, that is, whether or not two
> >  	successive reads from the same variable are ordered.
> > 
> 

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

[Peter Zijlstra]

On Sat, Feb 15, 2020 at 07:52:15AM +0800, Boqun Feng wrote:
> I agree, and thanks for the suggestion! And I change the sentence in
> atomic_t.txt with:
> 
> 	A note for the implementation of atomic_set{}() is that it
> 	cannot break the atomicity of the RMW ops.
> 
> , since I think that part of the doc is more about the suggestion to
> anyone who want to implement the atomic_set(). Peter, is that OK to you?

Sure.

[RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

[Boqun Feng]

We already use a litmus test in atomic_t.txt to describe atomic RMW +
smp_mb__after_atomic() is "strong acquire" (both the read and the write
part is ordered). So make it a litmus test in memory-model litmus-tests
directory, so that people can access the litmus easily.

Additionally, change the processor numbers "P1, P2" to "P0, P1" in
atomic_t.txt for the consistency with the processor numbers in the
litmus test, which herd can handle.

Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
 Documentation/atomic_t.txt                    |  6 ++--
 ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
 tools/memory-model/litmus-tests/README        |  5 ++++
 3 files changed, 37 insertions(+), 3 deletions(-)
 create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index ceb85ada378e..e3ad4e4cd9ed 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -238,14 +238,14 @@ strictly stronger than ACQUIRE. As illustrated:
   {
   }
 
-  P1(int *x, atomic_t *y)
+  P0(int *x, atomic_t *y)
   {
     r0 = READ_ONCE(*x);
     smp_rmb();
     r1 = atomic_read(y);
   }
 
-  P2(int *x, atomic_t *y)
+  P1(int *x, atomic_t *y)
   {
     atomic_inc(y);
     smp_mb__after_atomic();
@@ -260,7 +260,7 @@ This should not happen; but a hypothetical atomic_inc_acquire() --
 because it would not order the W part of the RMW against the following
 WRITE_ONCE.  Thus:
 
-  P1			P2
+  P0			P1
 
 			t = LL.acq *y (0)
 			t++;
diff --git a/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
new file mode 100644
index 000000000000..e7216cf9d92a
--- /dev/null
+++ b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
@@ -0,0 +1,29 @@
+C Atomic-RMW+mb__after_atomic-is-strong-acquire
+
+(*
+ * Result: Never
+ *
+ * Test of an atomic RMW followed by a smp_mb__after_atomic() is
+ * "strong-acquire": both the read and write part of the RMW is ordered before
+ * the subsequential memory accesses.
+ *)
+
+{
+}
+
+P0(int *x, atomic_t *y)
+{
+	r0 = READ_ONCE(*x);
+	smp_rmb();
+	r1 = atomic_read(y);
+}
+
+P1(int *x, atomic_t *y)
+{
+	atomic_inc(y);
+	smp_mb__after_atomic();
+	WRITE_ONCE(*x, 1);
+}
+
+exists
+(r0=1 /\ r1=0)
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 81eeacebd160..774e10058c72 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -2,6 +2,11 @@
 LITMUS TESTS
 ============
 
+Atomic-RMW+mb__after_atomic-is-strong-acquire
+	Test of an atomic RMW followed by a smp_mb__after_atomic() is
+	"strong-acquire": both the read and write part of the RMW is ordered
+	before the subsequential memory accesses.
+
 Atomic-set-observable-to-RMW.litmus
 	Test of the result of atomic_set() must be observable to atomic RMWs.
 
-- 
2.25.0

Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

[Boqun Feng]

On Fri, Feb 14, 2020 at 12:01:32PM +0800, Boqun Feng wrote:
> We already use a litmus test in atomic_t.txt to describe atomic RMW +
> smp_mb__after_atomic() is "strong acquire" (both the read and the write
> part is ordered). So make it a litmus test in memory-model litmus-tests
> directory, so that people can access the litmus easily.
> 
> Additionally, change the processor numbers "P1, P2" to "P0, P1" in
> atomic_t.txt for the consistency with the processor numbers in the
> litmus test, which herd can handle.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  Documentation/atomic_t.txt                    |  6 ++--
>  ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
>  tools/memory-model/litmus-tests/README        |  5 ++++
>  3 files changed, 37 insertions(+), 3 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> 
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index ceb85ada378e..e3ad4e4cd9ed 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -238,14 +238,14 @@ strictly stronger than ACQUIRE. As illustrated:
>    {
>    }
>  
> -  P1(int *x, atomic_t *y)
> +  P0(int *x, atomic_t *y)
>    {
>      r0 = READ_ONCE(*x);
>      smp_rmb();
>      r1 = atomic_read(y);
>    }
>  
> -  P2(int *x, atomic_t *y)
> +  P1(int *x, atomic_t *y)
>    {
>      atomic_inc(y);
>      smp_mb__after_atomic();
> @@ -260,7 +260,7 @@ This should not happen; but a hypothetical atomic_inc_acquire() --
>  because it would not order the W part of the RMW against the following
>  WRITE_ONCE.  Thus:
>  
> -  P1			P2
> +  P0			P1
>  
>  			t = LL.acq *y (0)
>  			t++;
> diff --git a/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> new file mode 100644
> index 000000000000..e7216cf9d92a
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> @@ -0,0 +1,29 @@
> +C Atomic-RMW+mb__after_atomic-is-strong-acquire
> +
> +(*
> + * Result: Never
> + *
> + * Test of an atomic RMW followed by a smp_mb__after_atomic() is
> + * "strong-acquire": both the read and write part of the RMW is ordered before
> + * the subsequential memory accesses.
> + *)
> +
> +{
> +}
> +
> +P0(int *x, atomic_t *y)
> +{
> +	r0 = READ_ONCE(*x);
> +	smp_rmb();
> +	r1 = atomic_read(y);
> +}
> +
> +P1(int *x, atomic_t *y)
> +{
> +	atomic_inc(y);
> +	smp_mb__after_atomic();
> +	WRITE_ONCE(*x, 1);
> +}
> +
> +exists
> +(r0=1 /\ r1=0)

Hmm.. this should be "(0:r0=1 /\ 0:r1=0)", I will fix this in next
verison.

Regards,
Boqun

> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 81eeacebd160..774e10058c72 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -2,6 +2,11 @@
>  LITMUS TESTS
>  ============
>  
> +Atomic-RMW+mb__after_atomic-is-strong-acquire
> +	Test of an atomic RMW followed by a smp_mb__after_atomic() is
> +	"strong-acquire": both the read and write part of the RMW is ordered
> +	before the subsequential memory accesses.
> +
>  Atomic-set-observable-to-RMW.litmus
>  	Test of the result of atomic_set() must be observable to atomic RMWs.
>  
> -- 
> 2.25.0
> 

Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

[Andrea Parri]

> > @@ -0,0 +1,29 @@
> > +C Atomic-RMW+mb__after_atomic-is-strong-acquire
> > +
> > +(*
> > + * Result: Never
> > + *
> > + * Test of an atomic RMW followed by a smp_mb__after_atomic() is
> > + * "strong-acquire": both the read and write part of the RMW is ordered before
> > + * the subsequential memory accesses.
> > + *)
> > +
> > +{
> > +}
> > +
> > +P0(int *x, atomic_t *y)
> > +{
> > +	r0 = READ_ONCE(*x);
> > +	smp_rmb();
> > +	r1 = atomic_read(y);

IIRC, klitmus7 needs a declaration for these local variables, say
(trying to keep herd7 happy):

P0(int *x, atomic_t *y)
{
	int r0;
	int r1;

	r0 = READ_ONCE(*x);
	smp_rmb();
	r1 = atomic_read(y);
}

Thanks,
  Andrea

Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

[Boqun Feng]

On Fri, Feb 14, 2020 at 09:18:26AM +0100, Andrea Parri wrote:
> > > @@ -0,0 +1,29 @@
> > > +C Atomic-RMW+mb__after_atomic-is-strong-acquire
> > > +
> > > +(*
> > > + * Result: Never
> > > + *
> > > + * Test of an atomic RMW followed by a smp_mb__after_atomic() is
> > > + * "strong-acquire": both the read and write part of the RMW is ordered before
> > > + * the subsequential memory accesses.
> > > + *)
> > > +
> > > +{
> > > +}
> > > +
> > > +P0(int *x, atomic_t *y)
> > > +{
> > > +	r0 = READ_ONCE(*x);
> > > +	smp_rmb();
> > > +	r1 = atomic_read(y);
> 
> IIRC, klitmus7 needs a declaration for these local variables, say
> (trying to keep herd7 happy):
> 

Got it. I will add the declaration in the next version. It's just that
herd doesn't need those so I haven't put them in this version ;-)

Thanks!

Regards,
Boqun

> P0(int *x, atomic_t *y)
> {
> 	int r0;
> 	int r1;
> 
> 	r0 = READ_ONCE(*x);
> 	smp_rmb();
> 	r1 = atomic_read(y);
> }
> 
> Thanks,
>   Andrea

Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

[Alan Stern]

On Fri, 14 Feb 2020, Boqun Feng wrote:

> We already use a litmus test in atomic_t.txt to describe atomic RMW +
> smp_mb__after_atomic() is "strong acquire" (both the read and the write
> part is ordered).

"strong acquire" is not an appropriate description -- there is no such
thing as a strong acquire in the LKMM -- nor is it a good name for the
litmus test.  A better description would be "stronger than acquire", as
in the sentence preceding the litmus test in atomic_t.txt.

>  So make it a litmus test in memory-model litmus-tests
> directory, so that people can access the litmus easily.
> 
> Additionally, change the processor numbers "P1, P2" to "P0, P1" in
> atomic_t.txt for the consistency with the processor numbers in the
> litmus test, which herd can handle.
> 
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  Documentation/atomic_t.txt                    |  6 ++--
>  ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
>  tools/memory-model/litmus-tests/README        |  5 ++++
>  3 files changed, 37 insertions(+), 3 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> 
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index ceb85ada378e..e3ad4e4cd9ed 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -238,14 +238,14 @@ strictly stronger than ACQUIRE. As illustrated:
>    {
>    }
>  
> -  P1(int *x, atomic_t *y)
> +  P0(int *x, atomic_t *y)
>    {
>      r0 = READ_ONCE(*x);
>      smp_rmb();
>      r1 = atomic_read(y);
>    }
>  
> -  P2(int *x, atomic_t *y)
> +  P1(int *x, atomic_t *y)
>    {
>      atomic_inc(y);
>      smp_mb__after_atomic();
> @@ -260,7 +260,7 @@ This should not happen; but a hypothetical atomic_inc_acquire() --
>  because it would not order the W part of the RMW against the following
>  WRITE_ONCE.  Thus:
>  
> -  P1			P2
> +  P0			P1
>  
>  			t = LL.acq *y (0)
>  			t++;
> diff --git a/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> new file mode 100644
> index 000000000000..e7216cf9d92a
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> @@ -0,0 +1,29 @@
> +C Atomic-RMW+mb__after_atomic-is-strong-acquire
> +
> +(*
> + * Result: Never
> + *
> + * Test of an atomic RMW followed by a smp_mb__after_atomic() is

s/Test of/Test that/

> + * "strong-acquire": both the read and write part of the RMW is ordered before

This should say "stronger than a normal acquire".  And "part" should be
"parts", and "is ordered" should be "are ordered".

Also, please try to arrange the line breaks so that the comment lines
don't have vastly different lengths.

Similar changes should be made for the text added to README.

Alan Stern

Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()

[Boqun Feng]

On Fri, Feb 14, 2020 at 10:58:57AM -0500, Alan Stern wrote:
> On Fri, 14 Feb 2020, Boqun Feng wrote:
> 
> > We already use a litmus test in atomic_t.txt to describe atomic RMW +
> > smp_mb__after_atomic() is "strong acquire" (both the read and the write
> > part is ordered).
> 
> "strong acquire" is not an appropriate description -- there is no such
> thing as a strong acquire in the LKMM -- nor is it a good name for the
> litmus test.  A better description would be "stronger than acquire", as
> in the sentence preceding the litmus test in atomic_t.txt.
> 

Agreed, I will change it. 

And I can't help feeling this is another reason to add more litmus tests
into kernel directory. During the review process you found two places
where we can improve the text of the documents to be aligned to LKMM. I
think we all want to use a unversial language (LKMM) to discuss things
of parallel programming in kernel, and providing more litmus tests to
people so that they can handly use them will cerntainly be helpful on
this ;-)

> >  So make it a litmus test in memory-model litmus-tests
> > directory, so that people can access the litmus easily.
> > 
> > Additionally, change the processor numbers "P1, P2" to "P0, P1" in
> > atomic_t.txt for the consistency with the processor numbers in the
> > litmus test, which herd can handle.
> > 
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > ---
> >  Documentation/atomic_t.txt                    |  6 ++--
> >  ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
> >  tools/memory-model/litmus-tests/README        |  5 ++++
> >  3 files changed, 37 insertions(+), 3 deletions(-)
> >  create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> > 
> > diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> > index ceb85ada378e..e3ad4e4cd9ed 100644
> > --- a/Documentation/atomic_t.txt
> > +++ b/Documentation/atomic_t.txt
> > @@ -238,14 +238,14 @@ strictly stronger than ACQUIRE. As illustrated:
> >    {
> >    }
> >  
> > -  P1(int *x, atomic_t *y)
> > +  P0(int *x, atomic_t *y)
> >    {
> >      r0 = READ_ONCE(*x);
> >      smp_rmb();
> >      r1 = atomic_read(y);
> >    }
> >  
> > -  P2(int *x, atomic_t *y)
> > +  P1(int *x, atomic_t *y)
> >    {
> >      atomic_inc(y);
> >      smp_mb__after_atomic();
> > @@ -260,7 +260,7 @@ This should not happen; but a hypothetical atomic_inc_acquire() --
> >  because it would not order the W part of the RMW against the following
> >  WRITE_ONCE.  Thus:
> >  
> > -  P1			P2
> > +  P0			P1
> >  
> >  			t = LL.acq *y (0)
> >  			t++;
> > diff --git a/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> > new file mode 100644
> > index 000000000000..e7216cf9d92a
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> > @@ -0,0 +1,29 @@
> > +C Atomic-RMW+mb__after_atomic-is-strong-acquire
> > +
> > +(*
> > + * Result: Never
> > + *
> > + * Test of an atomic RMW followed by a smp_mb__after_atomic() is
> 
> s/Test of/Test that/
> 
> > + * "strong-acquire": both the read and write part of the RMW is ordered before
> 
> This should say "stronger than a normal acquire".  And "part" should be
> "parts", and "is ordered" should be "are ordered".
> 

Thanks! I will improve in the next version.

> Also, please try to arrange the line breaks so that the comment lines
> don't have vastly different lengths.
> 
> Similar changes should be made for the text added to README.
> 

Got it.

Regards,
Boqun

> Alan Stern
> 

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Peter Zijlstra]

On Fri, Feb 14, 2020 at 12:01:29PM +0800, Boqun Feng wrote:
> A recent discussion raises up the requirement for having test cases for
> atomic APIs:
> 
> 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> 
> , and since we already have a way to generate a test module from a
> litmus test with klitmus[1]. It makes sense that we add more litmus
> tests for atomic APIs into memory-model.
> 
> So I begin to do this and the plan is to add the litmus tests we already
> use in atomic_t.txt, ones from Paul's litmus collection[2], and any
> other valuable litmus test we come up while adding the previous two
> kinds of tests.
> 
> This patchset finishes the first part (adding atomic_t.txt litmus
> tests). I also improve the atomic_t.txt to make it consistent with the
> litmus tests.
> 
> One thing to note is patch #2 requires a modification to herd and I just
> made a PR to Luc's repo:
> 
> 	https://github.com/herd/herdtools7/pull/28
> 
> , so if this patchset looks good to everyone and someone plans to take
> it (and I assume is Paul), please wait until that PR is settled. And
> probably we need to bump the required herd version because of it.
> 
> Comments and suggesions are welcome!

Very nice, thanks!

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Paul E. McKenney]

On Fri, Feb 14, 2020 at 12:01:29PM +0800, Boqun Feng wrote:
> A recent discussion raises up the requirement for having test cases for
> atomic APIs:
> 
> 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> 
> , and since we already have a way to generate a test module from a
> litmus test with klitmus[1]. It makes sense that we add more litmus
> tests for atomic APIs into memory-model.
> 
> So I begin to do this and the plan is to add the litmus tests we already
> use in atomic_t.txt, ones from Paul's litmus collection[2], and any
> other valuable litmus test we come up while adding the previous two
> kinds of tests.
> 
> This patchset finishes the first part (adding atomic_t.txt litmus
> tests). I also improve the atomic_t.txt to make it consistent with the
> litmus tests.
> 
> One thing to note is patch #2 requires a modification to herd and I just
> made a PR to Luc's repo:
> 
> 	https://github.com/herd/herdtools7/pull/28
> 
> , so if this patchset looks good to everyone and someone plans to take
> it (and I assume is Paul), please wait until that PR is settled. And
> probably we need to bump the required herd version because of it.

Please let me know when you are ready for me to take them, and thank
you for doing this!

							Thanx, Paul

> Comments and suggesions are welcome!
> 
> Regards,
> Boqun
> 
> 
> [1]: http://diy.inria.fr/doc/litmus.html#klitmus
> [2]: https://github.com/paulmckrcu/litmus/tree/master/manual/atomic
> 
> *** BLURB HERE ***
> 
> Boqun Feng (3):
>   Documentation/locking/atomic: Fix atomic-set litmus test
>   tools/memory-model: Add a litmus test for atomic_set()
>   tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic()
> 
>  Documentation/atomic_t.txt                    | 14 ++++-----
>  ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
>  .../Atomic-set-observable-to-RMW.litmus       | 24 +++++++++++++++
>  tools/memory-model/litmus-tests/README        |  8 +++++
>  4 files changed, 68 insertions(+), 7 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
>  create mode 100644 tools/memory-model/litmus-tests/Atomic-set-observable-to-RMW.litmus
> 
> -- 
> 2.25.0
> 

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Alan Stern]

On Fri, 14 Feb 2020, Boqun Feng wrote:

> A recent discussion raises up the requirement for having test cases for
> atomic APIs:
> 
> 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> 
> , and since we already have a way to generate a test module from a
> litmus test with klitmus[1]. It makes sense that we add more litmus
> tests for atomic APIs into memory-model.

It might be worth discussing this point a little more fully.  The 
set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
limited.  Paul has a vastly more expansive set of litmus tests in a 
GitHub repository, and I am doubtful about how many new tests we want 
to keep in the kernel source.

Perhaps it makes sense to have tests corresponding to all the examples
in Documentation/, perhaps not.  How do people feel about this?

Alan

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Boqun Feng]

On Fri, Feb 14, 2020 at 10:27:44AM -0500, Alan Stern wrote:
> On Fri, 14 Feb 2020, Boqun Feng wrote:
> 
> > A recent discussion raises up the requirement for having test cases for
> > atomic APIs:
> > 
> > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > 
> > , and since we already have a way to generate a test module from a
> > litmus test with klitmus[1]. It makes sense that we add more litmus
> > tests for atomic APIs into memory-model.
> 
> It might be worth discussing this point a little more fully.  The 

I'm open to any suggestion, and ...

> set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
> limited.  Paul has a vastly more expansive set of litmus tests in a 

I'm OK if we want to limit the number of litmus tests in
tools/memory-model/litmus-tests directory. But ...

> GitHub repository, and I am doubtful about how many new tests we want 
> to keep in the kernel source.
> 

I think we all agree we want to use litmus tests as much as possbile for
discussing locking/parallel programming/memory model related problems,
right? This is benefical for both kernel and the herd tool, as they can
improve each other.

Atomic APIs (perhaps even {READ,WRITE}_ONCE(), smp_load_acquire() and
smp_store_release()) have been longing for some more concrete examples
as a complement for the semantics description in the docs, so that
people can check their understandings. Further, with the help of
klitmus, the litmus tests can be a useful tool for testing if a new arch
support is added to kernel. That's why I plan to add litmus tests into
kernel source.

Thoughts?

Regards,
Boqun

> Perhaps it makes sense to have tests corresponding to all the examples
> in Documentation/, perhaps not.  How do people feel about this?
> 
> Alan
> 

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Paul E. McKenney]

On Fri, Feb 14, 2020 at 10:27:44AM -0500, Alan Stern wrote:
> On Fri, 14 Feb 2020, Boqun Feng wrote:
> 
> > A recent discussion raises up the requirement for having test cases for
> > atomic APIs:
> > 
> > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > 
> > , and since we already have a way to generate a test module from a
> > litmus test with klitmus[1]. It makes sense that we add more litmus
> > tests for atomic APIs into memory-model.
> 
> It might be worth discussing this point a little more fully.  The 
> set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
> limited.  Paul has a vastly more expansive set of litmus tests in a 
> GitHub repository, and I am doubtful about how many new tests we want 
> to keep in the kernel source.

Indeed, the current view is that the litmus tests in the kernel source
tree are intended to provide examples of C-litmus-test-language features
and functions, as opposed to exercising the full cross-product of
Linux-kernel synchronization primitives.

For a semi-reasonable subset of that cross-product, as Alan says, please
see https://github.com/paulmckrcu/litmus.

For a list of the Linux-kernel synchronization primitives currently
supported by LKMM, please see tools/memory-model/linux-kernel.def.

> Perhaps it makes sense to have tests corresponding to all the examples
> in Documentation/, perhaps not.  How do people feel about this?

Agreed, we don't want to say that the set of litmus tests in the kernel
source tree is limited for all time to the set currently present, but
rather that the justification for adding more would involve useful and
educational examples of litmus-test features and techniques rather than
being a full-up LKMM test suite.

I would guess that there are litmus-test tricks that could usefully
be added to tools/memory-model/litmus-tests.  Any nomination?  Perhaps
handling CAS loops while maintaining finite state space?  Something else?

							Thanx, Paul

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Boqun Feng]

On Sat, Feb 15, 2020 at 07:25:50AM -0800, Paul E. McKenney wrote:
> On Fri, Feb 14, 2020 at 10:27:44AM -0500, Alan Stern wrote:
> > On Fri, 14 Feb 2020, Boqun Feng wrote:
> > 
> > > A recent discussion raises up the requirement for having test cases for
> > > atomic APIs:
> > > 
> > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > 
> > > , and since we already have a way to generate a test module from a
> > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > tests for atomic APIs into memory-model.
> > 
> > It might be worth discussing this point a little more fully.  The 
> > set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
> > limited.  Paul has a vastly more expansive set of litmus tests in a 
> > GitHub repository, and I am doubtful about how many new tests we want 
> > to keep in the kernel source.
> 
> Indeed, the current view is that the litmus tests in the kernel source
> tree are intended to provide examples of C-litmus-test-language features
> and functions, as opposed to exercising the full cross-product of
> Linux-kernel synchronization primitives.
> 
> For a semi-reasonable subset of that cross-product, as Alan says, please
> see https://github.com/paulmckrcu/litmus.
> 
> For a list of the Linux-kernel synchronization primitives currently
> supported by LKMM, please see tools/memory-model/linux-kernel.def.
> 

So how about I put those atomic API tests into a separate directory, say
Documentation/atomic/ ?

The problem I want to solve here is that people (usually who implements
the atomic APIs for new archs) may want some examples, which can help
them understand the API requirements and test the implementation. And
litmus tests are the perfect tool here (given that them can be
translated to test modules with klitmus). And I personally really think
this is something the LKMM group should maintain, that's why I put them
in the tools/memory-model/litmus-tests/. But I'm OK if we end up
deciding those should be put outside that directory.

Regards,
Boqun

> > Perhaps it makes sense to have tests corresponding to all the examples
> > in Documentation/, perhaps not.  How do people feel about this?
> 
> Agreed, we don't want to say that the set of litmus tests in the kernel
> source tree is limited for all time to the set currently present, but
> rather that the justification for adding more would involve useful and
> educational examples of litmus-test features and techniques rather than
> being a full-up LKMM test suite.
> 
> I would guess that there are litmus-test tricks that could usefully
> be added to tools/memory-model/litmus-tests.  Any nomination?  Perhaps
> handling CAS loops while maintaining finite state space?  Something else?
> 
> 							Thanx, Paul

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Paul E. McKenney]

On Sun, Feb 16, 2020 at 01:43:45PM +0800, Boqun Feng wrote:
> On Sat, Feb 15, 2020 at 07:25:50AM -0800, Paul E. McKenney wrote:
> > On Fri, Feb 14, 2020 at 10:27:44AM -0500, Alan Stern wrote:
> > > On Fri, 14 Feb 2020, Boqun Feng wrote:
> > > 
> > > > A recent discussion raises up the requirement for having test cases for
> > > > atomic APIs:
> > > > 
> > > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > > 
> > > > , and since we already have a way to generate a test module from a
> > > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > > tests for atomic APIs into memory-model.
> > > 
> > > It might be worth discussing this point a little more fully.  The 
> > > set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
> > > limited.  Paul has a vastly more expansive set of litmus tests in a 
> > > GitHub repository, and I am doubtful about how many new tests we want 
> > > to keep in the kernel source.
> > 
> > Indeed, the current view is that the litmus tests in the kernel source
> > tree are intended to provide examples of C-litmus-test-language features
> > and functions, as opposed to exercising the full cross-product of
> > Linux-kernel synchronization primitives.
> > 
> > For a semi-reasonable subset of that cross-product, as Alan says, please
> > see https://github.com/paulmckrcu/litmus.
> > 
> > For a list of the Linux-kernel synchronization primitives currently
> > supported by LKMM, please see tools/memory-model/linux-kernel.def.
> > 
> 
> So how about I put those atomic API tests into a separate directory, say
> Documentation/atomic/ ?
> 
> The problem I want to solve here is that people (usually who implements
> the atomic APIs for new archs) may want some examples, which can help
> them understand the API requirements and test the implementation. And
> litmus tests are the perfect tool here (given that them can be
> translated to test modules with klitmus). And I personally really think
> this is something the LKMM group should maintain, that's why I put them
> in the tools/memory-model/litmus-tests/. But I'm OK if we end up
> deciding those should be put outside that directory.

Good point!

However, we should dicuss this with the proposed beneficiaries, namely
the architecture maintainers.  Do they want it?  If so, where would
they like it to be?  How should it be organized?

In the meantime, I am more than happy to accept litmus tests into the
github archive.

So how would you like to proceed?

							Thanx, Paul

> Regards,
> Boqun
> 
> > > Perhaps it makes sense to have tests corresponding to all the examples
> > > in Documentation/, perhaps not.  How do people feel about this?
> > 
> > Agreed, we don't want to say that the set of litmus tests in the kernel
> > source tree is limited for all time to the set currently present, but
> > rather that the justification for adding more would involve useful and
> > educational examples of litmus-test features and techniques rather than
> > being a full-up LKMM test suite.
> > 
> > I would guess that there are litmus-test tricks that could usefully
> > be added to tools/memory-model/litmus-tests.  Any nomination?  Perhaps
> > handling CAS loops while maintaining finite state space?  Something else?
> > 
> > 							Thanx, Paul

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Alan Stern]

On Sun, 16 Feb 2020, Paul E. McKenney wrote:

> On Sun, Feb 16, 2020 at 01:43:45PM +0800, Boqun Feng wrote:
> > On Sat, Feb 15, 2020 at 07:25:50AM -0800, Paul E. McKenney wrote:
> > > On Fri, Feb 14, 2020 at 10:27:44AM -0500, Alan Stern wrote:
> > > > On Fri, 14 Feb 2020, Boqun Feng wrote:
> > > > 
> > > > > A recent discussion raises up the requirement for having test cases for
> > > > > atomic APIs:
> > > > > 
> > > > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > > > 
> > > > > , and since we already have a way to generate a test module from a
> > > > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > > > tests for atomic APIs into memory-model.
> > > > 
> > > > It might be worth discussing this point a little more fully.  The 
> > > > set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
> > > > limited.  Paul has a vastly more expansive set of litmus tests in a 
> > > > GitHub repository, and I am doubtful about how many new tests we want 
> > > > to keep in the kernel source.
> > > 
> > > Indeed, the current view is that the litmus tests in the kernel source
> > > tree are intended to provide examples of C-litmus-test-language features
> > > and functions, as opposed to exercising the full cross-product of
> > > Linux-kernel synchronization primitives.
> > > 
> > > For a semi-reasonable subset of that cross-product, as Alan says, please
> > > see https://github.com/paulmckrcu/litmus.
> > > 
> > > For a list of the Linux-kernel synchronization primitives currently
> > > supported by LKMM, please see tools/memory-model/linux-kernel.def.
> > > 
> > 
> > So how about I put those atomic API tests into a separate directory, say
> > Documentation/atomic/ ?
> > 
> > The problem I want to solve here is that people (usually who implements
> > the atomic APIs for new archs) may want some examples, which can help
> > them understand the API requirements and test the implementation. And
> > litmus tests are the perfect tool here (given that them can be
> > translated to test modules with klitmus). And I personally really think
> > this is something the LKMM group should maintain, that's why I put them
> > in the tools/memory-model/litmus-tests/. But I'm OK if we end up
> > deciding those should be put outside that directory.
> 
> Good point!
> 
> However, we should dicuss this with the proposed beneficiaries, namely
> the architecture maintainers.  Do they want it?  If so, where would
> they like it to be?  How should it be organized?
> 
> In the meantime, I am more than happy to accept litmus tests into the
> github archive.
> 
> So how would you like to proceed?

I think it makes sense to put Boqun's tests under Documentation/ rather
than tools/.  After all, their point is to document the memory model's
requirements for operations on atomic_t's.  They aren't meant to be
examples or demos showing how to use herd or write litmus tests.

Alan

Re: [RFC 0/3] tools/memory-model: Add litmus tests for atomic APIs

[Boqun Feng]

On Sun, Feb 16, 2020 at 11:16:50AM -0500, Alan Stern wrote:
> On Sun, 16 Feb 2020, Paul E. McKenney wrote:
> 
> > On Sun, Feb 16, 2020 at 01:43:45PM +0800, Boqun Feng wrote:
> > > On Sat, Feb 15, 2020 at 07:25:50AM -0800, Paul E. McKenney wrote:
> > > > On Fri, Feb 14, 2020 at 10:27:44AM -0500, Alan Stern wrote:
> > > > > On Fri, 14 Feb 2020, Boqun Feng wrote:
> > > > > 
> > > > > > A recent discussion raises up the requirement for having test cases for
> > > > > > atomic APIs:
> > > > > > 
> > > > > > 	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/
> > > > > > 
> > > > > > , and since we already have a way to generate a test module from a
> > > > > > litmus test with klitmus[1]. It makes sense that we add more litmus
> > > > > > tests for atomic APIs into memory-model.
> > > > > 
> > > > > It might be worth discussing this point a little more fully.  The 
> > > > > set of tests in tools/memory-model/litmus-tests/ is deliberately rather 
> > > > > limited.  Paul has a vastly more expansive set of litmus tests in a 
> > > > > GitHub repository, and I am doubtful about how many new tests we want 
> > > > > to keep in the kernel source.
> > > > 
> > > > Indeed, the current view is that the litmus tests in the kernel source
> > > > tree are intended to provide examples of C-litmus-test-language features
> > > > and functions, as opposed to exercising the full cross-product of
> > > > Linux-kernel synchronization primitives.
> > > > 
> > > > For a semi-reasonable subset of that cross-product, as Alan says, please
> > > > see https://github.com/paulmckrcu/litmus.
> > > > 
> > > > For a list of the Linux-kernel synchronization primitives currently
> > > > supported by LKMM, please see tools/memory-model/linux-kernel.def.
> > > > 
> > > 
> > > So how about I put those atomic API tests into a separate directory, say
> > > Documentation/atomic/ ?
> > > 
> > > The problem I want to solve here is that people (usually who implements
> > > the atomic APIs for new archs) may want some examples, which can help
> > > them understand the API requirements and test the implementation. And
> > > litmus tests are the perfect tool here (given that them can be
> > > translated to test modules with klitmus). And I personally really think
> > > this is something the LKMM group should maintain, that's why I put them
> > > in the tools/memory-model/litmus-tests/. But I'm OK if we end up
> > > deciding those should be put outside that directory.
> > 
> > Good point!
> > 
> > However, we should dicuss this with the proposed beneficiaries, namely
> > the architecture maintainers.  Do they want it?  If so, where would
> > they like it to be?  How should it be organized?
> > 

Paul,

Well, I was simply motivated by the discuss on microblaze's atomic
implementation (which I pasted the link in this cover letter):

	https://lore.kernel.org/lkml/20200213085849.GL14897@hirez.programming.kicks-ass.net/

, please see the last paragraph, Michal asking Peter for some tests. So
I think there is at least some one wanting this ;-)

> > In the meantime, I am more than happy to accept litmus tests into the
> > github archive.
> > 

Thanks ;-)

> > So how would you like to proceed?

I think we are still at the discussion stage, so I'm happy to see
suggestions on where to put the litmus tests and which litmus tests
should be included.

> 
> I think it makes sense to put Boqun's tests under Documentation/ rather
> than tools/.  After all, their point is to document the memory model's
> requirements for operations on atomic_t's.  They aren't meant to be
> examples or demos showing how to use herd or write litmus tests.
> 

Alan,

Got it. I will create the Documentation/atomic directory and put the
litmus tests there in the next version.

Thank you both!

Regards,
Boqun

> Alan
>