PPaul E. McKenneytools/memory-model: Document LKMM test procedure
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
tools/memory-model: Document LKMM test procedure This commit documents how to run the various scripts in order to test a potentially pervasive change to the memory model. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Hardware checking for check{,all}litmus.sh This commit makes checklitmus.sh and checkalllitmus.sh check to see if a hardware verification was specified (via the --hw command-line argument, which sets the LKMM_HW_MAP_FILE environment variable). If so, the C-language litmus test is converted to the specified type of assembly-language litmus test and herd is run on it. Hardware is permitted to be stronger than LKMM requires, so "Always" and "Never" verifications of "Sometimes" C-language litmus tests are forgiven. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Use "grep -E" instead of "egrep" The latest version of grep claims the egrep is now obsolete so the build now contains warnings that look like: egrep: warning: egrep is obsolescent; using grep -E fix this up by moving the related file to use "grep -E" instead. sed -i "s/egrep/grep -E/g" grep egrep -rwl tools/memory-model Here are the steps to install the latest grep: wget http://ftp.gnu.org/gnu/grep/grep-3.8.tar.gz tar xf grep-3.8.tar.gz cd grep-3.8 && ./configure && make sudo make install export PATH=/usr/local/bin:$PATH Signed-off-by: Tiezhu Yang <yangtiezhu@loongson.cn> Reviewed-by: Akira Yokosawa <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Split runlitmus.sh out of checklitmus.sh This commit prepares for adding --hw capability to github litmus-test scripts by splitting runlitmus.sh (which simply runs the verification) out of checklitmus.sh (which also judges the results). Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Fix paulmck email address on pre-existing scripts Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Add checktheselitmus.sh to run specified litmus tests This commit adds a checktheselitmus.sh script that runs the litmus tests specified on the command line. This is useful for verifying fixes to specific litmus tests. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Make judgelitmus.sh identify bad macros Currently, judgelitmus.sh treats use of unknown primitives (such as srcu_read_lock() prior to SRCU support) as "!!! Verification error". This can be misleading because it fails to call out typos and running a version LKMM on a litmus test requiring a feature not provided by that version. This commit therefore changes judgelitmus.sh to check for unknown primitives and to report them, for example, with: '!!! Current LKMM version does not know "rcu_write_lock"'. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Implement --hw support for checkghlitmus.sh This commits enables the "--hw" argument for the checkghlitmus.sh script, causing it to convert any applicable C-language litmus tests to the specified flavor of assembly language, to verify these assembly-language litmus tests, and checking compatibility of the outcomes. Note that the conversion does not yet handle locking, RCU, SRCU, plain C-language memory accesses, or casts. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Make history-check scripts use mselect7 The history-check scripts currently use grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists the aid of "mselect7 -arch C", given Luc Maraget's recent modifications that allow mselect7 to operate in filter mode. This change requires herdtools 7.52-32-g1da3e0e50977 or later. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Make judgelitmus.sh handle scripted Result: tag The scripts that generate the litmus tests in the "auto" directory of the https://github.com/paulmckrcu/litmus archive place the "Result:" tag into a single-line ocaml comment, which judgelitmus.sh currently does not recognize. This commit therefore makes judgelitmus.sh recognize both the multiline comment format that it currently does and the automatically generated single-line format. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Make history-check scripts use mselect7 The history-check scripts currently use grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists the aid of "mselect7 -arch C", given Luc Maraget's recent modifications that allow mselect7 to operate in filter mode. This change requires herdtools 7.52-32-g1da3e0e50977 or later. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Repair parseargs.sh header comment Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Use "-unroll 0" to keep --hw runs finite Litmus tests involving atomic operations produce LL/SC loops on a number of architectures, and unrolling these loops can result in excessive verification times or even stack overflows. This commit therefore uses the "-unroll 0" herd7 argument to avoid unrolling, on the grounds that additional passes through an LL/SC loop should not change the verification. Note however, that certain bugs in the mapping of the LL/SC loop to machine instructions may go undetected. On the other hand, herd7 might not be the best vehicle for finding such bugs in any case. (You do stress-test your architecture-specific code, don't you?) Suggested-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Implement --hw support for checkghlitmus.sh This commits enables the "--hw" argument for the checkghlitmus.sh script, causing it to convert any applicable C-language litmus tests to the specified flavor of assembly language, to verify these assembly-language litmus tests, and checking compatibility of the outcomes. Note that the conversion does not yet handle locking, RCU, SRCU, plain C-language memory accesses, or casts. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 | |
tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU This commit abstracts out common function to check a given litmus test for locking, RCU, and SRCU in order to avoid duplicating code. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> | 3 年前 |