Commit de6f9972 authored by Jonas Oberhauser's avatar Jonas Oberhauser Committed by Paul E. McKenney
Browse files

tools/memory-model: Legitimize current use of tags in LKMM macros 



The current macros in linux-kernel.def reference instructions such as
__xchg{mb} or __cmpxchg{acquire}, which are invalid combinations of tags
and instructions according to the declarations in linux-kernel.bell.
This works with current herd7 because herd7 removes these tags anyways
and does not actually enforce validity of combinations at all.

If a future herd7 version no longer applies these hardcoded
transformations, then all currently invalid combinations will actually
appear on some instruction.

We therefore adjust the declarations to make the resulting combinations
valid, by adding the 'mb tag to the set of Accesses and allowing all
Accesses to appear on all read, write, and RMW instructions.

Signed-off-by: default avatarJonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Signed-off-by: default avatarPaul E. McKenney <paulmck@kernel.org>
Reviewed-by: default avatarBoqun Feng <boqun.feng@gmail.com>
Tested-by: default avatarBoqun Feng <boqun.feng@gmail.com>
parent e176ebff

tools/memory-model/linux-kernel.bell

+5 −4
Original line number Diff line number Diff line
@@ -16,10 +16,11 @@ 
enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||

		'release (*smp_store_release*) ||

		'acquire (*smp_load_acquire*) ||

		'noreturn (* R of non-return RMW *)

instructions R[{'once,'acquire,'noreturn}]

instructions W[{'once,'release}]

instructions RMW[{'once,'acquire,'release}]

		'noreturn (* R of non-return RMW *) ||

		'mb (*xchg(),cmpxchg(),...*)

instructions R[Accesses]

instructions W[Accesses]

instructions RMW[Accesses]



enum Barriers = 'wmb (*smp_wmb*) ||

		'rmb (*smp_rmb*) ||