[v3,1/5] tools/memory-model: Add an exception for limitations on _unless() family
diff mbox series

Message ID 20200227004049.6853-2-boqun.feng@gmail.com
State In Next
Commit 54f1f5dda73af07aea234b29431edcf5cc142011
Headers show
Series
  • Documentation/locking/atomic: Add litmus tests for atomic APIs
Related show

Commit Message

Boqun Feng Feb. 27, 2020, 12:40 a.m. UTC
According to Luc, atomic_add_unless() is directly provided by herd7,
therefore it can be used in litmus tests. So change the limitation
section in README to unlimit the use of atomic_add_unless().

Cc: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
 tools/memory-model/README | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

Comments

Alan Stern Feb. 27, 2020, 4:32 p.m. UTC | #1
On Thu, 27 Feb 2020, Boqun Feng wrote:

> According to Luc, atomic_add_unless() is directly provided by herd7,
> therefore it can be used in litmus tests. So change the limitation
> section in README to unlimit the use of atomic_add_unless().

Is this really true?  Why does herd treat atomic_add_unless() different
from all the other atomic RMS ops?  All the other ones we support do
have entries in linux-kernel.def.

Alan

PS: It seems strange to support atomic_add_unless but not 
atomic_long_add_unless.  The difference between the two is trivial.

> 
> Cc: Luc Maranget <luc.maranget@inria.fr>
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  tools/memory-model/README | 10 +++++++---
>  1 file changed, 7 insertions(+), 3 deletions(-)
> 
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index fc07b52f2028..409211b1c544 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 provided 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 Maranget Feb. 27, 2020, 4:49 p.m. UTC | #2
> On Thu, 27 Feb 2020, Boqun Feng wrote:
> 
> > According to Luc, atomic_add_unless() is directly provided by herd7,
> > therefore it can be used in litmus tests. So change the limitation
> > section in README to unlimit the use of atomic_add_unless().
> 
> Is this really true?  Why does herd treat atomic_add_unless() different
> from all the other atomic RMS ops?  All the other ones we support do
> have entries in linux-kernel.def.

I think this to be true :)

As far as I remember atomic_add_unless is quite different fron other atomic
RMW ops and called for a specific all-OCaml implementation, without an
entry in linux-kernel.def. As to  atomic_long_add_unless, I was not aware
of its existence.

--Luc

> 
> Alan
> 
> PS: It seems strange to support atomic_add_unless but not 
> atomic_long_add_unless.  The difference between the two is trivial.
> 
> > 
> > Cc: Luc Maranget <luc.maranget@inria.fr>
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > ---
> >  tools/memory-model/README | 10 +++++++---
> >  1 file changed, 7 insertions(+), 3 deletions(-)
> > 
> > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > index fc07b52f2028..409211b1c544 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 provided 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
> >
Andrea Parri Feb. 27, 2020, 5:52 p.m. UTC | #3
On Thu, Feb 27, 2020 at 08:40:45AM +0800, Boqun Feng wrote:
> According to Luc, atomic_add_unless() is directly provided by herd7,
> therefore it can be used in litmus tests. So change the limitation
> section in README to unlimit the use of atomic_add_unless().
> 
> Cc: Luc Maranget <luc.maranget@inria.fr>
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
>  tools/memory-model/README | 10 +++++++---
>  1 file changed, 7 insertions(+), 3 deletions(-)
> 
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index fc07b52f2028..409211b1c544 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 provided directly by herd7 (so no corresponding
> +		definition in linux-kernel.def). atomic_add_unless() is

Nit: Two spaces after period?

  Andrea


> +		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
> -- 
> 2.25.0
>
Alan Stern Feb. 27, 2020, 6:16 p.m. UTC | #4
On Thu, 27 Feb 2020, Luc Maranget wrote:

> > On Thu, 27 Feb 2020, Boqun Feng wrote:
> > 
> > > According to Luc, atomic_add_unless() is directly provided by herd7,
> > > therefore it can be used in litmus tests. So change the limitation
> > > section in README to unlimit the use of atomic_add_unless().
> > 
> > Is this really true?  Why does herd treat atomic_add_unless() different
> > from all the other atomic RMS ops?  All the other ones we support do
> > have entries in linux-kernel.def.
> 
> I think this to be true :)
> 
> As far as I remember atomic_add_unless is quite different fron other atomic
> RMW ops and called for a specific all-OCaml implementation, without an
> entry in linux-kernel.def. As to  atomic_long_add_unless, I was not aware
> of its existence.

Can you explain what is so different about atomic_add_unless?

Alan

Patch
diff mbox series

diff --git a/tools/memory-model/README b/tools/memory-model/README
index fc07b52f2028..409211b1c544 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 provided 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