lkml.org 
[lkml]   [2020]   [Feb]   [25]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
Patch in this message
/
From
Subject[PATCH] tools/memory-model: Remove lock-final checking in lock.cat
Date
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
\
 
 \ /
  Last update: 2020-02-26 04:23    [W:0.074 / U:0.648 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site