diff options
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 17 | ||||
| -rw-r--r-- | tools/memory-model/linux-kernel.def | 6 | ||||
| -rw-r--r-- | tools/memory-model/lock.cat | 6 |
3 files changed, 12 insertions, 17 deletions
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index b92fdf7f6eeb..ce068700939c 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -58,20 +58,13 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rcu-lock flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) -let srcu-rscs = let rec - unmatched-locks = Srcu-lock \ domain(matched) - and unmatched-unlocks = Srcu-unlock \ range(matched) - and unmatched = unmatched-locks | unmatched-unlocks - and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc - and unmatched-locks-to-unlocks = - ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc - and matched = matched | (unmatched-locks-to-unlocks \ - (unmatched-po ; unmatched-po)) - in matched +let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)* +let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc (* Validate nesting *) flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock +flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches (* Check for use of synchronize_srcu() inside an RCU critical section *) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep @@ -81,11 +74,11 @@ flag ~empty different-values(srcu-rscs) as srcu-bad-value-match (* Compute marked and plain memory accesses *) let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | - LKR | LKW | UL | LF | RL | RU + LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock let Plain = M \ Marked (* Redefine dependencies to include those carried through plain accesses *) -let carry-dep = (data ; rfi)* +let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* let addr = carry-dep ; addr let ctrl = carry-dep ; ctrl let data = carry-dep ; data diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index a6b6fbc9d0b2..88a39601f525 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -50,8 +50,10 @@ synchronize_rcu() { __fence{sync-rcu}; } synchronize_rcu_expedited() { __fence{sync-rcu}; } // SRCU -srcu_read_lock(X) __srcu{srcu-lock}(X) -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); } +srcu_read_lock(X) __load{srcu-lock}(*X) +srcu_read_unlock(X,Y) { __store{srcu-unlock}(*X,Y); } +srcu_down_read(X) __load{srcu-lock}(*X) +srcu_up_read(X,Y) { __store{srcu-unlock}(*X,Y); } synchronize_srcu(X) { __srcu{sync-srcu}(X); } synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); } diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 6b52f365d73a..53b5a492739d 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -36,9 +36,9 @@ let RU = try RU with emptyset (* Treat RL as a kind of LF: a read with no ordering properties *) let LF = LF | RL -(* There should be no ordinary R or W accesses to spinlocks *) -let ALL-LOCKS = LKR | LKW | UL | LF | RU -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *) +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses (* Link Lock-Reads to their RMW-partner Lock-Writes *) let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) |