mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/next/linux-next.git
synced 2024-12-28 16:52:18 +00:00
tools/memory-model: Switch to softcoded herd7 tags
A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7 behavior of simply ignoring any softcoded tags in the .def and .bell files. We port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg and reporting an error if the LKMM is used without this switch. To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic RMW which do not return a value and define atomic_add_unless with an Mb tag in linux-kernel.def. We update the herd-representation.txt accordingly and clarify some of the resulting combinations. Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> Tested-by: Boqun Feng <boqun.feng@gmail.com>
This commit is contained in:
Jonas Oberhauser
Paul E. McKenney
parent
a73d299a22
commit
55ea0b074d
@ -18,6 +18,11 @@
|
||||
#
|
||||
# By convention, a blank line in a cell means "same as the preceding line".
|
||||
#
|
||||
# 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.
|
||||
#
|
||||
# Disclaimer. The table includes representations of "add" and "and" operations;
|
||||
# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
|
||||
# "andnot" operations are omitted.
|
||||
@ -60,14 +65,13 @@
|
||||
------------------------------------------------------------------------------
|
||||
| RMW ops w/o return value | |
|
||||
------------------------------------------------------------------------------
|
||||
| atomic_add | R*[noreturn] ->rmw W*[once] |
|
||||
| atomic_add | R*[noreturn] ->rmw W*[noreturn] |
|
||||
| atomic_and | |
|
||||
| spin_lock | LKR ->po LKW |
|
||||
------------------------------------------------------------------------------
|
||||
| RMW ops w/ return value | |
|
||||
------------------------------------------------------------------------------
|
||||
| atomic_add_return | F[mb] ->po R*[once] |
|
||||
| | ->rmw W*[once] ->po F[mb] |
|
||||
| atomic_add_return | R*[mb] ->rmw W*[mb] |
|
||||
| atomic_fetch_add | |
|
||||
| atomic_fetch_and | |
|
||||
| atomic_xchg | |
|
||||
@ -79,13 +83,13 @@
|
||||
| atomic_xchg_relaxed | |
|
||||
| xchg_relaxed | |
|
||||
| atomic_add_negative_relaxed | |
|
||||
| atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
|
||||
| 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*[once] ->rmw W*[release] |
|
||||
| atomic_add_return_release | R*[release] ->rmw W*[release] |
|
||||
| atomic_fetch_add_release | |
|
||||
| atomic_fetch_and_release | |
|
||||
| atomic_xchg_release | |
|
||||
@ -94,17 +98,16 @@
|
||||
------------------------------------------------------------------------------
|
||||
| Conditional RMW ops | |
|
||||
------------------------------------------------------------------------------
|
||||
| atomic_cmpxchg | On success: F[mb] ->po R*[once] |
|
||||
| | ->rmw W*[once] ->po F[mb] |
|
||||
| | On failure: R*[once] |
|
||||
| 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*[once] |
|
||||
| | On failure: R*[once] |
|
||||
| atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
|
||||
| | 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 |
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel.
|
||||
REQUIREMENTS
|
||||
============
|
||||
|
||||
Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
|
||||
Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
|
||||
downloaded separately:
|
||||
|
||||
https://github.com/herd/herdtools7
|
||||
|
||||
@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
|
||||
let addr = carry-dep ; addr
|
||||
let ctrl = carry-dep ; ctrl
|
||||
let data = carry-dep ; data
|
||||
|
||||
flag ~empty (if "lkmmv2" then 0 else _)
|
||||
as this-model-requires-variant-higher-than-lkmmv1
|
||||
|
||||
@ -1,6 +1,7 @@
|
||||
macros linux-kernel.def
|
||||
bell linux-kernel.bell
|
||||
model linux-kernel.cat
|
||||
variant lkmmv2
|
||||
graph columns
|
||||
squished true
|
||||
showevents noregs
|
||||
|
||||
@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
|
||||
atomic_read_acquire(X) smp_load_acquire(X)
|
||||
atomic_set_release(X,V) { smp_store_release(X,V); }
|
||||
|
||||
atomic_add(V,X) { __atomic_op(X,+,V); }
|
||||
atomic_sub(V,X) { __atomic_op(X,-,V); }
|
||||
atomic_and(V,X) { __atomic_op(X,&,V); }
|
||||
atomic_or(V,X) { __atomic_op(X,|,V); }
|
||||
atomic_xor(V,X) { __atomic_op(X,^,V); }
|
||||
atomic_inc(X) { __atomic_op(X,+,1); }
|
||||
atomic_dec(X) { __atomic_op(X,-,1); }
|
||||
atomic_andnot(V,X) { __atomic_op(X,&~,V); }
|
||||
atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); }
|
||||
atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); }
|
||||
atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); }
|
||||
atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); }
|
||||
atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); }
|
||||
atomic_inc(X) { __atomic_op{noreturn}(X,+,1); }
|
||||
atomic_dec(X) { __atomic_op{noreturn}(X,-,1); }
|
||||
atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); }
|
||||
|
||||
atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
|
||||
atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
|
||||
@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
|
||||
atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
|
||||
atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
|
||||
atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
|
||||
|
||||
atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user