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@xxxxxxxxx>
> > ---
> > 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
>
