From d1a84ab190137cc2a980b6979b1f2790d51b2d87 Mon Sep 17 00:00:00 2001 From: Alan Stern Date: Mon, 22 Apr 2019 12:17:58 -0400 Subject: tools/memory-model: Add definitions of plain and marked accesses This patch adds definitions for marked and plain accesses to the Linux-Kernel Memory Model. It also modifies the definitions of the existing parts of the model (including the cumul-fence, prop, hb, pb, and rb relations) so as to make them apply only to marked accesses. Signed-off-by: Alan Stern Reviewed-by: Andrea Parri Signed-off-by: Paul E. McKenney --- tools/memory-model/linux-kernel.bell | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'tools/memory-model/linux-kernel.bell') diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index def9131d3d8e..b60eb5a01053 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -76,3 +76,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 -- cgit v1.2.3