tools/memory-model/README - linux - Git at Google

 		=====================================
 		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.52 or higher of the "herd7" and "klitmus7" tools must be
 downloaded separately:

   https://github.com/herd/herdtools7

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

 Note that although these tools usually provide backwards compatibility,
 this is not absolutely guaranteed.  Therefore, if a later version does
 not work, please try using the exact version called out above.


 ==================
 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+fencembonceonces.litmus against the memory model:

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

 Here is the corresponding output:

   Test SB+fencembonceonces 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+fencembonceonces Never 0 3
   Time SB+fencembonceonces 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+fencembonceonces.litmus against hardware:

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

 The corresponding output includes:

   Test SB+fencembonceonces 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+fencembonceonces Never 0 2000000
   Time SB+fencembonceonces 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.

 scripts	Various scripts, see scripts/README.


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

 The Linux-kernel memory model (LKMM) has the following limitations:

 1.	Compiler optimizations are not accurately modeled.  Of course,
 	the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
 	ability to optimize, but under some circumstances it is possible
 	for the compiler to undermine the memory model.  For more
 	information, see Documentation/explanation.txt (in 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.

 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.

 	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.	Although sleepable RCU (SRCU) is now modeled, there
 		are some subtle differences between its semantics and
 		those in the Linux kernel.  For example, the kernel
 		might interpret the following sequence as two partially
 		overlapping SRCU read-side critical sections:

 			 1  r1 = srcu_read_lock(&my_srcu);
 			 2  do_something_1();
 			 3  r2 = srcu_read_lock(&my_srcu);
 			 4  do_something_2();
 			 5  srcu_read_unlock(&my_srcu, r1);
 			 6  do_something_3();
 			 7  srcu_read_unlock(&my_srcu, r2);

 		In contrast, LKMM will interpret this as a nested pair of
 		SRCU read-side critical sections, with the outer critical
 		section spanning lines 1-7 and the inner critical section
 		spanning lines 3-5.

 		This difference would be more of a concern had anyone
 		identified a reasonable use case for partially overlapping
 		SRCU read-side critical sections.  For more information,
 		please see: https://paulmck.livejournal.com/40593.html

 	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:

 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.

 Finally, please note that LKMM is subject to change as hardware, use cases,
 and compilers evolve.
	=====================================
	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.52 or higher of the "herd7" and "klitmus7" tools must be
	downloaded separately:

	https://github.com/herd/herdtools7

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

	Note that although these tools usually provide backwards compatibility,
	this is not absolutely guaranteed. Therefore, if a later version does
	not work, please try using the exact version called out above.


	==================
	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+fencembonceonces.litmus against the memory model:

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

	Here is the corresponding output:

	Test SB+fencembonceonces 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+fencembonceonces Never 0 3
	Time SB+fencembonceonces 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+fencembonceonces.litmus against hardware:

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

	The corresponding output includes:

	Test SB+fencembonceonces 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+fencembonceonces Never 0 2000000
	Time SB+fencembonceonces 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.

	scripts Various scripts, see scripts/README.


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

	The Linux-kernel memory model (LKMM) has the following limitations:

	1. Compiler optimizations are not accurately modeled. Of course,
	the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
	ability to optimize, but under some circumstances it is possible
	for the compiler to undermine the memory model. For more
	information, see Documentation/explanation.txt (in 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.

	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.

	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. Although sleepable RCU (SRCU) is now modeled, there
	are some subtle differences between its semantics and
	those in the Linux kernel. For example, the kernel
	might interpret the following sequence as two partially
	overlapping SRCU read-side critical sections:

	1 r1 = srcu_read_lock(&my_srcu);
	2 do_something_1();
	3 r2 = srcu_read_lock(&my_srcu);
	4 do_something_2();
	5 srcu_read_unlock(&my_srcu, r1);
	6 do_something_3();
	7 srcu_read_unlock(&my_srcu, r2);

	In contrast, LKMM will interpret this as a nested pair of
	SRCU read-side critical sections, with the outer critical
	section spanning lines 1-7 and the inner critical section
	spanning lines 3-5.

	This difference would be more of a concern had anyone
	identified a reasonable use case for partially overlapping
	SRCU read-side critical sections. For more information,
	please see: https://paulmck.livejournal.com/40593.html

	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:

	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.

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