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?
C test
{
spinlock_t s;
}
...
exists (s=0)
Alan
