linux/tools/memory-model
Linus Torvalds 60eb450742 LKMM scripting updates for v6.4
This update improves litmus-test documentation and improves the ability
 to do before/after tests on the https://github.com/paulmckrcu/litmus repo.
 -----BEGIN PGP SIGNATURE-----
 
 iQJHBAABCgAxFiEEbK7UrM+RBIrCoViJnr8S83LZ+4wFAmQwtAMTHHBhdWxtY2tA
 a2VybmVsLm9yZwAKCRCevxLzctn7jE9AD/4pdoS4w+XmGTkOaSYWVKz0B822+FnZ
 822s/Z+4sA7ngoDEx4NSno299mSjONMS/HS8oTDXQQgGL7xXZNJc1phD1oP17dwa
 3Ic6RKqWlYLOtFLfGLZF+wvVo6Z0WLnyh4KDeA31AVcb/Cdzzb30RZTO9oz1WDZH
 ueD4egvl6ECyZPh2HfjcQ7Y2hH00Ohi1igY+WPCBiMM1FrTbPmaLrAwsRrEbhsqx
 PwnrbMdGrTvT62sgnm9LHGr/P2YKDdYxs8wUyWRg876KitdUPmZb8uy2gZ0Bpp5+
 mMB6h54mjVtDnpVtPHm8u4Viq2ir3zSlbWGmI24JxFCn3FTRFQwYQMCPBm7tlpqB
 n+08OGtWDRM3b+aLa5gYo1MogMayWtZN/vL6/9BSTF6mvjMbKLu2esi6JttU1tOV
 o4LvG+b6lO+L1ZvQctnDmzCPjmVB4QuFZvcNdRwHIVFtlG2v2ffaZ5ogaM+3uN4u
 vUeW5pOmAaD3aO0g7xJVdTwHfBasxrXfYazjYPdpvuoIXHbOeEC+LVfCaQVJRFGf
 20w0lB6hZqsE8qnaKAvHzupDi7nz3X0Ge/PAvu54o9PgOP1XKDNH+p6fCxefCx1T
 M8VnQHdgR29kuyrVy9XbQjRDgEXSPrQXrItl2B8MAoXVhaCDt6LOQ/LyGnKL3Q7w
 4sEBieegEnqLQQ==
 =kQ01
 -----END PGP SIGNATURE-----

Merge tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu

Pull Linux Kernel Memory Model scripting updates from Paul McKenney:
 "This improves litmus-test documentation and improves the ability to do
  before/after tests on the https://github.com/paulmckrcu/litmus repo"

* tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: (32 commits)
  tools/memory-model: Remove out-of-date SRCU documentation
  tools/memory-model: Document LKMM test procedure
  tools/memory-model: Use "grep -E" instead of "egrep"
  tools/memory-model: Use "-unroll 0" to keep --hw runs finite
  tools/memory-model: Make judgelitmus.sh handle scripted Result: tag
  tools/memory-model: Add data-race capabilities to judgelitmus.sh
  tools/memory-model: Add checktheselitmus.sh to run specified litmus tests
  tools/memory-model: Repair parseargs.sh header comment
  tools/memory-model:  Add "--" to parseargs.sh for additional arguments
  tools/memory-model: Make history-check scripts use mselect7
  tools/memory-model: Make checkghlitmus.sh use mselect7
  tools/memory-model: Fix scripting --jobs argument
  tools/memory-model: Implement --hw support for checkghlitmus.sh
  tools/memory-model: Add -v flag to jingle7 runs
  tools/memory-model: Make runlitmus.sh check for jingle errors
  tools/memory-model: Allow herd to deduce CPU type
  tools/memory-model: Keep assembly-language litmus tests
  tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out
  tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw
  tools/memory-model: Split runlitmus.sh out of checklitmus.sh
  ...
2023-04-24 12:02:25 -07:00
..
Documentation LKMM scripting updates for v6.4 2023-04-24 12:02:25 -07:00
litmus-tests tools/memory-model: Keep assembly-language litmus tests 2023-03-24 10:24:14 -07:00
scripts tools/memory-model: Document LKMM test procedure 2023-03-24 10:24:15 -07:00
.gitignore
linux-kernel.bell tools/memory-model: Provide exact SRCU semantics 2023-03-22 12:02:21 -07:00
linux-kernel.cat tools/memory-model: Make ppo a subrelation of po 2023-03-22 12:02:21 -07:00
linux-kernel.cfg
linux-kernel.def tools/memory-model: Provide exact SRCU semantics 2023-03-22 12:02:21 -07:00
lock.cat tools/memory-model: Provide exact SRCU semantics 2023-03-22 12:02:21 -07:00
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.