diff options
| author | Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> | 2024-11-05 17:48:58 +0100 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2025-02-25 10:17:39 -0800 |
| commit | dcc5197839f22655951056f399061872adfdb0b9 (patch) | |
| tree | 5d80596a076d2ae57667a43e6b95c349f97758da /tools/memory-model/Documentation | |
| parent | fafa180683591f5f917bfa68e95aae463afc852a (diff) | |
| download | linux-dcc5197839f22655951056f399061872adfdb0b9.tar.gz linux-dcc5197839f22655951056f399061872adfdb0b9.tar.bz2 linux-dcc5197839f22655951056f399061872adfdb0b9.zip | |
tools/memory-model: Distinguish between syntactic and semantic tags
Not all annotated accesses provide the semantics their syntactic tags
would imply. For example, an 'acquire tag on a write does not imply that
the write is finally in the Acquire set and provides acquire ordering.
To distinguish in those cases between the syntactic tags and actual
sets, we capitalize the former, so 'ACQUIRE tags may be present on both
reads and writes, but only reads will appear in the Acquire set.
For tags where the two concepts are the same we do not use specific
capitalization to make this distinction.
Reported-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Tested-by: Akira Yokosawa <akiyks@gmail.com> # herdtools7.7.58
Diffstat (limited to 'tools/memory-model/Documentation')
| -rw-r--r-- | tools/memory-model/Documentation/herd-representation.txt | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt index 7ae1ff3d3769..4e19b4f2a476 100644 --- a/tools/memory-model/Documentation/herd-representation.txt +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -21,7 +21,7 @@ # Note that the syntactic representation does not always match the sets and # relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and # lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw -# link, and W[acquire] are not included in the Acquire set. +# link, and W[ACQUIRE] are not included in the Acquire set. # # Disclaimer. The table includes representations of "add" and "and" operations; # corresponding/identical representations of "sub", "inc", "dec" and "or", "xor", @@ -32,16 +32,16 @@ ------------------------------------------------------------------------------ | Non-RMW ops | | ------------------------------------------------------------------------------ - | READ_ONCE | R[once] | + | READ_ONCE | R[ONCE] | | atomic_read | | - | WRITE_ONCE | W[once] | + | WRITE_ONCE | W[ONCE] | | atomic_set | | - | smp_load_acquire | R[acquire] | + | smp_load_acquire | R[ACQUIRE] | | atomic_read_acquire | | - | smp_store_release | W[release] | + | smp_store_release | W[RELEASE] | | atomic_set_release | | - | smp_store_mb | W[once] ->po F[mb] | - | smp_mb | F[mb] | + | smp_store_mb | W[ONCE] ->po F[MB] | + | smp_mb | F[MB] | | smp_rmb | F[rmb] | | smp_wmb | F[wmb] | | smp_mb__before_atomic | F[before-atomic] | @@ -54,8 +54,8 @@ | rcu_read_lock | F[rcu-lock] | | rcu_read_unlock | F[rcu-unlock] | | synchronize_rcu | F[sync-rcu] | - | rcu_dereference | R[once] | - | rcu_assign_pointer | W[release] | + | rcu_dereference | R[ONCE] | + | rcu_assign_pointer | W[RELEASE] | | srcu_read_lock | R[srcu-lock] | | srcu_down_read | | | srcu_read_unlock | W[srcu-unlock] | @@ -65,31 +65,31 @@ ------------------------------------------------------------------------------ | RMW ops w/o return value | | ------------------------------------------------------------------------------ - | atomic_add | R*[noreturn] ->rmw W*[noreturn] | + | atomic_add | R*[NORETURN] ->rmw W*[NORETURN] | | atomic_and | | | spin_lock | LKR ->po LKW | ------------------------------------------------------------------------------ | RMW ops w/ return value | | ------------------------------------------------------------------------------ - | atomic_add_return | R*[mb] ->rmw W*[mb] | + | atomic_add_return | R*[MB] ->rmw W*[MB] | | atomic_fetch_add | | | atomic_fetch_and | | | atomic_xchg | | | xchg | | | atomic_add_negative | | - | atomic_add_return_relaxed | R*[once] ->rmw W*[once] | + | atomic_add_return_relaxed | R*[ONCE] ->rmw W*[ONCE] | | atomic_fetch_add_relaxed | | | atomic_fetch_and_relaxed | | | atomic_xchg_relaxed | | | xchg_relaxed | | | atomic_add_negative_relaxed | | - | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] | + | atomic_add_return_acquire | R*[ACQUIRE] ->rmw W*[ACQUIRE] | | atomic_fetch_add_acquire | | | atomic_fetch_and_acquire | | | atomic_xchg_acquire | | | xchg_acquire | | | atomic_add_negative_acquire | | - | atomic_add_return_release | R*[release] ->rmw W*[release] | + | atomic_add_return_release | R*[RELEASE] ->rmw W*[RELEASE] | | atomic_fetch_add_release | | | atomic_fetch_and_release | | | atomic_xchg_release | | @@ -98,16 +98,16 @@ ------------------------------------------------------------------------------ | Conditional RMW ops | | ------------------------------------------------------------------------------ - | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] | - | | On failure: R*[mb] | + | atomic_cmpxchg | On success: R*[MB] ->rmw W*[MB] | + | | On failure: R*[MB] | | cmpxchg | | | atomic_add_unless | | - | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] | - | | On failure: R*[once] | - | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[acquire] | - | | On failure: R*[acquire] | - | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] | - | | On failure: R*[release] | + | atomic_cmpxchg_relaxed | On success: R*[ONCE] ->rmw W*[ONCE] | + | | On failure: R*[ONCE] | + | atomic_cmpxchg_acquire | On success: R*[ACQUIRE] ->rmw W*[ACQUIRE] | + | | On failure: R*[ACQUIRE] | + | atomic_cmpxchg_release | On success: R*[RELEASE] ->rmw W*[RELEASE] | + | | On failure: R*[RELEASE] | | spin_trylock | On success: LKR ->po LKW | | | On failure: LF | ------------------------------------------------------------------------------ |