tools/memory-model: Add an exception for limitations on _unless() family (4a9cc65f) · Commits · 戴 / test

According to Luc, atomic_add_unless() is directly provided by herd7, therefore it can be used in litmus tests. So change the limitation section in README to unlimit the use of atomic_add_unless(). Cc: Luc Maranget <luc.maranget@inria.fr> Acked-by:

Andrea Parri <parri.andrea@gmail.com> Reviewed-by:

Joel Fernandes (Google) <joel@joelfernandes.org> Signed-off-by:

Boqun Feng <boqun.feng@gmail.com> Signed-off-by:

Paul E. McKenney <paulmck@kernel.org>

tools/memory-model/README

+7 −3

Original line number	Diff line number	Diff line
		@@ -207,11 +207,15 @@ The Linux-kernel memory model (LKMM) has the following limitations:
		case as a store release.

		b. The "unless" RMW operations are not currently modeled:
		atomic_long_add_unless(), atomic_add_unless(),
		atomic_inc_unless_negative(), and
		atomic_dec_unless_positive(). These can be emulated
		atomic_long_add_unless(), atomic_inc_unless_negative(),
		and atomic_dec_unless_positive(). These can be emulated
		in litmus tests, for example, by using atomic_cmpxchg().

		One exception of this limitation is atomic_add_unless(),
		which is provided directly by herd7 (so no corresponding
		definition in linux-kernel.def). atomic_add_unless() is
		modeled by herd7 therefore it can be used in litmus tests.

		c. The call_rcu() function is not modeled. It can be
		emulated in litmus tests by adding another process that
		invokes synchronize_rcu() and the body of the callback

Admin message