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

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(-)

tools/memory-model/lock.cat +0 -0

index 6b52f365d73a..827a3646607c 100644

Quoted 5 lines · 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.

I don't understand this description. Why do you say that the normal-access checking is stronger than the lock-final check?

Quoted 13 lines

Signed-off-by Boqun Feng <[email protected]>

---
 tools/memory-model/lock.cat | 3 ---
 1 file changed, 3 deletions(-)

tools/memory-model/lock.cat +0 -0

index 6b52f365d73a..827a3646607c 100644
@@ -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
 

tools/memory-model/lock.cat flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR · line 59

Quoted 6 lines

tools/memory-model/lock.cat +0 -3

-(* 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