[PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Boqun Feng]

A recent discussion[1] shows that we are in favor of strengthening the
ordering of unlock + lock on the same CPU: a unlock and a po-after lock
should provide the so-called RCtso ordering, that is a memory access S
po-before the unlock should be ordered against a memory access R
po-after the lock, unless S is a store and R is a load.

The strengthening meets programmers' expection that "sequence of two
locked regions to be ordered wrt each other" (from Linus), and can
reduce the mental burden when using locks. Therefore add it in LKMM.

[1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/

Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
Alan,

I added the "Co-developed-by" and "Signed-off-by" tags since most of the
work is done by you. Feel free to let me know if you want to change
anything.

Regards,
Boqun


 .../Documentation/explanation.txt             | 44 +++++++++++--------
 tools/memory-model/linux-kernel.cat           |  6 +--
 ...LB+unlocklockonceonce+poacquireonce.litmus | 33 ++++++++++++++
 ...unlocklockonceonce+fencermbonceonce.litmus | 33 ++++++++++++++
 tools/memory-model/litmus-tests/README        |  8 ++++
 5 files changed, 102 insertions(+), 22 deletions(-)
 create mode 100644 tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
 create mode 100644 tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus

diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 5d72f3112e56..394ee57d58f2 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -1813,15 +1813,16 @@ spin_trylock() -- we can call these things lock-releases and
 lock-acquires -- have two properties beyond those of ordinary releases
 and acquires.
 
-First, when a lock-acquire reads from a lock-release, the LKMM
-requires that every instruction po-before the lock-release must
-execute before any instruction po-after the lock-acquire.  This would
-naturally hold if the release and acquire operations were on different
-CPUs, but the LKMM says it holds even when they are on the same CPU.
-For example:
+First, when a lock-acquire reads from or is po-after a lock-release,
+the LKMM requires that every instruction po-before the lock-release
+must execute before any instruction po-after the lock-acquire.  This
+would naturally hold if the release and acquire operations were on
+different CPUs and accessed the same lock variable, but the LKMM says
+it also holds when they are on the same CPU, even if they access
+different lock variables.  For example:
 
 	int x, y;
-	spinlock_t s;
+	spinlock_t s, t;
 
 	P0()
 	{
@@ -1830,9 +1831,9 @@ For example:
 		spin_lock(&s);
 		r1 = READ_ONCE(x);
 		spin_unlock(&s);
-		spin_lock(&s);
+		spin_lock(&t);
 		r2 = READ_ONCE(y);
-		spin_unlock(&s);
+		spin_unlock(&t);
 	}
 
 	P1()
@@ -1842,10 +1843,10 @@ For example:
 		WRITE_ONCE(x, 1);
 	}
 
-Here the second spin_lock() reads from the first spin_unlock(), and
-therefore the load of x must execute before the load of y.  Thus we
-cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
-MP pattern).
+Here the second spin_lock() is po-after the first spin_unlock(), and
+therefore the load of x must execute before the load of y, even though
+the two locking operations use different locks.  Thus we cannot have
+r1 = 1 and r2 = 0 at the end (this is an instance of the MP pattern).
 
 This requirement does not apply to ordinary release and acquire
 fences, only to lock-related operations.  For instance, suppose P0()
@@ -1872,13 +1873,13 @@ instructions in the following order:
 
 and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
 
-Second, when a lock-acquire reads from a lock-release, and some other
-stores W and W' occur po-before the lock-release and po-after the
-lock-acquire respectively, the LKMM requires that W must propagate to
-each CPU before W' does.  For example, consider:
+Second, when a lock-acquire reads from or is po-after a lock-release,
+and some other stores W and W' occur po-before the lock-release and
+po-after the lock-acquire respectively, the LKMM requires that W must
+propagate to each CPU before W' does.  For example, consider:
 
 	int x, y;
-	spinlock_t x;
+	spinlock_t s;
 
 	P0()
 	{
@@ -1908,7 +1909,12 @@ each CPU before W' does.  For example, consider:
 
 If r1 = 1 at the end then the spin_lock() in P1 must have read from
 the spin_unlock() in P0.  Hence the store to x must propagate to P2
-before the store to y does, so we cannot have r2 = 1 and r3 = 0.
+before the store to y does, so we cannot have r2 = 1 and r3 = 0.  But
+if P1 had used a lock variable different from s, the writes could have
+propagated in either order.  (On the other hand, if the code in P0 and
+P1 had all executed on a single CPU, as in the example before this
+one, then the writes would have propagated in order even if the two
+critical sections used different lock variables.)
 
 These two special requirements for lock-release and lock-acquire do
 not arise from the operational model.  Nevertheless, kernel developers
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 2a9b4fe4a84e..d70315fddef6 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -27,7 +27,7 @@ include "lock.cat"
 (* Release Acquire *)
 let acq-po = [Acquire] ; po ; [M]
 let po-rel = [M] ; po ; [Release]
-let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
+let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po
 
 (* Fences *)
 let R4rmb = R \ Noreturn	(* Reads for which rmb works *)
@@ -70,12 +70,12 @@ let rwdep = (dep | ctrl) ; [W]
 let overwrite = co | fr
 let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
 let to-r = addr | (dep ; [Marked] ; rfi)
-let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
+let ppo = to-r | to-w | fence | (po-unlock-lock-po & int)
 
 (* Propagation: Ordering from release operations and strong fences. *)
 let A-cumul(r) = (rfe ; [Marked])? ; r
 let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
-	po-unlock-rf-lock-po) ; [Marked]
+	po-unlock-lock-po) ; [Marked]
 let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
 	[Marked] ; rfe? ; [Marked]
 
diff --git a/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
new file mode 100644
index 000000000000..955b9c7cdc7f
--- /dev/null
+++ b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
@@ -0,0 +1,33 @@
+C LB+unlocklockonceonce+poacquireonce
+
+(*
+ * Result: Never
+ *
+ * If two locked critical sections execute on the same CPU, all accesses
+ * in the first must execute before any accesses in the second, even if
+ * the critical sections are protected by different locks.
+ *)
+
+{}
+
+P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
+{
+	int r1;
+
+	spin_lock(s);
+	r1 = READ_ONCE(*x);
+	spin_unlock(s);
+	spin_lock(t);
+	WRITE_ONCE(*y, 1);
+	spin_unlock(t);
+}
+
+P1(int *x, int *y)
+{
+	int r2;
+
+	r2 = smp_load_acquire(y);
+	WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r2=1)
diff --git a/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus
new file mode 100644
index 000000000000..2feb1398be71
--- /dev/null
+++ b/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus
@@ -0,0 +1,33 @@
+C MP+unlocklockonceonce+fencermbonceonce
+
+(*
+ * Result: Never
+ *
+ * If two locked critical sections execute on the same CPU, stores in the
+ * first must propagate to each CPU before stores in the second do, even if
+ * the critical sections are protected by different locks.
+ *)
+
+{}
+
+P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
+{
+	spin_lock(s);
+	WRITE_ONCE(*x, 1);
+	spin_unlock(s);
+	spin_lock(t);
+	WRITE_ONCE(*y, 1);
+	spin_unlock(t);
+}
+
+P1(int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	r2 = READ_ONCE(*x);
+}
+
+exists (1:r1=1 /\ 1:r2=0)
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 681f9067fa9e..d311a0ff1ae6 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -63,6 +63,10 @@ LB+poonceonces.litmus
 	As above, but with store-release replaced with WRITE_ONCE()
 	and load-acquire replaced with READ_ONCE().
 
+LB+unlocklockonceonce+poacquireonce.litmus
+	Does a unlock+lock pair provides ordering guarantee between a
+	load and a store?
+
 MP+onceassign+derefonce.litmus
 	As below, but with rcu_assign_pointer() and an rcu_dereference().
 
@@ -90,6 +94,10 @@ MP+porevlocks.litmus
 	As below, but with the first access of the writer process
 	and the second access of reader process protected by a lock.
 
+MP+unlocklockonceonce+fencermbonceonce.litmus
+	Does a unlock+lock pair provides ordering guarantee between a
+	store and another store?
+
 MP+fencewmbonceonce+fencermbonceonce.litmus
 	Does a smp_wmb() (between the stores) and an smp_rmb() (between
 	the loads) suffice for the message-passing litmus test, where one
-- 
2.32.0

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Alan Stern]

On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> A recent discussion[1] shows that we are in favor of strengthening the
> ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> should provide the so-called RCtso ordering, that is a memory access S
> po-before the unlock should be ordered against a memory access R
> po-after the lock, unless S is a store and R is a load.
> 
> The strengthening meets programmers' expection that "sequence of two
> locked regions to be ordered wrt each other" (from Linus), and can
> reduce the mental burden when using locks. Therefore add it in LKMM.
> 
> [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> 
> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
> Alan,
> 
> I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> work is done by you. Feel free to let me know if you want to change
> anything.

It looks good to me.  However, do we really want to add these litmus
tests to the kernel source, or would it be better to keep them with
the thousands of other tests in Paul's archives?

Alan

> Regards,
> Boqun

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Paul E. McKenney]

On Thu, Sep 30, 2021 at 11:20:33AM -0400, Alan Stern wrote:
> On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> > A recent discussion[1] shows that we are in favor of strengthening the
> > ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> > should provide the so-called RCtso ordering, that is a memory access S
> > po-before the unlock should be ordered against a memory access R
> > po-after the lock, unless S is a store and R is a load.
> > 
> > The strengthening meets programmers' expection that "sequence of two
> > locked regions to be ordered wrt each other" (from Linus), and can
> > reduce the mental burden when using locks. Therefore add it in LKMM.
> > 
> > [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> > 
> > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > ---
> > Alan,
> > 
> > I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> > work is done by you. Feel free to let me know if you want to change
> > anything.
> 
> It looks good to me.  However, do we really want to add these litmus
> tests to the kernel source, or would it be better to keep them with
> the thousands of other tests in Paul's archives?

Either way works for me.  But if they are referred to from within the
kernel, it is best to have them in the kernel source.  Which might be seen
as a reason to minimize referring to litmus tests from the kernel.  ;-)

							Thanx, Paul

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Alan Stern]

On Thu, Sep 30, 2021 at 11:17:53AM -0700, Paul E. McKenney wrote:
> On Thu, Sep 30, 2021 at 11:20:33AM -0400, Alan Stern wrote:
> > On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> > > A recent discussion[1] shows that we are in favor of strengthening the
> > > ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> > > should provide the so-called RCtso ordering, that is a memory access S
> > > po-before the unlock should be ordered against a memory access R
> > > po-after the lock, unless S is a store and R is a load.
> > > 
> > > The strengthening meets programmers' expection that "sequence of two
> > > locked regions to be ordered wrt each other" (from Linus), and can
> > > reduce the mental burden when using locks. Therefore add it in LKMM.
> > > 
> > > [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> > > 
> > > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > > ---
> > > Alan,
> > > 
> > > I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> > > work is done by you. Feel free to let me know if you want to change
> > > anything.
> > 
> > It looks good to me.  However, do we really want to add these litmus
> > tests to the kernel source, or would it be better to keep them with
> > the thousands of other tests in Paul's archives?
> 
> Either way works for me.  But if they are referred to from within the
> kernel, it is best to have them in the kernel source.  Which might be seen
> as a reason to minimize referring to litmus tests from the kernel.  ;-)

In this case the litmus tests are not referred to within the kernel 
source.

Alan

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Boqun Feng]

On Thu, Sep 30, 2021 at 04:46:34PM -0400, Alan Stern wrote:
> On Thu, Sep 30, 2021 at 11:17:53AM -0700, Paul E. McKenney wrote:
> > On Thu, Sep 30, 2021 at 11:20:33AM -0400, Alan Stern wrote:
> > > On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> > > > A recent discussion[1] shows that we are in favor of strengthening the
> > > > ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> > > > should provide the so-called RCtso ordering, that is a memory access S
> > > > po-before the unlock should be ordered against a memory access R
> > > > po-after the lock, unless S is a store and R is a load.
> > > > 
> > > > The strengthening meets programmers' expection that "sequence of two
> > > > locked regions to be ordered wrt each other" (from Linus), and can
> > > > reduce the mental burden when using locks. Therefore add it in LKMM.
> > > > 
> > > > [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> > > > 
> > > > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > > > ---
> > > > Alan,
> > > > 
> > > > I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> > > > work is done by you. Feel free to let me know if you want to change
> > > > anything.
> > > 
> > > It looks good to me.  However, do we really want to add these litmus
> > > tests to the kernel source, or would it be better to keep them with
> > > the thousands of other tests in Paul's archives?
> > 
> > Either way works for me.  But if they are referred to from within the
> > kernel, it is best to have them in the kernel source.  Which might be seen
> > as a reason to minimize referring to litmus tests from the kernel.  ;-)
> 
> In this case the litmus tests are not referred to within the kernel 
> source.
> 

I'm OK to drop the litmus tests, but the reason I add the two litmus
tests is that they directly describe one of our memory model rules. The
two litmus tests tells developers "you can use unlock+lock on the same
CPU to order READ->WRITE or WRITE->WRITE", so they are kind of part of
the manual of our memory model. Thoughts?

Regards,
Boqun


> Alan

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Boqun Feng]

(Add linux-arch in Cc list)

Architecture maintainers, this patch is about strengthening our memory
model a little bit, your inputs (confirmation, ack/nack, etc.) are
appreciated.

Regards,
Boqun

On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> A recent discussion[1] shows that we are in favor of strengthening the
> ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> should provide the so-called RCtso ordering, that is a memory access S
> po-before the unlock should be ordered against a memory access R
> po-after the lock, unless S is a store and R is a load.
> 
> The strengthening meets programmers' expection that "sequence of two
> locked regions to be ordered wrt each other" (from Linus), and can
> reduce the mental burden when using locks. Therefore add it in LKMM.
> 
> [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> 
> Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
> Alan,
> 
> I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> work is done by you. Feel free to let me know if you want to change
> anything.
> 
> Regards,
> Boqun
> 
> 
>  .../Documentation/explanation.txt             | 44 +++++++++++--------
>  tools/memory-model/linux-kernel.cat           |  6 +--
>  ...LB+unlocklockonceonce+poacquireonce.litmus | 33 ++++++++++++++
>  ...unlocklockonceonce+fencermbonceonce.litmus | 33 ++++++++++++++
>  tools/memory-model/litmus-tests/README        |  8 ++++
>  5 files changed, 102 insertions(+), 22 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
>  create mode 100644 tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus
> 
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 5d72f3112e56..394ee57d58f2 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -1813,15 +1813,16 @@ spin_trylock() -- we can call these things lock-releases and
>  lock-acquires -- have two properties beyond those of ordinary releases
>  and acquires.
>  
> -First, when a lock-acquire reads from a lock-release, the LKMM
> -requires that every instruction po-before the lock-release must
> -execute before any instruction po-after the lock-acquire.  This would
> -naturally hold if the release and acquire operations were on different
> -CPUs, but the LKMM says it holds even when they are on the same CPU.
> -For example:
> +First, when a lock-acquire reads from or is po-after a lock-release,
> +the LKMM requires that every instruction po-before the lock-release
> +must execute before any instruction po-after the lock-acquire.  This
> +would naturally hold if the release and acquire operations were on
> +different CPUs and accessed the same lock variable, but the LKMM says
> +it also holds when they are on the same CPU, even if they access
> +different lock variables.  For example:
>  
>  	int x, y;
> -	spinlock_t s;
> +	spinlock_t s, t;
>  
>  	P0()
>  	{
> @@ -1830,9 +1831,9 @@ For example:
>  		spin_lock(&s);
>  		r1 = READ_ONCE(x);
>  		spin_unlock(&s);
> -		spin_lock(&s);
> +		spin_lock(&t);
>  		r2 = READ_ONCE(y);
> -		spin_unlock(&s);
> +		spin_unlock(&t);
>  	}
>  
>  	P1()
> @@ -1842,10 +1843,10 @@ For example:
>  		WRITE_ONCE(x, 1);
>  	}
>  
> -Here the second spin_lock() reads from the first spin_unlock(), and
> -therefore the load of x must execute before the load of y.  Thus we
> -cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
> -MP pattern).
> +Here the second spin_lock() is po-after the first spin_unlock(), and
> +therefore the load of x must execute before the load of y, even though
> +the two locking operations use different locks.  Thus we cannot have
> +r1 = 1 and r2 = 0 at the end (this is an instance of the MP pattern).
>  
>  This requirement does not apply to ordinary release and acquire
>  fences, only to lock-related operations.  For instance, suppose P0()
> @@ -1872,13 +1873,13 @@ instructions in the following order:
>  
>  and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
>  
> -Second, when a lock-acquire reads from a lock-release, and some other
> -stores W and W' occur po-before the lock-release and po-after the
> -lock-acquire respectively, the LKMM requires that W must propagate to
> -each CPU before W' does.  For example, consider:
> +Second, when a lock-acquire reads from or is po-after a lock-release,
> +and some other stores W and W' occur po-before the lock-release and
> +po-after the lock-acquire respectively, the LKMM requires that W must
> +propagate to each CPU before W' does.  For example, consider:
>  
>  	int x, y;
> -	spinlock_t x;
> +	spinlock_t s;
>  
>  	P0()
>  	{
> @@ -1908,7 +1909,12 @@ each CPU before W' does.  For example, consider:
>  
>  If r1 = 1 at the end then the spin_lock() in P1 must have read from
>  the spin_unlock() in P0.  Hence the store to x must propagate to P2
> -before the store to y does, so we cannot have r2 = 1 and r3 = 0.
> +before the store to y does, so we cannot have r2 = 1 and r3 = 0.  But
> +if P1 had used a lock variable different from s, the writes could have
> +propagated in either order.  (On the other hand, if the code in P0 and
> +P1 had all executed on a single CPU, as in the example before this
> +one, then the writes would have propagated in order even if the two
> +critical sections used different lock variables.)
>  
>  These two special requirements for lock-release and lock-acquire do
>  not arise from the operational model.  Nevertheless, kernel developers
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 2a9b4fe4a84e..d70315fddef6 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -27,7 +27,7 @@ include "lock.cat"
>  (* Release Acquire *)
>  let acq-po = [Acquire] ; po ; [M]
>  let po-rel = [M] ; po ; [Release]
> -let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
> +let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po
>  
>  (* Fences *)
>  let R4rmb = R \ Noreturn	(* Reads for which rmb works *)
> @@ -70,12 +70,12 @@ let rwdep = (dep | ctrl) ; [W]
>  let overwrite = co | fr
>  let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
>  let to-r = addr | (dep ; [Marked] ; rfi)
> -let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
> +let ppo = to-r | to-w | fence | (po-unlock-lock-po & int)
>  
>  (* Propagation: Ordering from release operations and strong fences. *)
>  let A-cumul(r) = (rfe ; [Marked])? ; r
>  let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> -	po-unlock-rf-lock-po) ; [Marked]
> +	po-unlock-lock-po) ; [Marked]
>  let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
>  	[Marked] ; rfe? ; [Marked]
>  
> diff --git a/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
> new file mode 100644
> index 000000000000..955b9c7cdc7f
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus
> @@ -0,0 +1,33 @@
> +C LB+unlocklockonceonce+poacquireonce
> +
> +(*
> + * Result: Never
> + *
> + * If two locked critical sections execute on the same CPU, all accesses
> + * in the first must execute before any accesses in the second, even if
> + * the critical sections are protected by different locks.
> + *)
> +
> +{}
> +
> +P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
> +{
> +	int r1;
> +
> +	spin_lock(s);
> +	r1 = READ_ONCE(*x);
> +	spin_unlock(s);
> +	spin_lock(t);
> +	WRITE_ONCE(*y, 1);
> +	spin_unlock(t);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r2;
> +
> +	r2 = smp_load_acquire(y);
> +	WRITE_ONCE(*x, 1);
> +}
> +
> +exists (0:r1=1 /\ 1:r2=1)
> diff --git a/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus
> new file mode 100644
> index 000000000000..2feb1398be71
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus
> @@ -0,0 +1,33 @@
> +C MP+unlocklockonceonce+fencermbonceonce
> +
> +(*
> + * Result: Never
> + *
> + * If two locked critical sections execute on the same CPU, stores in the
> + * first must propagate to each CPU before stores in the second do, even if
> + * the critical sections are protected by different locks.
> + *)
> +
> +{}
> +
> +P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
> +{
> +	spin_lock(s);
> +	WRITE_ONCE(*x, 1);
> +	spin_unlock(s);
> +	spin_lock(t);
> +	WRITE_ONCE(*y, 1);
> +	spin_unlock(t);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r1;
> +	int r2;
> +
> +	r1 = READ_ONCE(*y);
> +	smp_rmb();
> +	r2 = READ_ONCE(*x);
> +}
> +
> +exists (1:r1=1 /\ 1:r2=0)
> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 681f9067fa9e..d311a0ff1ae6 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -63,6 +63,10 @@ LB+poonceonces.litmus
>  	As above, but with store-release replaced with WRITE_ONCE()
>  	and load-acquire replaced with READ_ONCE().
>  
> +LB+unlocklockonceonce+poacquireonce.litmus
> +	Does a unlock+lock pair provides ordering guarantee between a
> +	load and a store?
> +
>  MP+onceassign+derefonce.litmus
>  	As below, but with rcu_assign_pointer() and an rcu_dereference().
>  
> @@ -90,6 +94,10 @@ MP+porevlocks.litmus
>  	As below, but with the first access of the writer process
>  	and the second access of reader process protected by a lock.
>  
> +MP+unlocklockonceonce+fencermbonceonce.litmus
> +	Does a unlock+lock pair provides ordering guarantee between a
> +	store and another store?
> +
>  MP+fencewmbonceonce+fencermbonceonce.litmus
>  	Does a smp_wmb() (between the stores) and an smp_rmb() (between
>  	the loads) suffice for the message-passing litmus test, where one
> -- 
> 2.32.0
> 

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Alan Stern]

On Fri, Oct 01, 2021 at 08:12:56AM +0800, Boqun Feng wrote:
> On Thu, Sep 30, 2021 at 04:46:34PM -0400, Alan Stern wrote:
> > On Thu, Sep 30, 2021 at 11:17:53AM -0700, Paul E. McKenney wrote:
> > > On Thu, Sep 30, 2021 at 11:20:33AM -0400, Alan Stern wrote:
> > > > On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> > > > > A recent discussion[1] shows that we are in favor of strengthening the
> > > > > ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> > > > > should provide the so-called RCtso ordering, that is a memory access S
> > > > > po-before the unlock should be ordered against a memory access R
> > > > > po-after the lock, unless S is a store and R is a load.
> > > > > 
> > > > > The strengthening meets programmers' expection that "sequence of two
> > > > > locked regions to be ordered wrt each other" (from Linus), and can
> > > > > reduce the mental burden when using locks. Therefore add it in LKMM.
> > > > > 
> > > > > [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> > > > > 
> > > > > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > > > > ---
> > > > > Alan,
> > > > > 
> > > > > I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> > > > > work is done by you. Feel free to let me know if you want to change
> > > > > anything.
> > > > 
> > > > It looks good to me.  However, do we really want to add these litmus
> > > > tests to the kernel source, or would it be better to keep them with
> > > > the thousands of other tests in Paul's archives?
> > > 
> > > Either way works for me.  But if they are referred to from within the
> > > kernel, it is best to have them in the kernel source.  Which might be seen
> > > as a reason to minimize referring to litmus tests from the kernel.  ;-)
> > 
> > In this case the litmus tests are not referred to within the kernel 
> > source.
> > 
> 
> I'm OK to drop the litmus tests, but the reason I add the two litmus
> tests is that they directly describe one of our memory model rules. The
> two litmus tests tells developers "you can use unlock+lock on the same
> CPU to order READ->WRITE or WRITE->WRITE", so they are kind of part of
> the manual of our memory model. Thoughts?

The explanation.txt file already contains example litmus tests (not 
in a form acceptable to herd7, though) for these things.

Alan

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Boqun Feng]

On Thu, Sep 30, 2021 at 09:30:55PM -0400, Alan Stern wrote:
> On Fri, Oct 01, 2021 at 08:12:56AM +0800, Boqun Feng wrote:
> > On Thu, Sep 30, 2021 at 04:46:34PM -0400, Alan Stern wrote:
> > > On Thu, Sep 30, 2021 at 11:17:53AM -0700, Paul E. McKenney wrote:
> > > > On Thu, Sep 30, 2021 at 11:20:33AM -0400, Alan Stern wrote:
> > > > > On Thu, Sep 30, 2021 at 09:08:23PM +0800, Boqun Feng wrote:
> > > > > > A recent discussion[1] shows that we are in favor of strengthening the
> > > > > > ordering of unlock + lock on the same CPU: a unlock and a po-after lock
> > > > > > should provide the so-called RCtso ordering, that is a memory access S
> > > > > > po-before the unlock should be ordered against a memory access R
> > > > > > po-after the lock, unless S is a store and R is a load.
> > > > > > 
> > > > > > The strengthening meets programmers' expection that "sequence of two
> > > > > > locked regions to be ordered wrt each other" (from Linus), and can
> > > > > > reduce the mental burden when using locks. Therefore add it in LKMM.
> > > > > > 
> > > > > > [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/
> > > > > > 
> > > > > > Co-developed-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > > > > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > > > > > ---
> > > > > > Alan,
> > > > > > 
> > > > > > I added the "Co-developed-by" and "Signed-off-by" tags since most of the
> > > > > > work is done by you. Feel free to let me know if you want to change
> > > > > > anything.
> > > > > 
> > > > > It looks good to me.  However, do we really want to add these litmus
> > > > > tests to the kernel source, or would it be better to keep them with
> > > > > the thousands of other tests in Paul's archives?
> > > > 
> > > > Either way works for me.  But if they are referred to from within the
> > > > kernel, it is best to have them in the kernel source.  Which might be seen
> > > > as a reason to minimize referring to litmus tests from the kernel.  ;-)
> > > 
> > > In this case the litmus tests are not referred to within the kernel 
> > > source.
> > > 
> > 
> > I'm OK to drop the litmus tests, but the reason I add the two litmus
> > tests is that they directly describe one of our memory model rules. The
> > two litmus tests tells developers "you can use unlock+lock on the same
> > CPU to order READ->WRITE or WRITE->WRITE", so they are kind of part of
> > the manual of our memory model. Thoughts?
> 
> The explanation.txt file already contains example litmus tests (not 
> in a form acceptable to herd7, though) for these things.
> 

Agreed. I just think that runnable litmus tests may be more accurate
than words. But again, I'm OK to drop them.

While we are at it, maybe it's worthwhile to discuss what kind of litmus
tests should be put in tools/memory-model/litmus-tests. Selftests for
.cat changes? Documented patterns for developers to follow? Or something
else?

Regards,
Boqun

> Alan

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Michael Ellerman]

Boqun Feng <boqun.feng@gmail.com> writes:
> (Add linux-arch in Cc list)
>
> Architecture maintainers, this patch is about strengthening our memory
> model a little bit, your inputs (confirmation, ack/nack, etc.) are
> appreciated.

Hi Boqun,

I don't feel like I'm really qualified to give an ack here, you and the
other memory model folk know this stuff much better than me.

But I have reviewed it and it matches my understanding of how our
barriers work, so it looks OK to me.

Reviewed-by: Michael Ellerman <mpe@ellerman.id.au> (powerpc)

cheers

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Boqun Feng]

On Fri, Oct 08, 2021 at 04:30:37PM +1100, Michael Ellerman wrote:
> Boqun Feng <boqun.feng@gmail.com> writes:
> > (Add linux-arch in Cc list)
> >
> > Architecture maintainers, this patch is about strengthening our memory
> > model a little bit, your inputs (confirmation, ack/nack, etc.) are
> > appreciated.
> 
> Hi Boqun,
> 
> I don't feel like I'm really qualified to give an ack here, you and the
> other memory model folk know this stuff much better than me.
> 
> But I have reviewed it and it matches my understanding of how our
> barriers work, so it looks OK to me.
> 
> Reviewed-by: Michael Ellerman <mpe@ellerman.id.au> (powerpc)
> 

Thanks!

Regards,
Boqun

> cheers

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Palmer Dabbelt]

On Thu, 07 Oct 2021 23:54:23 PDT (-0700), boqun.feng@gmail.com wrote:
> On Fri, Oct 08, 2021 at 04:30:37PM +1100, Michael Ellerman wrote:
>> Boqun Feng <boqun.feng@gmail.com> writes:
>> > (Add linux-arch in Cc list)
>> >
>> > Architecture maintainers, this patch is about strengthening our memory
>> > model a little bit, your inputs (confirmation, ack/nack, etc.) are
>> > appreciated.
>>
>> Hi Boqun,
>>
>> I don't feel like I'm really qualified to give an ack here, you and the
>> other memory model folk know this stuff much better than me.
>>
>> But I have reviewed it and it matches my understanding of how our
>> barriers work, so it looks OK to me.
>>
>> Reviewed-by: Michael Ellerman <mpe@ellerman.id.au> (powerpc)

I'm basically in the same spot.  I think I said something to that effect 
somewhere in the thread, but I'm not sure if it got picked up so

Acked-by: Palmer Dabbelt <palmerdabbelt@google.com> (RISC-V)

(I don't feel comfortable reviewing it so I'm acking it, not sure if I'm 
just backwards about what all this means though ;)).

IIUC this change will mean the RISC-V port is broken, but I'm happy to 
fix it.  Were you guys trying to target this for 5.16?

Re: [PATCH] tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

[Boqun Feng]

On Fri, Oct 08, 2021 at 09:32:58AM -0700, Palmer Dabbelt wrote:
> On Thu, 07 Oct 2021 23:54:23 PDT (-0700), boqun.feng@gmail.com wrote:
> > On Fri, Oct 08, 2021 at 04:30:37PM +1100, Michael Ellerman wrote:
> > > Boqun Feng <boqun.feng@gmail.com> writes:
> > > > (Add linux-arch in Cc list)
> > > >
> > > > Architecture maintainers, this patch is about strengthening our memory
> > > > model a little bit, your inputs (confirmation, ack/nack, etc.) are
> > > > appreciated.
> > > 
> > > Hi Boqun,
> > > 
> > > I don't feel like I'm really qualified to give an ack here, you and the
> > > other memory model folk know this stuff much better than me.
> > > 
> > > But I have reviewed it and it matches my understanding of how our
> > > barriers work, so it looks OK to me.
> > > 
> > > Reviewed-by: Michael Ellerman <mpe@ellerman.id.au> (powerpc)
> 
> I'm basically in the same spot.  I think I said something to that effect
> somewhere in the thread, but I'm not sure if it got picked up so
> 
> Acked-by: Palmer Dabbelt <palmerdabbelt@google.com> (RISC-V)
> 

Thanks!

> (I don't feel comfortable reviewing it so I'm acking it, not sure if I'm
> just backwards about what all this means though ;)).
> 
> IIUC this change will mean the RISC-V port is broken, but I'm happy to fix

No, the RISC-V port is not broken, this patch only strengthen the
unlock(A)+lock(B) to TSO ordering, as per the previous discussion:

	https://lore.kernel.org/lkml/5412ab37-2979-5717-4951-6a61366df0f2@nvidia.com/

RISC-V's current lock implementation is fine, and it's still OK if
RISC-V still to queued spinlock, since as Dan said in that email thread,
the following code still provides TSO ordering:

	FENCE RW, W
	store A
	ll/sc B
	FENCE R, RW

Regards,
Boqun

> it.  Were you guys trying to target this for 5.16?