Documentation/litmus-tests: Add locking tests to README

This commit documents the litmus tests in the "locking" directory.

[ paulmck: Apply formatting feedback from Andrea Parri. ]

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: Mark Rutland <mark.rutland@arm.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: <linux-arch@vger.kernel.org>
Cc: <linux-doc@vger.kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
This commit is contained in:
Paul E. McKenney 2024-02-01 10:51:28 -08:00
parent 39cd87c4eb
commit d2c470c491

View File

@ -22,6 +22,35 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
NOTE: Require herd7 7.56 or later which supports "(void)expr".
locking (/locking directory)
----------------------------
DCL-broken.litmus
Demonstrates that double-checked locking needs more than just
the obvious lock acquisitions and releases.
DCL-fixed.litmus
Demonstrates corrected double-checked locking that uses
smp_store_release() and smp_load_acquire() in addition to the
obvious lock acquisitions and releases.
RM-broken.litmus
Demonstrates problems with "roach motel" locking, where code is
freely moved into lock-based critical sections. This example also
shows how to use the "filter" clause to discard executions that
would be excluded by other code not modeled in the litmus test.
Note also that this "roach motel" optimization is emulated by
physically moving P1()'s two reads from x under the lock.
What is a roach motel? This is from an old advertisement for
a cockroach trap, much later featured in one of the "Men in
Black" movies. "The roaches check in. They don't check out."
RM-fixed.litmus
The counterpart to RM-broken.litmus, showing P0()'s two loads from
x safely outside of the critical section.
RCU (/rcu directory)
--------------------