diff options
| author | Alan Stern <stern@rowland.harvard.edu> | 2019-04-22 12:17:58 -0400 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@linux.ibm.com> | 2019-05-28 08:18:21 -0700 |
| commit | d1a84ab190137cc2a980b6979b1f2790d51b2d87 (patch) | |
| tree | 083219522d9a0f94d7d092a794db8483fb961013 /tools/memory-model/linux-kernel.bell | |
| parent | 4494dd58fbb477e54c129c1d8ef477aad433eba0 (diff) | |
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 <stern@rowland.harvard.edu>
Reviewed-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Diffstat (limited to 'tools/memory-model/linux-kernel.bell')
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 5 |
1 files changed, 5 insertions, 0 deletions
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 |