[PATCH] tools/memory-model: Remove lock-final checking in lock.cat

[PATCH] tools/memory-model: Remove lock-final checking in lock.cat

[Boqun Feng]

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

Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat

[Alan Stern]

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

Re: [PATCH] tools/memory-model: Remove lock-final checking in lock.cat

[Boqun Feng]

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
>