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 <[email protected]>
---
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
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 <[email protected]>
> ---
> 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
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 <[email protected]>
> > ---
> > 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
>