README 7.3 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228
  1. =====================================
  2. LINUX KERNEL MEMORY CONSISTENCY MODEL
  3. =====================================
  4. ============
  5. INTRODUCTION
  6. ============
  7. This directory contains the memory consistency model (memory model, for
  8. short) of the Linux kernel, written in the "cat" language and executable
  9. by the externally provided "herd7" simulator, which exhaustively explores
  10. the state space of small litmus tests.
  11. In addition, the "klitmus7" tool (also externally provided) may be used
  12. to convert a litmus test to a Linux kernel module, which in turn allows
  13. that litmus test to be exercised within the Linux kernel.
  14. ============
  15. REQUIREMENTS
  16. ============
  17. Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
  18. downloaded separately:
  19. https://github.com/herd/herdtools7
  20. See "herdtools7/INSTALL.md" for installation instructions.
  21. Note that although these tools usually provide backwards compatibility,
  22. this is not absolutely guaranteed.
  23. For example, a future version of herd7 might not work with the model
  24. in this release. A compatible model will likely be made available in
  25. a later release of Linux kernel.
  26. If you absolutely need to run the model in this particular release,
  27. please try using the exact version called out above.
  28. klitmus7 is independent of the model provided here. It has its own
  29. dependency on a target kernel release where converted code is built
  30. and executed. Any change in kernel APIs essential to klitmus7 will
  31. necessitate an upgrade of klitmus7.
  32. If you find any compatibility issues in klitmus7, please inform the
  33. memory model maintainers.
  34. klitmus7 Compatibility Table
  35. ----------------------------
  36. ============ ==========
  37. target Linux herdtools7
  38. ------------ ----------
  39. -- 4.18 7.48 --
  40. 4.15 -- 4.19 7.49 --
  41. 4.20 -- 5.5 7.54 --
  42. 5.6 -- 7.56 --
  43. ============ ==========
  44. ==================
  45. BASIC USAGE: HERD7
  46. ==================
  47. The memory model is used, in conjunction with "herd7", to exhaustively
  48. explore the state space of small litmus tests. Documentation describing
  49. the format, features, capabilities and limitations of these litmus
  50. tests is available in tools/memory-model/Documentation/litmus-tests.txt.
  51. Example litmus tests may be found in the Linux-kernel source tree:
  52. tools/memory-model/litmus-tests/
  53. Documentation/litmus-tests/
  54. Several thousand more example litmus tests are available here:
  55. https://github.com/paulmckrcu/litmus
  56. https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
  57. https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
  58. Documentation describing litmus tests and now to use them may be found
  59. here:
  60. tools/memory-model/Documentation/litmus-tests.txt
  61. The remainder of this section uses the SB+fencembonceonces.litmus test
  62. located in the tools/memory-model directory.
  63. To run SB+fencembonceonces.litmus against the memory model:
  64. $ cd $LINUX_SOURCE_TREE/tools/memory-model
  65. $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
  66. Here is the corresponding output:
  67. Test SB+fencembonceonces Allowed
  68. States 3
  69. 0:r0=0; 1:r0=1;
  70. 0:r0=1; 1:r0=0;
  71. 0:r0=1; 1:r0=1;
  72. No
  73. Witnesses
  74. Positive: 0 Negative: 3
  75. Condition exists (0:r0=0 /\ 1:r0=0)
  76. Observation SB+fencembonceonces Never 0 3
  77. Time SB+fencembonceonces 0.01
  78. Hash=d66d99523e2cac6b06e66f4c995ebb48
  79. The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
  80. this litmus test's "exists" clause can not be satisfied.
  81. See "herd7 -help" or "herdtools7/doc/" for more information on running the
  82. tool itself, but please be aware that this documentation is intended for
  83. people who work on the memory model itself, that is, people making changes
  84. to the tools/memory-model/linux-kernel.* files. It is not intended for
  85. people focusing on writing, understanding, and running LKMM litmus tests.
  86. =====================
  87. BASIC USAGE: KLITMUS7
  88. =====================
  89. The "klitmus7" tool converts a litmus test into a Linux kernel module,
  90. which may then be loaded and run.
  91. For example, to run SB+fencembonceonces.litmus against hardware:
  92. $ mkdir mymodules
  93. $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
  94. $ cd mymodules ; make
  95. $ sudo sh run.sh
  96. The corresponding output includes:
  97. Test SB+fencembonceonces Allowed
  98. Histogram (3 states)
  99. 644580 :>0:r0=1; 1:r0=0;
  100. 644328 :>0:r0=0; 1:r0=1;
  101. 711092 :>0:r0=1; 1:r0=1;
  102. No
  103. Witnesses
  104. Positive: 0, Negative: 2000000
  105. Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
  106. Hash=d66d99523e2cac6b06e66f4c995ebb48
  107. Observation SB+fencembonceonces Never 0 2000000
  108. Time SB+fencembonceonces 0.16
  109. The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
  110. that during two million trials, the state specified in this litmus
  111. test's "exists" clause was not reached.
  112. And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
  113. for more information. And again, please be aware that this documentation
  114. is intended for people who work on the memory model itself, that is,
  115. people making changes to the tools/memory-model/linux-kernel.* files.
  116. It is not intended for people focusing on writing, understanding, and
  117. running LKMM litmus tests.
  118. ====================
  119. DESCRIPTION OF FILES
  120. ====================
  121. Documentation/cheatsheet.txt
  122. Quick-reference guide to the Linux-kernel memory model.
  123. Documentation/explanation.txt
  124. Describes the memory model in detail.
  125. Documentation/litmus-tests.txt
  126. Describes the format, features, capabilities, and limitations
  127. of the litmus tests that LKMM can evaluate.
  128. Documentation/recipes.txt
  129. Lists common memory-ordering patterns.
  130. Documentation/references.txt
  131. Provides background reading.
  132. Documentation/simple.txt
  133. Starting point for someone new to Linux-kernel concurrency.
  134. And also for those needing a reminder of the simpler approaches
  135. to concurrency!
  136. linux-kernel.bell
  137. Categorizes the relevant instructions, including memory
  138. references, memory barriers, atomic read-modify-write operations,
  139. lock acquisition/release, and RCU operations.
  140. More formally, this file (1) lists the subtypes of the various
  141. event types used by the memory model and (2) performs RCU
  142. read-side critical section nesting analysis.
  143. linux-kernel.cat
  144. Specifies what reorderings are forbidden by memory references,
  145. memory barriers, atomic read-modify-write operations, and RCU.
  146. More formally, this file specifies what executions are forbidden
  147. by the memory model. Allowed executions are those which
  148. satisfy the model's "coherence", "atomic", "happens-before",
  149. "propagation", and "rcu" axioms, which are defined in the file.
  150. linux-kernel.cfg
  151. Convenience file that gathers the common-case herd7 command-line
  152. arguments.
  153. linux-kernel.def
  154. Maps from C-like syntax to herd7's internal litmus-test
  155. instruction-set architecture.
  156. litmus-tests
  157. Directory containing a few representative litmus tests, which
  158. are listed in litmus-tests/README. A great deal more litmus
  159. tests are available at https://github.com/paulmckrcu/litmus.
  160. lock.cat
  161. Provides a front-end analysis of lock acquisition and release,
  162. for example, associating a lock acquisition with the preceding
  163. and following releases and checking for self-deadlock.
  164. More formally, this file defines a performance-enhanced scheme
  165. for generation of the possible reads-from and coherence order
  166. relations on the locking primitives.
  167. README
  168. This file.
  169. scripts Various scripts, see scripts/README.