tools/memory-model/README - third_party/kernel - 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.

 For example, a future version of herd7 might not work with the model
 in this release.  A compatible model will likely be made available in
 a later release of Linux kernel.

 If you absolutely need to run the model in this particular release,
 please try using the exact version called out above.

 klitmus7 is independent of the model provided here.  It has its own
 dependency on a target kernel release where converted code is built
 and executed.  Any change in kernel APIs essential to klitmus7 will
 necessitate an upgrade of klitmus7.

 If you find any compatibility issues in klitmus7, please inform the
 memory model maintainers.

 klitmus7 Compatibility Table
 ----------------------------

 	============  ==========
 	target Linux  herdtools7
 	------------  ----------
 	     -- 4.14  7.48 --
 	4.15 -- 4.19  7.49 --
 	4.20 -- 5.5   7.54 --
 	5.6  -- 5.16  7.56 --
 	5.17 --       7.56.1 --
 	============  ==========


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

 The memory model is used, in conjunction with "herd7", to exhaustively
 explore the state space of small litmus tests.  Documentation describing
 the format, features, capabilities and limitations of these litmus
 tests is available in tools/memory-model/Documentation/litmus-tests.txt.

 Example litmus tests may be found in the Linux-kernel source tree:

 	tools/memory-model/litmus-tests/
 	Documentation/litmus-tests/

 Several thousand more example litmus tests are available here:

 	https://github.com/paulmckrcu/litmus
 	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
 	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus

 Documentation describing litmus tests and now to use them may be found
 here:

 	tools/memory-model/Documentation/litmus-tests.txt

 The remainder of this section uses the SB+fencembonceonces.litmus test
 located in the tools/memory-model directory.

 To run SB+fencembonceonces.litmus against the memory model:

   $ cd $LINUX_SOURCE_TREE/tools/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 on running the
 tool itself, but please be aware that this documentation is intended for
 people who work on the memory model itself, that is, people making changes
 to the tools/memory-model/linux-kernel.* files.  It is not intended for
 people focusing on writing, understanding, and running LKMM litmus tests.


 =====================
 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.  And again, please be aware that this documentation
 is intended for people who work on the memory model itself, that is,
 people making changes to the tools/memory-model/linux-kernel.* files.
 It is not intended for people focusing on writing, understanding, and
 running LKMM litmus tests.


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

 Documentation/README
 	Guide to the other documents in the Documentation/ directory.

 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.

 	By "representative", it means the one in the litmus-tests
 	directory is:

 		1) simple, the number of threads should be relatively
 		   small and each thread function should be relatively
 		   simple.
 		2) orthogonal, there should be no two litmus tests
 		   describing the same aspect of the memory model.
 		3) textbook, developers can easily copy-paste-modify
 		   the litmus tests to use the patterns on their own
 		   code.

 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.
	=====================================
	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.

	For example, a future version of herd7 might not work with the model
	in this release. A compatible model will likely be made available in
	a later release of Linux kernel.

	If you absolutely need to run the model in this particular release,
	please try using the exact version called out above.

	klitmus7 is independent of the model provided here. It has its own
	dependency on a target kernel release where converted code is built
	and executed. Any change in kernel APIs essential to klitmus7 will
	necessitate an upgrade of klitmus7.

	If you find any compatibility issues in klitmus7, please inform the
	memory model maintainers.

	klitmus7 Compatibility Table
	----------------------------

	============ ==========
	target Linux herdtools7
	------------ ----------
	-- 4.14 7.48 --
	4.15 -- 4.19 7.49 --
	4.20 -- 5.5 7.54 --
	5.6 -- 5.16 7.56 --
	5.17 -- 7.56.1 --
	============ ==========


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

	The memory model is used, in conjunction with "herd7", to exhaustively
	explore the state space of small litmus tests. Documentation describing
	the format, features, capabilities and limitations of these litmus
	tests is available in tools/memory-model/Documentation/litmus-tests.txt.

	Example litmus tests may be found in the Linux-kernel source tree:

	tools/memory-model/litmus-tests/
	Documentation/litmus-tests/

	Several thousand more example litmus tests are available here:

	https://github.com/paulmckrcu/litmus
	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
	https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus

	Documentation describing litmus tests and now to use them may be found
	here:

	tools/memory-model/Documentation/litmus-tests.txt

	The remainder of this section uses the SB+fencembonceonces.litmus test
	located in the tools/memory-model directory.

	To run SB+fencembonceonces.litmus against the memory model:

	$ cd $LINUX_SOURCE_TREE/tools/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 on running the
	tool itself, but please be aware that this documentation is intended for
	people who work on the memory model itself, that is, people making changes
	to the tools/memory-model/linux-kernel.* files. It is not intended for
	people focusing on writing, understanding, and running LKMM litmus tests.


	=====================
	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. And again, please be aware that this documentation
	is intended for people who work on the memory model itself, that is,
	people making changes to the tools/memory-model/linux-kernel.* files.
	It is not intended for people focusing on writing, understanding, and
	running LKMM litmus tests.


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

	Documentation/README
	Guide to the other documents in the Documentation/ directory.

	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.

	By "representative", it means the one in the litmus-tests
	directory is:

	1) simple, the number of threads should be relatively
	small and each thread function should be relatively
	simple.
	2) orthogonal, there should be no two litmus tests
	describing the same aspect of the memory model.
	3) textbook, developers can easily copy-paste-modify
	the litmus tests to use the patterns on their own
	code.

	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.