Merge tag 'renesas-r9a07g043-dt-binding-defs-tag2' into HEAD

[linux-2.6-microblaze.git] / tools / memory-model / linux-kernel.bell

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 7965133..5be86b1 100644 (file)
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -24,6 +24,7 @@ instructions RMW[{'once,'acquire,'release}]
 enum Barriers = 'wmb (*smp_wmb*) ||
                'rmb (*smp_rmb*) ||
                'mb (*smp_mb*) ||
+               'barrier (*barrier*) ||
                'rcu-lock (*rcu_read_lock*)  ||
                'rcu-unlock (*rcu_read_unlock*) ||
                'sync-rcu (*synchronize_rcu*) ||
@@ -33,8 +34,14 @@ enum Barriers = 'wmb (*smp_wmb*) ||
                'after-unlock-lock (*smp_mb__after_unlock_lock*)
 instructions F[Barriers]
 
+(* SRCU *)
+enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
+instructions SRCU[SRCU]
+(* All srcu events *)
+let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu
+
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
-let matched = let rec
+let rcu-rscs = let rec
            unmatched-locks = Rcu-lock \ domain(matched)
        and unmatched-unlocks = Rcu-unlock \ range(matched)
        and unmatched = unmatched-locks | unmatched-unlocks
@@ -46,8 +53,32 @@ let matched = let rec
        in matched
 
 (* Validate nesting *)
-flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
-flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
+flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
+flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
+
+(* 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
+
+(* Validate nesting *)
+flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
+flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
+
+(* Check for use of synchronize_srcu() inside an RCU critical section *)
+flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
+
+(* Validate SRCU dynamic match *)
+flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
 
-(* Outermost level of nesting only *)
-let crit = matched \ (po^-1 ; matched ; po^-1)
+(* Compute marked and plain memory accesses *)
+let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
+               LKR | LKW | UL | LF | RL | RU
+let Plain = M \ Marked