From 8d2a02b24d66aa359e83eebc1ed3c0f85367a1cb Mon Sep 17 00:00:00 2001 From: hc <hc@nodka.com> Date: Thu, 16 May 2024 03:11:33 +0000 Subject: [PATCH] AX88772C_eeprom and ax8872c build together --- kernel/tools/memory-model/README | 130 +++++++++++++++++++++++++------------------ 1 files changed, 76 insertions(+), 54 deletions(-) diff --git a/kernel/tools/memory-model/README b/kernel/tools/memory-model/README index ee987ce..c8144d4 100644 --- a/kernel/tools/memory-model/README +++ b/kernel/tools/memory-model/README @@ -20,12 +20,42 @@ REQUIREMENTS ============ -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded -separately: +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.18 7.48 -- + 4.15 -- 4.19 7.49 -- + 4.20 -- 5.5 7.54 -- + 5.6 -- 7.56 -- + ============ ========== ================== @@ -33,10 +63,32 @@ ================== The memory model is used, in conjunction with "herd7", to exhaustively -explore the state space of small litmus tests. +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. -For example, to run SB+fencembonceonces.litmus against the memory model: +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: @@ -57,7 +109,11 @@ 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. +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. ===================== @@ -94,7 +150,11 @@ test's "exists" clause was not reached. And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/" -for more information. +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. ==================== @@ -107,11 +167,20 @@ Documentation/explanation.txt Describes the memory model in detail. +Documentation/litmus-tests.txt + Describes the format, features, capabilities, and limitations + of the litmus tests that LKMM can evaluate. + Documentation/recipes.txt Lists common memory-ordering patterns. Documentation/references.txt Provides background reading. + +Documentation/simple.txt + Starting point for someone new to Linux-kernel concurrency. + And also for those needing a reminder of the simpler approaches + to concurrency! linux-kernel.bell Categorizes the relevant instructions, including memory @@ -156,51 +225,4 @@ 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. +scripts Various scripts, see scripts/README. -- Gitblit v1.6.2