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 def9131..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*) ||
@@ -76,3 +77,8 @@ 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
+
+(* 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