Commit d8fa25c4 authored by Paul E. McKenney's avatar Paul E. McKenney Committed by Ingo Molnar
Browse files

tools/memory-model: Add more LKMM limitations



This commit adds more detail about compiler optimizations and
not-yet-modeled Linux-kernel APIs.

Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.vnet.ibm.com>
Reviewed-by: default avatarAndrea Parri <andrea.parri@amarulasolutions.com>
Cc: Alexander Shishkin <alexander.shishkin@linux.intel.com>
Cc: Arnaldo Carvalho de Melo <acme@redhat.com>
Cc: Jiri Olsa <jolsa@redhat.com>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Stephane Eranian <eranian@google.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Vince Weaver <vincent.weaver@maine.edu>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/20180926182920.27644-4-paulmck@linux.ibm.com


Signed-off-by: default avatarIngo Molnar <mingo@kernel.org>
parent 3d2046a6
Loading
Loading
Loading
Loading
+39 −0
Original line number Diff line number Diff line
@@ -171,6 +171,12 @@ The Linux-kernel memory model has the following limitations:
	particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
	and "A WARNING" sections).

	Note that this limitation in turn limits LKMM's ability to
	accurately model address, control, and data dependencies.
	For example, if the compiler can deduce the value of some variable
	carrying a dependency, then the compiler can break that dependency
	by substituting a constant of that value.

2.	Multiple access sizes for a single variable are not supported,
	and neither are misaligned or partially overlapping accesses.

@@ -190,6 +196,36 @@ The Linux-kernel memory model has the following limitations:
	However, a substantial amount of support is provided for these
	operations, as shown in the linux-kernel.def file.

	a.	When rcu_assign_pointer() is passed NULL, the Linux
		kernel provides no ordering, but LKMM models this
		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
		in litmus tests, for example, by using atomic_cmpxchg().

	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
		function, with (for example) a release-acquire from
		the site of the emulated call_rcu() to the beginning
		of the additional process.

	d.	The rcu_barrier() function is not modeled.  It can be
		emulated in litmus tests emulating call_rcu() via
		(for example) a release-acquire from the end of each
		additional call_rcu() process to the site of the
		emulated rcu-barrier().

	e.	Sleepable RCU (SRCU) is not modeled.  It can be
		emulated, but perhaps not simply.

	f.	Reader-writer locking is not modeled.  It can be
		emulated in litmus tests using atomic read-modify-write
		operations.

The "herd7" tool has some additional limitations of its own, apart from
the memory model:

@@ -204,3 +240,6 @@ the memory model:
Some of these limitations may be overcome in the future, but others are
more likely to be addressed by incorporating the Linux-kernel memory model
into other tools.

Finally, please note that LKMM is subject to change as hardware, use cases,
and compilers evolve.