linux/tools/memory-model
Alan Stern bd5c0ba2cd tools/memory-model: Finish the removal of rb-dep, smp_read_barrier_depends(), and lockless_dereference()
Commit:

  bf28ae5627 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")

was merged too early, while it was still in RFC form.  This patch adds in
the missing pieces.

Akira pointed out some typos in the original patch, and he noted that
cheatsheet.txt should indicate that READ_ONCE() now implies an address
dependency.  Andrea suggested documenting the relationship betwwen
unsuccessful RMW operations and address dependencies.

Andrea pointed out that the macro for rcu_dereference() in linux.def
should now use the "once" annotation instead of "deref".  He also
suggested that the comments should mention commit:

  5a8897cc76 ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics")

... as an important precursor, and he contributed commit:

  cb13b424e9 ("locking/xchg/alpha: Add unconditional memory barrier to cmpxchg()")

which is another prerequisite.

Suggested-by: Akira Yokosawa <akiyks@gmail.com>
Suggested-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
[ Fixed read_read_lock() typo reported by Akira. ]
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
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: will.deacon@arm.com
Fixes: bf28ae5627 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
Link: http://lkml.kernel.org/r/1520443660-16858-4-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-03-10 10:22:23 +01:00
..
Documentation tools/memory-model: Finish the removal of rb-dep, smp_read_barrier_depends(), and lockless_dereference() 2018-03-10 10:22:23 +01:00
litmus-tests tools/memory-model: Add documentation of new litmus test 2018-03-10 10:22:23 +01:00
linux-kernel.bell tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference 2018-02-21 09:58:16 +01:00
linux-kernel.cat tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference 2018-02-21 09:58:16 +01:00
linux-kernel.cfg
linux-kernel.def tools/memory-model: Finish the removal of rb-dep, smp_read_barrier_depends(), and lockless_dereference() 2018-03-10 10:22:23 +01:00
lock.cat
README tools/memory-model: Remove mention of docker/gentoo image 2018-03-10 10:22:23 +01:00

		=====================================
		LINUX KERNEL MEMORY CONSISTENCY MODEL
		=====================================

============
INTRODUCTION
============

This directory contains the memory consistency model (memory model, for
short) of the Linux kernel, written in the "cat" language and executable
by the externally provided "herd7" simulator, which exhaustively explores
the state space of small litmus tests.

In addition, the "klitmus7" tool (also externally provided) may be used
to convert a litmus test to a Linux kernel module, which in turn allows
that litmus test to be exercised within the Linux kernel.


============
REQUIREMENTS
============

Version 7.48 of the "herd7" and "klitmus7" tools must be downloaded
separately:

  https://github.com/herd/herdtools7

See "herdtools7/INSTALL.md" for installation instructions.


==================
BASIC USAGE: HERD7
==================

The memory model is used, in conjunction with "herd7", to exhaustively
explore the state space of small litmus tests.

For example, to run SB+mbonceonces.litmus against the memory model:

  $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus

Here is the corresponding output:

  Test SB+mbonceonces Allowed
  States 3
  0:r0=0; 1:r0=1;
  0:r0=1; 1:r0=0;
  0:r0=1; 1:r0=1;
  No
  Witnesses
  Positive: 0 Negative: 3
  Condition exists (0:r0=0 /\ 1:r0=0)
  Observation SB+mbonceonces Never 0 3
  Time SB+mbonceonces 0.01
  Hash=d66d99523e2cac6b06e66f4c995ebb48

The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
this litmus test's "exists" clause can not be satisfied.

See "herd7 -help" or "herdtools7/doc/" for more information.


=====================
BASIC USAGE: KLITMUS7
=====================

The "klitmus7" tool converts a litmus test into a Linux kernel module,
which may then be loaded and run.

For example, to run SB+mbonceonces.litmus against hardware:

  $ mkdir mymodules
  $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus
  $ cd mymodules ; make
  $ sudo sh run.sh

The corresponding output includes:

  Test SB+mbonceonces Allowed
  Histogram (3 states)
  644580  :>0:r0=1; 1:r0=0;
  644328  :>0:r0=0; 1:r0=1;
  711092  :>0:r0=1; 1:r0=1;
  No
  Witnesses
  Positive: 0, Negative: 2000000
  Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
  Hash=d66d99523e2cac6b06e66f4c995ebb48
  Observation SB+mbonceonces Never 0 2000000
  Time SB+mbonceonces 0.16

The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
that during two million trials, the state specified in this litmus
test's "exists" clause was not reached.

And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
for more information.


====================
DESCRIPTION OF FILES
====================

Documentation/cheatsheet.txt
	Quick-reference guide to the Linux-kernel memory model.

Documentation/explanation.txt
	Describes the memory model in detail.

Documentation/recipes.txt
	Lists common memory-ordering patterns.

Documentation/references.txt
	Provides background reading.

linux-kernel.bell
	Categorizes the relevant instructions, including memory
	references, memory barriers, atomic read-modify-write operations,
	lock acquisition/release, and RCU operations.

	More formally, this file (1) lists the subtypes of the various
	event types used by the memory model and (2) performs RCU
	read-side critical section nesting analysis.

linux-kernel.cat
	Specifies what reorderings are forbidden by memory references,
	memory barriers, atomic read-modify-write operations, and RCU.

	More formally, this file specifies what executions are forbidden
	by the memory model.  Allowed executions are those which
	satisfy the model's "coherence", "atomic", "happens-before",
	"propagation", and "rcu" axioms, which are defined in the file.

linux-kernel.cfg
	Convenience file that gathers the common-case herd7 command-line
	arguments.

linux-kernel.def
	Maps from C-like syntax to herd7's internal litmus-test
	instruction-set architecture.

litmus-tests
	Directory containing a few representative litmus tests, which
	are listed in litmus-tests/README.  A great deal more litmus
	tests are available at https://github.com/paulmckrcu/litmus.

lock.cat
	Provides a front-end analysis of lock acquisition and release,
	for example, associating a lock acquisition with the preceding
	and following releases and checking for self-deadlock.

	More formally, this file defines a performance-enhanced scheme
	for generation of the possible reads-from and coherence order
	relations on the locking primitives.

README
	This file.


===========
LIMITATIONS
===========

The Linux-kernel memory model has the following limitations:

1.	Compiler optimizations are not modeled.  Of course, the use
	of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
	to optimize, but there is Linux-kernel code that uses bare C
	memory accesses.  Handling this code is on the to-do list.
	For more information, see Documentation/explanation.txt (in
	particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
	and "A WARNING" sections).

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

3.	Exceptions and interrupts are not modeled.  In some cases,
	this limitation can be overcome by modeling the interrupt or
	exception with an additional process.

4.	I/O such as MMIO or DMA is not supported.

5.	Self-modifying code (such as that found in the kernel's
	alternatives mechanism, function tracer, Berkeley Packet Filter
	JIT compiler, and module loader) is not supported.

6.	Complete modeling of all variants of atomic read-modify-write
	operations, locking primitives, and RCU is not provided.
	For example, call_rcu() and rcu_barrier() are not supported.
	However, a substantial amount of support is provided for these
	operations, as shown in the linux-kernel.def file.

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

1.	Non-trivial data structures such as arrays or structures are
	not supported.	However, pointers are supported, allowing trivial
	linked lists to be constructed.

2.	Dynamic memory allocation is not supported, although this can
	be worked around in some cases by supplying multiple statically
	allocated variables.

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.