From 2024436d482eca356840a3aec022bad68f72eb25 Mon Sep 17 00:00:00 2001 From: "Paul E. McKenney" Date: Tue, 19 Mar 2019 14:39:10 -0700 Subject: tools/memory-model: Make judgelitmus.sh handle hardware verifications This commit makes the judgelitmus.sh script check the --hw argument (AKA the LKMM_HW_MAP_FILE environment variable) and to adjust its judgment for a run where a C-language litmus test has been translated to assembly and the assembly version verified. In this case, the assembly verification output is checked against the C-language script's "Result:" comment. However, because hardware can be stronger than LKMM requires, the judgelitmus.sh script forgives verification mismatches featuring a "Sometimes" in the C-language script and an "Always" or "Never" assembly-language verification. Note that deadlock is not forgiven, however, this should not normally be an issue given that C-language tests containing locking, RCU, or SRCU cannot be translated to assembly. However, this issue can crop up in litmus tests that mimic deadlock by using the "filter" clause to ignore all executions. It can also crop up when certain herd arguments are used to autofilter everything that does not match the "exists" clause in cases where the "exists" clause cannot be satisfied. Signed-off-by: Paul E. McKenney --- tools/memory-model/scripts/README | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tools/memory-model/scripts/README') diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index 095c7eb36f9f..0e29a52044c1 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -43,10 +43,10 @@ initlitmushist.sh judgelitmus.sh - Given a .litmus file and its .litmus.out herd7 output, check the - .litmus.out file against the .litmus file's "Result:" comment to - judge whether the test ran correctly. Not normally run manually, - provided instead for use by other scripts. + Given a .litmus file and its herd7 output, check the output file + against the .litmus file's "Result:" comment to judge whether + the test ran correctly. Not normally run manually, provided + instead for use by other scripts. newlitmushist.sh -- cgit v1.2.3 From df0f675065bf003c4f182941f62b01b06be97182 Mon Sep 17 00:00:00 2001 From: "Paul E. McKenney" Date: Thu, 2 May 2019 10:05:14 -0700 Subject: 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 --- tools/memory-model/scripts/README | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'tools/memory-model/scripts/README') diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index 0e29a52044c1..cc2c4e5be9ec 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -27,6 +27,14 @@ checklitmushist.sh checklitmus.sh Check a single litmus test against its "Result:" expected result. + Not intended to for manual use. + +checktheselitmus.sh + + Check the specified list of litmus tests against their "Result:" + expected results. This takes optional parseargs.sh arguments, + followed by "--" followed by pathnames starting from the current + directory. cmplitmushist.sh -- cgit v1.2.3 From 05dc8470b3bfcad6b84bcf5953172ce26cfb2bd9 Mon Sep 17 00:00:00 2001 From: "Paul E. McKenney" Date: Thu, 26 Jan 2023 15:41:00 -0800 Subject: 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 --- tools/memory-model/scripts/README | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'tools/memory-model/scripts/README') diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index cc2c4e5be9ec..fb39bd0fd1b9 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -76,3 +76,35 @@ runlitmushist.sh README This file + +Testing a change to LKMM might go as follows: + + # Populate expected results without that change, and + # runs for about an hour on an 8-CPU x86 system: + scripts/initlitmushist.sh --timeout 10m --procs 10 + # Incorporate the change: + git am -s -3 /path/to/patch # Or whatever it takes. + + # Test the new version of LKMM as follows... + + # Runs in seconds, good smoke test: + scripts/checkalllitmus.sh + + # Compares results to those produced by initlitmushist.sh, + # and runs for about an hour on an 8-CPU x86 system: + scripts/checklitmushist.sh --timeout 10m --procs 10 + + # Checks results against Result tags, runs in minutes: + scripts/checkghlitmus.sh --timeout 10m --procs 10 + +The checkghlitmus.sh should not report errors in cases where the +checklitmushist.sh script did not also report a change. However, +this check is nevertheless valuable because it can find errors in the +original version of LKMM. Note however, that given the above procedure, +an error in the original LKMM version that is fixed by the patch will +be reported both as a mismatch by checklitmushist.sh and as an error +by checkghlitmus.sh. One exception to this rule of thumb is when the +test fails completely on the original version of LKMM and passes on the +new version. In this case, checklitmushist.sh will report a mismatch +and checkghlitmus.sh will report success. This happens when the change +to LKMM introduces a new primitive for which litmus tests already existed. -- cgit v1.2.3