Skip to content

Commit e8adbac

Browse files
andrea-parripaulmckrcu
andrea-parri
authored and
paulmckrcu
committed
tools/memory-model: Document herd7 (abstract) representation
The Linux-kernel memory model (LKMM) source code and the herd7 tool are closely linked in that the latter is responsible for (pre)processing each C-like macro of a litmus test, and for providing the LKMM with a set of events, or "representation", corresponding to the given macro. This commit therefore provides herd-representation.txt to document the representations of the concurrency macros, following their "classification" in Documentation/atomic_t.txt. Link: https://lore.kernel.org/all/ZnFZPJlILp5B9scN@andrea/ Suggested-by: Hernan Ponce de Leon <[email protected]> Signed-off-by: Andrea Parri <[email protected]> Reviewed-by: Boqun Feng <[email protected]> Reviewed-by: Hernan Ponce de Leon <[email protected]> Signed-off-by: Paul E. McKenney <[email protected]>
1 parent 8400291 commit e8adbac

File tree

2 files changed

+116
-1
lines changed

2 files changed

+116
-1
lines changed

‎tools/memory-model/Documentation/README

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of
3333

3434
o You are familiar with Linux-kernel concurrency and the use
3535
of LKMM, and would like to learn about LKMM's requirements,
36-
rationale, and implementation: explanation.txt
36+
rationale, and implementation: explanation.txt and
37+
herd-representation.txt
3738

3839
o You are interested in the publications related to LKMM, including
3940
hardware manuals, academic literature, standards-committee
@@ -61,6 +62,10 @@ control-dependencies.txt
6162
explanation.txt
6263
Detailed description of the memory model.
6364

65+
herd-representation.txt
66+
The (abstract) representation of the Linux-kernel concurrency
67+
primitives in terms of events.
68+
6469
litmus-tests.txt
6570
The format, features, capabilities, and limitations of the litmus
6671
tests that LKMM can evaluate.

‎tools/memory-model/Documentation/herd-representation.txt

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
#
2+
# Legend:
3+
# R, a Load event
4+
# W, a Store event
5+
# F, a Fence event
6+
# LKR, a Lock-Read event
7+
# LKW, a Lock-Write event
8+
# UL, an Unlock event
9+
# LF, a Lock-Fail event
10+
# RL, a Read-Locked event
11+
# RU, a Read-Unlocked event
12+
# R*, a Load event included in RMW
13+
# W*, a Store event included in RMW
14+
# SRCU, a Sleepable-Read-Copy-Update event
15+
#
16+
# po, a Program-Order link
17+
# rmw, a Read-Modify-Write link - every rmw link is a po link
18+
#
19+
# By convention, a blank line in a cell means "same as the preceding line".
20+
#
21+
# Disclaimer. The table includes representations of "add" and "and" operations;
22+
# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
23+
# "andnot" operations are omitted.
24+
#
25+
------------------------------------------------------------------------------
26+
| C macro | Events |
27+
------------------------------------------------------------------------------
28+
| Non-RMW ops | |
29+
------------------------------------------------------------------------------
30+
| READ_ONCE | R[once] |
31+
| atomic_read | |
32+
| WRITE_ONCE | W[once] |
33+
| atomic_set | |
34+
| smp_load_acquire | R[acquire] |
35+
| atomic_read_acquire | |
36+
| smp_store_release | W[release] |
37+
| atomic_set_release | |
38+
| smp_store_mb | W[once] ->po F[mb] |
39+
| smp_mb | F[mb] |
40+
| smp_rmb | F[rmb] |
41+
| smp_wmb | F[wmb] |
42+
| smp_mb__before_atomic | F[before-atomic] |
43+
| smp_mb__after_atomic | F[after-atomic] |
44+
| spin_unlock | UL |
45+
| spin_is_locked | On success: RL |
46+
| | On failure: RU |
47+
| smp_mb__after_spinlock | F[after-spinlock] |
48+
| smp_mb__after_unlock_lock | F[after-unlock-lock] |
49+
| rcu_read_lock | F[rcu-lock] |
50+
| rcu_read_unlock | F[rcu-unlock] |
51+
| synchronize_rcu | F[sync-rcu] |
52+
| rcu_dereference | R[once] |
53+
| rcu_assign_pointer | W[release] |
54+
| srcu_read_lock | R[srcu-lock] |
55+
| srcu_down_read | |
56+
| srcu_read_unlock | W[srcu-unlock] |
57+
| srcu_up_read | |
58+
| synchronize_srcu | SRCU[sync-srcu] |
59+
| smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] |
60+
------------------------------------------------------------------------------
61+
| RMW ops w/o return value | |
62+
------------------------------------------------------------------------------
63+
| atomic_add | R*[noreturn] ->rmw W*[once] |
64+
| atomic_and | |
65+
| spin_lock | LKR ->po LKW |
66+
------------------------------------------------------------------------------
67+
| RMW ops w/ return value | |
68+
------------------------------------------------------------------------------
69+
| atomic_add_return | F[mb] ->po R*[once] |
70+
| | ->rmw W*[once] ->po F[mb] |
71+
| atomic_fetch_add | |
72+
| atomic_fetch_and | |
73+
| atomic_xchg | |
74+
| xchg | |
75+
| atomic_add_negative | |
76+
| atomic_add_return_relaxed | R*[once] ->rmw W*[once] |
77+
| atomic_fetch_add_relaxed | |
78+
| atomic_fetch_and_relaxed | |
79+
| atomic_xchg_relaxed | |
80+
| xchg_relaxed | |
81+
| atomic_add_negative_relaxed | |
82+
| atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
83+
| atomic_fetch_add_acquire | |
84+
| atomic_fetch_and_acquire | |
85+
| atomic_xchg_acquire | |
86+
| xchg_acquire | |
87+
| atomic_add_negative_acquire | |
88+
| atomic_add_return_release | R*[once] ->rmw W*[release] |
89+
| atomic_fetch_add_release | |
90+
| atomic_fetch_and_release | |
91+
| atomic_xchg_release | |
92+
| xchg_release | |
93+
| atomic_add_negative_release | |
94+
------------------------------------------------------------------------------
95+
| Conditional RMW ops | |
96+
------------------------------------------------------------------------------
97+
| atomic_cmpxchg | On success: F[mb] ->po R*[once] |
98+
| | ->rmw W*[once] ->po F[mb] |
99+
| | On failure: R*[once] |
100+
| cmpxchg | |
101+
| atomic_add_unless | |
102+
| atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
103+
| | On failure: R*[once] |
104+
| atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
105+
| | On failure: R*[once] |
106+
| atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
107+
| | On failure: R*[once] |
108+
| spin_trylock | On success: LKR ->po LKW |
109+
| | On failure: LF |
110+
------------------------------------------------------------------------------

0 commit comments

Comments
 (0)