* [PATCH] tools/memory-model: Remove lock-final checking in lock.cat
@ 2020-02-26 3:21 Boqun Feng
2020-02-26 3:21 ` Boqun Feng
2020-02-26 14:58 ` Alan Stern
0 siblings, 2 replies; 5+ messages in thread
From: Boqun Feng @ 2020-02-26 3:21 UTC (permalink / raw)
To: linux-kernel, rcu
Cc: Boqun Feng, Alan Stern, Andrea Parri, Will Deacon, Peter Zijlstra,
Nicholas Piggin, David Howells, Jade Alglave, Luc Maranget,
Paul E. McKenney, Akira Yokosawa, Daniel Lustig, linux-arch
In commit 30b795df11a1 ("tools/memory-model: Improve mixed-access
checking in lock.cat"), we have added the checking to disallow any
normal memory access to lock variables, and this checking is stronger
than lock-final. So remove the lock-final checking as it's unnecessary
now.
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
tools/memory-model/lock.cat | 3 ---
1 file changed, 3 deletions(-)
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index 6b52f365d73a..827a3646607c 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -54,9 +54,6 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
*)
empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
-(* The final value of a spinlock should not be tested *)
-flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
-
(*
* Put lock operations in their appropriate classes, but leave UL out of W
* until after the co relation has been generated.
--
2.25.0
^ permalink raw reply related [flat|nested] 5+ messages in thread* [PATCH] tools/memory-model: Remove lock-final checking in lock.cat
2020-02-26 3:21 [PATCH] tools/memory-model: Remove lock-final checking in lock.cat Boqun Feng
@ 2020-02-26 3:21 ` Boqun Feng
2020-02-26 14:58 ` Alan Stern
1 sibling, 0 replies; 5+ messages in thread
From: Boqun Feng @ 2020-02-26 3:21 UTC (permalink / raw)
To: linux-kernel, rcu
Cc: Boqun Feng, Alan Stern, Andrea Parri, Will Deacon, Peter Zijlstra,
Nicholas Piggin, David Howells, Jade Alglave, Luc Maranget,
Paul E. McKenney, Akira Yokosawa, Daniel Lustig, linux-arch
In commit 30b795df11a1 ("tools/memory-model: Improve mixed-access
checking in lock.cat"), we have added the checking to disallow any
normal memory access to lock variables, and this checking is stronger
than lock-final. So remove the lock-final checking as it's unnecessary
now.
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
---
tools/memory-model/lock.cat | 3 ---
1 file changed, 3 deletions(-)
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index 6b52f365d73a..827a3646607c 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -54,9 +54,6 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
*)
empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
-(* The final value of a spinlock should not be tested *)
-flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
-
(*
* Put lock operations in their appropriate classes, but leave UL out of W
* until after the co relation has been generated.
--
2.25.0
^ permalink raw reply related [flat|nested] 5+ messages in thread* Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat
2020-02-26 3:21 [PATCH] tools/memory-model: Remove lock-final checking in lock.cat Boqun Feng
2020-02-26 3:21 ` Boqun Feng
@ 2020-02-26 14:58 ` Alan Stern
2020-02-26 23:59 ` Boqun Feng
1 sibling, 1 reply; 5+ messages in thread
From: Alan Stern @ 2020-02-26 14:58 UTC (permalink / raw)
To: Boqun Feng
Cc: linux-kernel, rcu, Andrea Parri, Will Deacon, Peter Zijlstra,
Nicholas Piggin, David Howells, Jade Alglave, Luc Maranget,
Paul E. McKenney, Akira Yokosawa, Daniel Lustig, linux-arch
On Wed, 26 Feb 2020, Boqun Feng wrote:
> In commit 30b795df11a1 ("tools/memory-model: Improve mixed-access
> checking in lock.cat"), we have added the checking to disallow any
> normal memory access to lock variables, and this checking is stronger
> than lock-final. So remove the lock-final checking as it's unnecessary
> now.
I don't understand this description. Why do you say that the
normal-access checking is stronger than the lock-final check?
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> ---
> tools/memory-model/lock.cat | 3 ---
> 1 file changed, 3 deletions(-)
>
> diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> index 6b52f365d73a..827a3646607c 100644
> --- a/tools/memory-model/lock.cat
> +++ b/tools/memory-model/lock.cat
> @@ -54,9 +54,6 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
> *)
> empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
>
> -(* The final value of a spinlock should not be tested *)
> -flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> -
> (*
> * Put lock operations in their appropriate classes, but leave UL out of W
> * until after the co relation has been generated.
With this check removed, what will prevent people from writing litmus
tests like this?
C test
{
spinlock_t s;
}
...
exists (s=0)
Alan
^ permalink raw reply [flat|nested] 5+ messages in thread* Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat
2020-02-26 14:58 ` Alan Stern
@ 2020-02-26 23:59 ` Boqun Feng
2020-02-26 23:59 ` Boqun Feng
0 siblings, 1 reply; 5+ messages in thread
From: Boqun Feng @ 2020-02-26 23:59 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, rcu, Andrea Parri, Will Deacon, Peter Zijlstra,
Nicholas Piggin, David Howells, Jade Alglave, Luc Maranget,
Paul E. McKenney, Akira Yokosawa, Daniel Lustig, linux-arch
On Wed, Feb 26, 2020 at 09:58:12AM -0500, Alan Stern wrote:
> On Wed, 26 Feb 2020, Boqun Feng wrote:
>
> > In commit 30b795df11a1 ("tools/memory-model: Improve mixed-access
> > checking in lock.cat"), we have added the checking to disallow any
> > normal memory access to lock variables, and this checking is stronger
> > than lock-final. So remove the lock-final checking as it's unnecessary
> > now.
>
> I don't understand this description. Why do you say that the
> normal-access checking is stronger than the lock-final check?
>
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > ---
> > tools/memory-model/lock.cat | 3 ---
> > 1 file changed, 3 deletions(-)
> >
> > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> > index 6b52f365d73a..827a3646607c 100644
> > --- a/tools/memory-model/lock.cat
> > +++ b/tools/memory-model/lock.cat
> > @@ -54,9 +54,6 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
> > *)
> > empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
> >
> > -(* The final value of a spinlock should not be tested *)
> > -flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> > -
> > (*
> > * Put lock operations in their appropriate classes, but leave UL out of W
> > * until after the co relation has been generated.
>
> With this check removed, what will prevent people from writing litmus
> tests like this?
>
You are right, one thing I was missing is although FW is a subset of M,
however FW & IW is not empty. Thanks! I will drop this.
Regards,
Boqun
> C test
>
> {
> spinlock_t s;
> }
>
> ...
>
> exists (s=0)
>
> Alan
>
^ permalink raw reply [flat|nested] 5+ messages in thread* Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat
2020-02-26 23:59 ` Boqun Feng
@ 2020-02-26 23:59 ` Boqun Feng
0 siblings, 0 replies; 5+ messages in thread
From: Boqun Feng @ 2020-02-26 23:59 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, rcu, Andrea Parri, Will Deacon, Peter Zijlstra,
Nicholas Piggin, David Howells, Jade Alglave, Luc Maranget,
Paul E. McKenney, Akira Yokosawa, Daniel Lustig, linux-arch
On Wed, Feb 26, 2020 at 09:58:12AM -0500, Alan Stern wrote:
> On Wed, 26 Feb 2020, Boqun Feng wrote:
>
> > In commit 30b795df11a1 ("tools/memory-model: Improve mixed-access
> > checking in lock.cat"), we have added the checking to disallow any
> > normal memory access to lock variables, and this checking is stronger
> > than lock-final. So remove the lock-final checking as it's unnecessary
> > now.
>
> I don't understand this description. Why do you say that the
> normal-access checking is stronger than the lock-final check?
>
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > ---
> > tools/memory-model/lock.cat | 3 ---
> > 1 file changed, 3 deletions(-)
> >
> > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> > index 6b52f365d73a..827a3646607c 100644
> > --- a/tools/memory-model/lock.cat
> > +++ b/tools/memory-model/lock.cat
> > @@ -54,9 +54,6 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
> > *)
> > empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
> >
> > -(* The final value of a spinlock should not be tested *)
> > -flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> > -
> > (*
> > * Put lock operations in their appropriate classes, but leave UL out of W
> > * until after the co relation has been generated.
>
> With this check removed, what will prevent people from writing litmus
> tests like this?
>
You are right, one thing I was missing is although FW is a subset of M,
however FW & IW is not empty. Thanks! I will drop this.
Regards,
Boqun
> C test
>
> {
> spinlock_t s;
> }
>
> ...
>
> exists (s=0)
>
> Alan
>
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2020-02-26 23:59 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2020-02-26 3:21 [PATCH] tools/memory-model: Remove lock-final checking in lock.cat Boqun Feng
2020-02-26 3:21 ` Boqun Feng
2020-02-26 14:58 ` Alan Stern
2020-02-26 23:59 ` Boqun Feng
2020-02-26 23:59 ` Boqun Feng
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox