mirror of
https://github.com/torvalds/linux.git
synced 2024-11-21 19:41:42 +00:00
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 ...
This commit is contained in:
Linus Torvalds
commit
60eb450742
54
Documentation/litmus-tests/locking/DCL-broken.litmus
Normal file
54
Documentation/litmus-tests/locking/DCL-broken.litmus
Normal file
@ -0,0 +1,54 @@
|
||||
C DCL-broken
|
||||
|
||||
(*
|
||||
* Result: Sometimes
|
||||
*
|
||||
* This litmus test demonstrates more than just locking is required to
|
||||
* correctly implement double-checked locking.
|
||||
*)
|
||||
|
||||
{
|
||||
int flag;
|
||||
int data;
|
||||
}
|
||||
|
||||
P0(int *flag, int *data, spinlock_t *lck)
|
||||
{
|
||||
int r0;
|
||||
int r1;
|
||||
int r2;
|
||||
|
||||
r0 = READ_ONCE(*flag);
|
||||
if (r0 == 0) {
|
||||
spin_lock(lck);
|
||||
r1 = READ_ONCE(*flag);
|
||||
if (r1 == 0) {
|
||||
WRITE_ONCE(*data, 1);
|
||||
WRITE_ONCE(*flag, 1);
|
||||
}
|
||||
spin_unlock(lck);
|
||||
}
|
||||
r2 = READ_ONCE(*data);
|
||||
}
|
||||
|
||||
P1(int *flag, int *data, spinlock_t *lck)
|
||||
{
|
||||
int r0;
|
||||
int r1;
|
||||
int r2;
|
||||
|
||||
r0 = READ_ONCE(*flag);
|
||||
if (r0 == 0) {
|
||||
spin_lock(lck);
|
||||
r1 = READ_ONCE(*flag);
|
||||
if (r1 == 0) {
|
||||
WRITE_ONCE(*data, 1);
|
||||
WRITE_ONCE(*flag, 1);
|
||||
}
|
||||
spin_unlock(lck);
|
||||
}
|
||||
r2 = READ_ONCE(*data);
|
||||
}
|
||||
|
||||
locations [flag;data;0:r0;0:r1;1:r0;1:r1]
|
||||
exists (0:r2=0 \/ 1:r2=0)
|
||||
55
Documentation/litmus-tests/locking/DCL-fixed.litmus
Normal file
55
Documentation/litmus-tests/locking/DCL-fixed.litmus
Normal file
@ -0,0 +1,55 @@
|
||||
C DCL-fixed
|
||||
|
||||
(*
|
||||
* Result: Never
|
||||
*
|
||||
* This litmus test demonstrates that double-checked locking can be
|
||||
* reliable given proper use of smp_load_acquire() and smp_store_release()
|
||||
* in addition to the locking.
|
||||
*)
|
||||
|
||||
{
|
||||
int flag;
|
||||
int data;
|
||||
}
|
||||
|
||||
P0(int *flag, int *data, spinlock_t *lck)
|
||||
{
|
||||
int r0;
|
||||
int r1;
|
||||
int r2;
|
||||
|
||||
r0 = smp_load_acquire(flag);
|
||||
if (r0 == 0) {
|
||||
spin_lock(lck);
|
||||
r1 = READ_ONCE(*flag);
|
||||
if (r1 == 0) {
|
||||
WRITE_ONCE(*data, 1);
|
||||
smp_store_release(flag, 1);
|
||||
}
|
||||
spin_unlock(lck);
|
||||
}
|
||||
r2 = READ_ONCE(*data);
|
||||
}
|
||||
|
||||
P1(int *flag, int *data, spinlock_t *lck)
|
||||
{
|
||||
int r0;
|
||||
int r1;
|
||||
int r2;
|
||||
|
||||
r0 = smp_load_acquire(flag);
|
||||
if (r0 == 0) {
|
||||
spin_lock(lck);
|
||||
r1 = READ_ONCE(*flag);
|
||||
if (r1 == 0) {
|
||||
WRITE_ONCE(*data, 1);
|
||||
smp_store_release(flag, 1);
|
||||
}
|
||||
spin_unlock(lck);
|
||||
}
|
||||
r2 = READ_ONCE(*data);
|
||||
}
|
||||
|
||||
locations [flag;data;0:r0;0:r1;1:r0;1:r1]
|
||||
exists (0:r2=0 \/ 1:r2=0)
|
||||
41
Documentation/litmus-tests/locking/RM-broken.litmus
Normal file
41
Documentation/litmus-tests/locking/RM-broken.litmus
Normal file
@ -0,0 +1,41 @@
|
||||
C RM-broken
|
||||
|
||||
(*
|
||||
* Result: DEADLOCK
|
||||
*
|
||||
* This litmus test demonstrates that the old "roach motel" approach
|
||||
* to locking, where code can be freely moved into critical sections,
|
||||
* cannot be used in the Linux kernel.
|
||||
*)
|
||||
|
||||
{
|
||||
int x;
|
||||
atomic_t y;
|
||||
}
|
||||
|
||||
P0(int *x, atomic_t *y, spinlock_t *lck)
|
||||
{
|
||||
int r2;
|
||||
|
||||
spin_lock(lck);
|
||||
r2 = atomic_inc_return(y);
|
||||
WRITE_ONCE(*x, 1);
|
||||
spin_unlock(lck);
|
||||
}
|
||||
|
||||
P1(int *x, atomic_t *y, spinlock_t *lck)
|
||||
{
|
||||
int r0;
|
||||
int r1;
|
||||
int r2;
|
||||
|
||||
spin_lock(lck);
|
||||
r0 = READ_ONCE(*x);
|
||||
r1 = READ_ONCE(*x);
|
||||
r2 = atomic_inc_return(y);
|
||||
spin_unlock(lck);
|
||||
}
|
||||
|
||||
locations [x;0:r2;1:r0;1:r1;1:r2]
|
||||
filter (1:r0=0 /\ 1:r1=1)
|
||||
exists (1:r2=1)
|
||||
41
Documentation/litmus-tests/locking/RM-fixed.litmus
Normal file
41
Documentation/litmus-tests/locking/RM-fixed.litmus
Normal file
@ -0,0 +1,41 @@
|
||||
C RM-fixed
|
||||
|
||||
(*
|
||||
* Result: Never
|
||||
*
|
||||
* This litmus test demonstrates that the old "roach motel" approach
|
||||
* to locking, where code can be freely moved into critical sections,
|
||||
* cannot be used in the Linux kernel.
|
||||
*)
|
||||
|
||||
{
|
||||
int x;
|
||||
atomic_t y;
|
||||
}
|
||||
|
||||
P0(int *x, atomic_t *y, spinlock_t *lck)
|
||||
{
|
||||
int r2;
|
||||
|
||||
spin_lock(lck);
|
||||
r2 = atomic_inc_return(y);
|
||||
WRITE_ONCE(*x, 1);
|
||||
spin_unlock(lck);
|
||||
}
|
||||
|
||||
P1(int *x, atomic_t *y, spinlock_t *lck)
|
||||
{
|
||||
int r0;
|
||||
int r1;
|
||||
int r2;
|
||||
|
||||
r0 = READ_ONCE(*x);
|
||||
r1 = READ_ONCE(*x);
|
||||
spin_lock(lck);
|
||||
r2 = atomic_inc_return(y);
|
||||
spin_unlock(lck);
|
||||
}
|
||||
|
||||
locations [x;0:r2;1:r0;1:r1;1:r2]
|
||||
filter (1:r0=0 /\ 1:r1=1)
|
||||
exists (1:r2=1)
|
||||
@ -1028,32 +1028,7 @@ Limitations of the Linux-kernel memory model (LKMM) include:
|
||||
additional call_rcu() process to the site of the
|
||||
emulated rcu-barrier().
|
||||
|
||||
e. Although sleepable RCU (SRCU) is now modeled, there
|
||||
are some subtle differences between its semantics and
|
||||
those in the Linux kernel. For example, the kernel
|
||||
might interpret the following sequence as two partially
|
||||
overlapping SRCU read-side critical sections:
|
||||
|
||||
1 r1 = srcu_read_lock(&my_srcu);
|
||||
2 do_something_1();
|
||||
3 r2 = srcu_read_lock(&my_srcu);
|
||||
4 do_something_2();
|
||||
5 srcu_read_unlock(&my_srcu, r1);
|
||||
6 do_something_3();
|
||||
7 srcu_read_unlock(&my_srcu, r2);
|
||||
|
||||
In contrast, LKMM will interpret this as a nested pair of
|
||||
SRCU read-side critical sections, with the outer critical
|
||||
section spanning lines 1-7 and the inner critical section
|
||||
spanning lines 3-5.
|
||||
|
||||
This difference would be more of a concern had anyone
|
||||
identified a reasonable use case for partially overlapping
|
||||
SRCU read-side critical sections. For more information
|
||||
on the trickiness of such overlapping, please see:
|
||||
https://paulmck.livejournal.com/40593.html
|
||||
|
||||
f. Reader-writer locking is not modeled. It can be
|
||||
e. Reader-writer locking is not modeled. It can be
|
||||
emulated in litmus tests using atomic read-modify-write
|
||||
operations.
|
||||
|
||||
|
||||
298
tools/memory-model/Documentation/locking.txt
Normal file
298
tools/memory-model/Documentation/locking.txt
Normal file
@ -0,0 +1,298 @@
|
||||
Locking
|
||||
=======
|
||||
|
||||
Locking is well-known and the common use cases are straightforward: Any
|
||||
CPU holding a given lock sees any changes previously seen or made by any
|
||||
CPU before it previously released that same lock. This last sentence
|
||||
is the only part of this document that most developers will need to read.
|
||||
|
||||
However, developers who would like to also access lock-protected shared
|
||||
variables outside of their corresponding locks should continue reading.
|
||||
|
||||
|
||||
Locking and Prior Accesses
|
||||
--------------------------
|
||||
|
||||
The basic rule of locking is worth repeating:
|
||||
|
||||
Any CPU holding a given lock sees any changes previously seen
|
||||
or made by any CPU before it previously released that same lock.
|
||||
|
||||
Note that this statement is a bit stronger than "Any CPU holding a
|
||||
given lock sees all changes made by any CPU during the time that CPU was
|
||||
previously holding this same lock". For example, consider the following
|
||||
pair of code fragments:
|
||||
|
||||
/* See MP+polocks.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
WRITE_ONCE(x, 1);
|
||||
spin_lock(&mylock);
|
||||
WRITE_ONCE(y, 1);
|
||||
spin_unlock(&mylock);
|
||||
}
|
||||
|
||||
void CPU1(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
r0 = READ_ONCE(y);
|
||||
spin_unlock(&mylock);
|
||||
r1 = READ_ONCE(x);
|
||||
}
|
||||
|
||||
The basic rule guarantees that if CPU0() acquires mylock before CPU1(),
|
||||
then both r0 and r1 must be set to the value 1. This also has the
|
||||
consequence that if the final value of r0 is equal to 1, then the final
|
||||
value of r1 must also be equal to 1. In contrast, the weaker rule would
|
||||
say nothing about the final value of r1.
|
||||
|
||||
|
||||
Locking and Subsequent Accesses
|
||||
-------------------------------
|
||||
|
||||
The converse to the basic rule also holds: Any CPU holding a given
|
||||
lock will not see any changes that will be made by any CPU after it
|
||||
subsequently acquires this same lock. This converse statement is
|
||||
illustrated by the following litmus test:
|
||||
|
||||
/* See MP+porevlocks.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
r0 = READ_ONCE(y);
|
||||
spin_lock(&mylock);
|
||||
r1 = READ_ONCE(x);
|
||||
spin_unlock(&mylock);
|
||||
}
|
||||
|
||||
void CPU1(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
WRITE_ONCE(x, 1);
|
||||
spin_unlock(&mylock);
|
||||
WRITE_ONCE(y, 1);
|
||||
}
|
||||
|
||||
This converse to the basic rule guarantees that if CPU0() acquires
|
||||
mylock before CPU1(), then both r0 and r1 must be set to the value 0.
|
||||
This also has the consequence that if the final value of r1 is equal
|
||||
to 0, then the final value of r0 must also be equal to 0. In contrast,
|
||||
the weaker rule would say nothing about the final value of r0.
|
||||
|
||||
These examples show only a single pair of CPUs, but the effects of the
|
||||
locking basic rule extend across multiple acquisitions of a given lock
|
||||
across multiple CPUs.
|
||||
|
||||
|
||||
Double-Checked Locking
|
||||
----------------------
|
||||
|
||||
It is well known that more than just a lock is required to make
|
||||
double-checked locking work correctly, This litmus test illustrates
|
||||
one incorrect approach:
|
||||
|
||||
/* See Documentation/litmus-tests/locking/DCL-broken.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
r0 = READ_ONCE(flag);
|
||||
if (r0 == 0) {
|
||||
spin_lock(&lck);
|
||||
r1 = READ_ONCE(flag);
|
||||
if (r1 == 0) {
|
||||
WRITE_ONCE(data, 1);
|
||||
WRITE_ONCE(flag, 1);
|
||||
}
|
||||
spin_unlock(&lck);
|
||||
}
|
||||
r2 = READ_ONCE(data);
|
||||
}
|
||||
/* CPU1() is the exactly the same as CPU0(). */
|
||||
|
||||
There are two problems. First, there is no ordering between the first
|
||||
READ_ONCE() of "flag" and the READ_ONCE() of "data". Second, there is
|
||||
no ordering between the two WRITE_ONCE() calls. It should therefore be
|
||||
no surprise that "r2" can be zero, and a quick herd7 run confirms this.
|
||||
|
||||
One way to fix this is to use smp_load_acquire() and smp_store_release()
|
||||
as shown in this corrected version:
|
||||
|
||||
/* See Documentation/litmus-tests/locking/DCL-fixed.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
r0 = smp_load_acquire(&flag);
|
||||
if (r0 == 0) {
|
||||
spin_lock(&lck);
|
||||
r1 = READ_ONCE(flag);
|
||||
if (r1 == 0) {
|
||||
WRITE_ONCE(data, 1);
|
||||
smp_store_release(&flag, 1);
|
||||
}
|
||||
spin_unlock(&lck);
|
||||
}
|
||||
r2 = READ_ONCE(data);
|
||||
}
|
||||
/* CPU1() is the exactly the same as CPU0(). */
|
||||
|
||||
The smp_load_acquire() guarantees that its load from "flags" will
|
||||
be ordered before the READ_ONCE() from data, thus solving the first
|
||||
problem. The smp_store_release() guarantees that its store will be
|
||||
ordered after the WRITE_ONCE() to "data", solving the second problem.
|
||||
The smp_store_release() pairs with the smp_load_acquire(), thus ensuring
|
||||
that the ordering provided by each actually takes effect. Again, a
|
||||
quick herd7 run confirms this.
|
||||
|
||||
In short, if you access a lock-protected variable without holding the
|
||||
corresponding lock, you will need to provide additional ordering, in
|
||||
this case, via the smp_load_acquire() and the smp_store_release().
|
||||
|
||||
|
||||
Ordering Provided by a Lock to CPUs Not Holding That Lock
|
||||
---------------------------------------------------------
|
||||
|
||||
It is not necessarily the case that accesses ordered by locking will be
|
||||
seen as ordered by CPUs not holding that lock. Consider this example:
|
||||
|
||||
/* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
WRITE_ONCE(x, 1);
|
||||
WRITE_ONCE(y, 1);
|
||||
spin_unlock(&mylock);
|
||||
}
|
||||
|
||||
void CPU1(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
r0 = READ_ONCE(y);
|
||||
WRITE_ONCE(z, 1);
|
||||
spin_unlock(&mylock);
|
||||
}
|
||||
|
||||
void CPU2(void)
|
||||
{
|
||||
WRITE_ONCE(z, 2);
|
||||
smp_mb();
|
||||
r1 = READ_ONCE(x);
|
||||
}
|
||||
|
||||
Counter-intuitive though it might be, it is quite possible to have
|
||||
the final value of r0 be 1, the final value of z be 2, and the final
|
||||
value of r1 be 0. The reason for this surprising outcome is that CPU2()
|
||||
never acquired the lock, and thus did not fully benefit from the lock's
|
||||
ordering properties.
|
||||
|
||||
Ordering can be extended to CPUs not holding the lock by careful use
|
||||
of smp_mb__after_spinlock():
|
||||
|
||||
/* See Z6.0+pooncelock+poonceLock+pombonce.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
WRITE_ONCE(x, 1);
|
||||
WRITE_ONCE(y, 1);
|
||||
spin_unlock(&mylock);
|
||||
}
|
||||
|
||||
void CPU1(void)
|
||||
{
|
||||
spin_lock(&mylock);
|
||||
smp_mb__after_spinlock();
|
||||
r0 = READ_ONCE(y);
|
||||
WRITE_ONCE(z, 1);
|
||||
spin_unlock(&mylock);
|
||||
}
|
||||
|
||||
void CPU2(void)
|
||||
{
|
||||
WRITE_ONCE(z, 2);
|
||||
smp_mb();
|
||||
r1 = READ_ONCE(x);
|
||||
}
|
||||
|
||||
This addition of smp_mb__after_spinlock() strengthens the lock
|
||||
acquisition sufficiently to rule out the counter-intuitive outcome.
|
||||
In other words, the addition of the smp_mb__after_spinlock() prohibits
|
||||
the counter-intuitive result where the final value of r0 is 1, the final
|
||||
value of z is 2, and the final value of r1 is 0.
|
||||
|
||||
|
||||
No Roach-Motel Locking!
|
||||
-----------------------
|
||||
|
||||
This example requires familiarity with the herd7 "filter" clause, so
|
||||
please read up on that topic in litmus-tests.txt.
|
||||
|
||||
It is tempting to allow memory-reference instructions to be pulled
|
||||
into a critical section, but this cannot be allowed in the general case.
|
||||
For example, consider a spin loop preceding a lock-based critical section.
|
||||
Now, herd7 does not model spin loops, but we can emulate one with two
|
||||
loads, with a "filter" clause to constrain the first to return the
|
||||
initial value and the second to return the updated value, as shown below:
|
||||
|
||||
/* See Documentation/litmus-tests/locking/RM-fixed.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
spin_lock(&lck);
|
||||
r2 = atomic_inc_return(&y);
|
||||
WRITE_ONCE(x, 1);
|
||||
spin_unlock(&lck);
|
||||
}
|
||||
|
||||
void CPU1(void)
|
||||
{
|
||||
r0 = READ_ONCE(x);
|
||||
r1 = READ_ONCE(x);
|
||||
spin_lock(&lck);
|
||||
r2 = atomic_inc_return(&y);
|
||||
spin_unlock(&lck);
|
||||
}
|
||||
|
||||
filter (1:r0=0 /\ 1:r1=1)
|
||||
exists (1:r2=1)
|
||||
|
||||
The variable "x" is the control variable for the emulated spin loop.
|
||||
CPU0() sets it to "1" while holding the lock, and CPU1() emulates the
|
||||
spin loop by reading it twice, first into "1:r0" (which should get the
|
||||
initial value "0") and then into "1:r1" (which should get the updated
|
||||
value "1").
|
||||
|
||||
The "filter" clause takes this into account, constraining "1:r0" to
|
||||
equal "0" and "1:r1" to equal 1.
|
||||
|
||||
Then the "exists" clause checks to see if CPU1() acquired its lock first,
|
||||
which should not happen given the filter clause because CPU0() updates
|
||||
"x" while holding the lock. And herd7 confirms this.
|
||||
|
||||
But suppose that the compiler was permitted to reorder the spin loop
|
||||
into CPU1()'s critical section, like this:
|
||||
|
||||
/* See Documentation/litmus-tests/locking/RM-broken.litmus. */
|
||||
void CPU0(void)
|
||||
{
|
||||
int r2;
|
||||
|
||||
spin_lock(&lck);
|
||||
r2 = atomic_inc_return(&y);
|
||||
WRITE_ONCE(x, 1);
|
||||
spin_unlock(&lck);
|
||||
}
|
||||
|
||||
void CPU1(void)
|
||||
{
|
||||
spin_lock(&lck);
|
||||
r0 = READ_ONCE(x);
|
||||
r1 = READ_ONCE(x);
|
||||
r2 = atomic_inc_return(&y);
|
||||
spin_unlock(&lck);
|
||||
}
|
||||
|
||||
filter (1:r0=0 /\ 1:r1=1)
|
||||
exists (1:r2=1)
|
||||
|
||||
If "1:r0" is equal to "0", "1:r1" can never equal "1" because CPU0()
|
||||
cannot update "x" while CPU1() holds the lock. And herd7 confirms this,
|
||||
showing zero executions matching the "filter" criteria.
|
||||
|
||||
And this is why Linux-kernel lock and unlock primitives must prevent
|
||||
code from entering critical sections. It is not sufficient to only
|
||||
prevent code from leaving them.
|
||||
2
tools/memory-model/litmus-tests/.gitignore
vendored
2
tools/memory-model/litmus-tests/.gitignore
vendored
@ -1,2 +1,2 @@
|
||||
# SPDX-License-Identifier: GPL-2.0-only
|
||||
*.litmus.out
|
||||
*.litmus.*
|
||||
|
||||
@ -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
|
||||
|
||||
@ -43,10 +51,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
|
||||
|
||||
@ -68,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.
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
#!/bin/sh
|
||||
#!/bin/bash
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Run herd7 tests on all .litmus files in the litmus-tests directory
|
||||
@ -8,6 +8,11 @@
|
||||
# "^^^". It also outputs verification results to a file whose name is
|
||||
# that of the specified litmus test, but with ".out" appended.
|
||||
#
|
||||
# If the --hw argument is specified, this script translates the .litmus
|
||||
# C-language file to the specified type of assembly and verifies that.
|
||||
# But in this case, litmus tests using complex synchronization (such as
|
||||
# locking, RCU, and SRCU) are cheerfully ignored.
|
||||
#
|
||||
# Usage:
|
||||
# checkalllitmus.sh
|
||||
#
|
||||
@ -17,7 +22,7 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
. scripts/parseargs.sh
|
||||
|
||||
@ -30,29 +35,23 @@ else
|
||||
exit 255
|
||||
fi
|
||||
|
||||
# Create any new directories that have appeared in the github litmus
|
||||
# repo since the last run.
|
||||
# Create any new directories that have appeared in the litmus-tests
|
||||
# directory since the last run.
|
||||
if test "$LKMM_DESTDIR" != "."
|
||||
then
|
||||
find $litmusdir -type d -print |
|
||||
( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
|
||||
fi
|
||||
|
||||
# Find the checklitmus script. If it is not where we expect it, then
|
||||
# assume that the caller has the PATH environment variable set
|
||||
# appropriately.
|
||||
if test -x scripts/checklitmus.sh
|
||||
then
|
||||
clscript=scripts/checklitmus.sh
|
||||
else
|
||||
clscript=checklitmus.sh
|
||||
fi
|
||||
|
||||
# Run the script on all the litmus tests in the specified directory
|
||||
ret=0
|
||||
for i in $litmusdir/*.litmus
|
||||
do
|
||||
if ! $clscript $i
|
||||
if test -n "$LKMM_HW_MAP_FILE" && ! scripts/simpletest.sh $i
|
||||
then
|
||||
continue
|
||||
fi
|
||||
if ! scripts/checklitmus.sh $i
|
||||
then
|
||||
ret=1
|
||||
fi
|
||||
|
||||
@ -10,6 +10,7 @@
|
||||
# parseargs.sh scripts for arguments.
|
||||
|
||||
. scripts/parseargs.sh
|
||||
. scripts/hwfnseg.sh
|
||||
|
||||
T=/tmp/checkghlitmus.sh.$$
|
||||
trap 'rm -rf $T' 0
|
||||
@ -32,19 +33,19 @@ then
|
||||
( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
|
||||
fi
|
||||
|
||||
# Create a list of the C-language litmus tests previously run.
|
||||
( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
|
||||
sed -e 's/\.out$//' |
|
||||
xargs -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' |
|
||||
# Create a list of the specified litmus tests previously run.
|
||||
( cd $LKMM_DESTDIR; find litmus -name "*.litmus${hwfnseg}.out" -print ) |
|
||||
sed -e "s/${hwfnseg}"'\.out$//' |
|
||||
xargs -r grep -E -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' |
|
||||
xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
|
||||
|
||||
# Create a list of C-language litmus tests with "Result:" commands and
|
||||
# no more than the specified number of processes.
|
||||
find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
|
||||
xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result
|
||||
find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C
|
||||
xargs < $T/list-C -r grep -E -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result
|
||||
xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short
|
||||
|
||||
# Form list of tests without corresponding .litmus.out files
|
||||
# Form list of tests without corresponding .out files
|
||||
sort $T/list-C-already $T/list-C-result-short | uniq -u > $T/list-C-needed
|
||||
|
||||
# Run any needed tests.
|
||||
|
||||
@ -1,10 +1,8 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Run a herd7 test and invokes judgelitmus.sh to check the result against
|
||||
# a "Result:" comment within the litmus test. It also outputs verification
|
||||
# results to a file whose name is that of the specified litmus test, but
|
||||
# with ".out" appended.
|
||||
# Invokes runlitmus.sh and judgelitmus.sh on its arguments to run the
|
||||
# specified litmus test and pass judgment on the results.
|
||||
#
|
||||
# Usage:
|
||||
# checklitmus.sh file.litmus
|
||||
@ -15,20 +13,7 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
litmus=$1
|
||||
herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
|
||||
|
||||
if test -f "$litmus" -a -r "$litmus"
|
||||
then
|
||||
:
|
||||
else
|
||||
echo ' --- ' error: \"$litmus\" is not a readable file
|
||||
exit 255
|
||||
fi
|
||||
|
||||
echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
|
||||
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
|
||||
|
||||
scripts/judgelitmus.sh $litmus
|
||||
scripts/runlitmus.sh $1
|
||||
scripts/judgelitmus.sh $1
|
||||
|
||||
@ -12,7 +12,7 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
. scripts/parseargs.sh
|
||||
|
||||
|
||||
43
tools/memory-model/scripts/checktheselitmus.sh
Executable file
43
tools/memory-model/scripts/checktheselitmus.sh
Executable file
@ -0,0 +1,43 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Invokes checklitmus.sh on its arguments to run the specified litmus
|
||||
# test and pass judgment on the results.
|
||||
#
|
||||
# Usage:
|
||||
# checktheselitmus.sh -- [ file1.litmus [ file2.litmus ... ] ]
|
||||
#
|
||||
# Run this in the directory containing the memory model, specifying the
|
||||
# pathname of the litmus test to check. The usual parseargs.sh arguments
|
||||
# can be specified prior to the "--".
|
||||
#
|
||||
# This script is intended for use with pathnames that start from the
|
||||
# tools/memory-model directory. If some of the pathnames instead start at
|
||||
# the root directory, they all must do so and the "--destdir /" parseargs.sh
|
||||
# argument must be specified prior to the "--". Alternatively, some other
|
||||
# "--destdir" argument can be supplied as long as the needed subdirectories
|
||||
# are populated.
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
. scripts/parseargs.sh
|
||||
|
||||
ret=0
|
||||
for i in "$@"
|
||||
do
|
||||
if scripts/checklitmus.sh $i
|
||||
then
|
||||
:
|
||||
else
|
||||
ret=1
|
||||
fi
|
||||
done
|
||||
if test "$ret" -ne 0
|
||||
then
|
||||
echo " ^^^ VERIFICATION MISMATCHES" 1>&2
|
||||
else
|
||||
echo All litmus tests verified as was expected. 1>&2
|
||||
fi
|
||||
exit $ret
|
||||
@ -12,12 +12,49 @@ trap 'rm -rf $T' 0
|
||||
mkdir $T
|
||||
|
||||
# comparetest oldpath newpath
|
||||
badmacnam=0
|
||||
timedout=0
|
||||
perfect=0
|
||||
obsline=0
|
||||
noobsline=0
|
||||
obsresult=0
|
||||
badcompare=0
|
||||
comparetest () {
|
||||
if grep -q ': Unknown macro ' $1 || grep -q ': Unknown macro ' $2
|
||||
then
|
||||
if grep -q ': Unknown macro ' $1
|
||||
then
|
||||
badname=`grep ': Unknown macro ' $1 |
|
||||
sed -e 's/^.*: Unknown macro //' |
|
||||
sed -e 's/ (User error).*$//'`
|
||||
echo 'Current LKMM version does not know "'$badname'"' $1
|
||||
fi
|
||||
if grep -q ': Unknown macro ' $2
|
||||
then
|
||||
badname=`grep ': Unknown macro ' $2 |
|
||||
sed -e 's/^.*: Unknown macro //' |
|
||||
sed -e 's/ (User error).*$//'`
|
||||
echo 'Current LKMM version does not know "'$badname'"' $2
|
||||
fi
|
||||
badmacnam=`expr "$badmacnam" + 1`
|
||||
return 0
|
||||
elif grep -q '^Command exited with non-zero status 124' $1 ||
|
||||
grep -q '^Command exited with non-zero status 124' $2
|
||||
then
|
||||
if grep -q '^Command exited with non-zero status 124' $1 &&
|
||||
grep -q '^Command exited with non-zero status 124' $2
|
||||
then
|
||||
echo Both runs timed out: $2
|
||||
elif grep -q '^Command exited with non-zero status 124' $1
|
||||
then
|
||||
echo Old run timed out: $2
|
||||
elif grep -q '^Command exited with non-zero status 124' $2
|
||||
then
|
||||
echo New run timed out: $2
|
||||
fi
|
||||
timedout=`expr "$timedout" + 1`
|
||||
return 0
|
||||
fi
|
||||
grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout
|
||||
grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout
|
||||
if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1
|
||||
@ -38,7 +75,7 @@ comparetest () {
|
||||
return 0
|
||||
fi
|
||||
else
|
||||
echo Missing Observation line "(e.g., herd7 timeout)": $2
|
||||
echo Missing Observation line "(e.g., syntax error)": $2
|
||||
noobsline=`expr "$noobsline" + 1`
|
||||
return 0
|
||||
fi
|
||||
@ -72,12 +109,20 @@ then
|
||||
fi
|
||||
if test "$noobsline" -ne 0
|
||||
then
|
||||
echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2
|
||||
echo Missing Observation line "(e.g., syntax error)": $noobsline 1>&2
|
||||
fi
|
||||
if test "$obsresult" -ne 0
|
||||
then
|
||||
echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2
|
||||
fi
|
||||
if test "$timedout" -ne 0
|
||||
then
|
||||
echo "!!!" Timed out: $timedout 1>&2
|
||||
fi
|
||||
if test "$badmacnam" -ne 0
|
||||
then
|
||||
echo "!!!" Unknown primitive: $badmacnam 1>&2
|
||||
fi
|
||||
if test "$badcompare" -ne 0
|
||||
then
|
||||
echo "!!!" Result changed: $badcompare 1>&2
|
||||
|
||||
20
tools/memory-model/scripts/hwfnseg.sh
Executable file
20
tools/memory-model/scripts/hwfnseg.sh
Executable file
@ -0,0 +1,20 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Generate the hardware extension to the litmus-test filename, or the
|
||||
# empty string if this is an LKMM run. The extension is placed in
|
||||
# the shell variable hwfnseg.
|
||||
#
|
||||
# Usage:
|
||||
# . hwfnseg.sh
|
||||
#
|
||||
# Copyright IBM Corporation, 2019
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
if test -z "$LKMM_HW_MAP_FILE"
|
||||
then
|
||||
hwfnseg=
|
||||
else
|
||||
hwfnseg=".$LKMM_HW_MAP_FILE"
|
||||
fi
|
||||
@ -60,7 +60,7 @@ fi
|
||||
|
||||
# Create a list of the C-language litmus tests with no more than the
|
||||
# specified number of processes (per the --procs argument).
|
||||
find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
|
||||
find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C
|
||||
xargs < $T/list-C -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
|
||||
|
||||
scripts/runlitmushist.sh < $T/list-C-short
|
||||
|
||||
@ -1,9 +1,22 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Given a .litmus test and the corresponding .litmus.out file, check
|
||||
# the .litmus.out file against the "Result:" comment to judge whether
|
||||
# the test ran correctly.
|
||||
# Given a .litmus test and the corresponding litmus output file, check
|
||||
# the .litmus.out file against the "Result:" comment to judge whether the
|
||||
# test ran correctly. If the --hw argument is omitted, check against the
|
||||
# LKMM output, which is assumed to be in file.litmus.out. If either a
|
||||
# "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker
|
||||
# in the LKMM output is present, the other must also be as well, at least
|
||||
# for litmus tests having a "Result:" comment. In this case, a failure of
|
||||
# the Always/Sometimes/Never portion of the "Result:" prediction will be
|
||||
# noted, but forgiven.
|
||||
#
|
||||
# If the --hw argument is provided, this is assumed to be a hardware
|
||||
# test, and the output is assumed to be in file.litmus.HW.out, where
|
||||
# "HW" is the --hw argument. In addition, non-Sometimes verification
|
||||
# results will be noted, but forgiven. Furthermore, if there is no
|
||||
# "Result:" comment but there is an LKMM .litmus.out file, the observation
|
||||
# in that file will be used to judge the assembly-language verification.
|
||||
#
|
||||
# Usage:
|
||||
# judgelitmus.sh file.litmus
|
||||
@ -13,7 +26,7 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
litmus=$1
|
||||
|
||||
@ -24,55 +37,120 @@ else
|
||||
echo ' --- ' error: \"$litmus\" is not a readable file
|
||||
exit 255
|
||||
fi
|
||||
if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
|
||||
if test -z "$LKMM_HW_MAP_FILE"
|
||||
then
|
||||
litmusout=$litmus.out
|
||||
lkmmout=
|
||||
else
|
||||
litmusout="`echo $litmus |
|
||||
sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out"
|
||||
lkmmout=$litmus.out
|
||||
fi
|
||||
if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
|
||||
then
|
||||
:
|
||||
else
|
||||
echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
|
||||
echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
|
||||
exit 255
|
||||
fi
|
||||
if grep -q '^ \* Result: ' $litmus
|
||||
if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
|
||||
then
|
||||
outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
|
||||
datarace_modeled=1
|
||||
fi
|
||||
if grep -q '^[( ]\* Result: ' $litmus
|
||||
then
|
||||
outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'`
|
||||
if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus
|
||||
then
|
||||
datarace_predicted=1
|
||||
fi
|
||||
if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"
|
||||
then
|
||||
echo '!!! Predicted data race not modeled' $litmus
|
||||
exit 252
|
||||
elif test -z "$datarace_predicted" -a -n "$datarace_modeled"
|
||||
then
|
||||
# Note that hardware models currently don't model data races
|
||||
echo '!!! Unexpected data race modeled' $litmus
|
||||
exit 253
|
||||
fi
|
||||
elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
|
||||
then
|
||||
outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
|
||||
else
|
||||
outcome=specified
|
||||
fi
|
||||
|
||||
grep '^Observation' $LKMM_DESTDIR/$litmus.out
|
||||
if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
|
||||
grep '^Observation' $LKMM_DESTDIR/$litmusout
|
||||
if grep -q '^Observation' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
:
|
||||
elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |
|
||||
sed -e 's/^.*: Unknown macro //' |
|
||||
sed -e 's/ (User error).*$//'`
|
||||
badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"
|
||||
echo $badmsg
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1
|
||||
fi
|
||||
exit 254
|
||||
elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo ' !!! Timeout' $litmus
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1
|
||||
fi
|
||||
exit 124
|
||||
else
|
||||
echo ' !!! Verification error' $litmus
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
|
||||
echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1
|
||||
fi
|
||||
exit 255
|
||||
fi
|
||||
if test "$outcome" = DEADLOCK
|
||||
then
|
||||
if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
|
||||
if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
|
||||
then
|
||||
ret=0
|
||||
else
|
||||
echo " !!! Unexpected non-$outcome verification" $litmus
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
|
||||
echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
|
||||
fi
|
||||
ret=1
|
||||
fi
|
||||
elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
|
||||
elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
|
||||
then
|
||||
echo " !!! Unexpected non-$outcome deadlock" $litmus
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1
|
||||
fi
|
||||
ret=1
|
||||
elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe
|
||||
then
|
||||
ret=0
|
||||
else
|
||||
echo " !!! Unexpected non-$outcome verification" $litmus
|
||||
if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
|
||||
if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled"
|
||||
then
|
||||
echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
|
||||
flag="--- Forgiven"
|
||||
ret=0
|
||||
else
|
||||
flag="!!! Unexpected"
|
||||
ret=1
|
||||
fi
|
||||
echo " $flag non-$outcome verification" $litmus
|
||||
if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout
|
||||
then
|
||||
echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
|
||||
fi
|
||||
ret=1
|
||||
fi
|
||||
tail -2 $LKMM_DESTDIR/$litmus.out | head -1
|
||||
tail -2 $LKMM_DESTDIR/$litmusout | head -1
|
||||
exit $ret
|
||||
|
||||
@ -12,7 +12,7 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
. scripts/parseargs.sh
|
||||
|
||||
@ -43,7 +43,7 @@ fi
|
||||
|
||||
# Form full list of litmus tests with no more than the specified
|
||||
# number of processes (per the --procs argument).
|
||||
find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C-all
|
||||
find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C-all
|
||||
xargs < $T/list-C-all -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
|
||||
|
||||
# Form list of new tests. Note: This does not handle litmus-test deletion!
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# the corresponding .litmus.out file, and does not judge the result.
|
||||
# Parse arguments common to the various scripts.
|
||||
#
|
||||
# . scripts/parseargs.sh
|
||||
#
|
||||
@ -9,7 +9,7 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
T=/tmp/parseargs.sh.$$
|
||||
mkdir $T
|
||||
@ -27,6 +27,7 @@ initparam () {
|
||||
|
||||
initparam LKMM_DESTDIR "."
|
||||
initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg"
|
||||
initparam LKMM_HW_MAP_FILE ""
|
||||
initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN`
|
||||
initparam LKMM_PROCS "3"
|
||||
initparam LKMM_TIMEOUT "1m"
|
||||
@ -37,10 +38,11 @@ usagehelp () {
|
||||
echo "Usage $scriptname [ arguments ]"
|
||||
echo " --destdir path (place for .litmus.out, default by .litmus)"
|
||||
echo " --herdopts -conf linux-kernel.cfg ..."
|
||||
echo " --hw AArch64"
|
||||
echo " --jobs N (number of jobs, default one per CPU)"
|
||||
echo " --procs N (litmus tests with at most this many processes)"
|
||||
echo " --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')"
|
||||
echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
|
||||
echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --hw '$LKMM_HW_MAP_FILE' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
|
||||
exit 1
|
||||
}
|
||||
|
||||
@ -81,7 +83,7 @@ do
|
||||
echo "Cannot create directory --destdir '$LKMM_DESTDIR'"
|
||||
usage
|
||||
fi
|
||||
if test -d "$LKMM_DESTDIR" -a -w "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR"
|
||||
if test -d "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR"
|
||||
then
|
||||
:
|
||||
else
|
||||
@ -95,6 +97,11 @@ do
|
||||
LKMM_HERD_OPTIONS="$2"
|
||||
shift
|
||||
;;
|
||||
--hw)
|
||||
checkarg --hw "(.map file architecture name)" "$#" "$2" '^[A-Za-z0-9_-]\+' '^--'
|
||||
LKMM_HW_MAP_FILE="$2"
|
||||
shift
|
||||
;;
|
||||
-j[1-9]*)
|
||||
njobs="`echo $1 | sed -e 's/^-j//'`"
|
||||
trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`"
|
||||
@ -106,7 +113,7 @@ do
|
||||
LKMM_JOBS="`echo $njobs | sed -e 's/^\([0-9]\+\).*$/\1/'`"
|
||||
;;
|
||||
--jobs|--job|-j)
|
||||
checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]\+$' '^--'
|
||||
checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]*$' '^--'
|
||||
LKMM_JOBS="$2"
|
||||
shift
|
||||
;;
|
||||
@ -120,6 +127,10 @@ do
|
||||
LKMM_TIMEOUT="$2"
|
||||
shift
|
||||
;;
|
||||
--)
|
||||
shift
|
||||
break
|
||||
;;
|
||||
*)
|
||||
echo Unknown argument $1
|
||||
usage
|
||||
|
||||
80
tools/memory-model/scripts/runlitmus.sh
Executable file
80
tools/memory-model/scripts/runlitmus.sh
Executable file
@ -0,0 +1,80 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Without the -hw argument, runs a herd7 test and outputs verification
|
||||
# results to a file whose name is that of the specified litmus test,
|
||||
# but with ".out" appended.
|
||||
#
|
||||
# If the --hw argument is specified, this script translates the .litmus
|
||||
# C-language file to the specified type of assembly and verifies that.
|
||||
# But in this case, litmus tests using complex synchronization (such as
|
||||
# locking, RCU, and SRCU) are cheerfully ignored.
|
||||
#
|
||||
# Either way, return the status of the herd7 command.
|
||||
#
|
||||
# Usage:
|
||||
# runlitmus.sh file.litmus
|
||||
#
|
||||
# Run this in the directory containing the memory model, specifying the
|
||||
# pathname of the litmus test to check. The caller is expected to have
|
||||
# properly set up the LKMM environment variables.
|
||||
#
|
||||
# Copyright IBM Corporation, 2019
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
litmus=$1
|
||||
if test -f "$litmus" -a -r "$litmus"
|
||||
then
|
||||
:
|
||||
else
|
||||
echo ' !!! ' error: \"$litmus\" is not a readable file
|
||||
exit 255
|
||||
fi
|
||||
|
||||
if test -z "$LKMM_HW_MAP_FILE" -o ! -e $LKMM_DESTDIR/$litmus.out
|
||||
then
|
||||
# LKMM run
|
||||
herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
|
||||
echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
|
||||
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
|
||||
ret=$?
|
||||
if test -z "$LKMM_HW_MAP_FILE"
|
||||
then
|
||||
exit $ret
|
||||
fi
|
||||
echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run
|
||||
fi
|
||||
|
||||
# Hardware run
|
||||
|
||||
T=/tmp/checklitmushw.sh.$$
|
||||
trap 'rm -rf $T' 0 2
|
||||
mkdir $T
|
||||
|
||||
# Generate filenames
|
||||
mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
|
||||
themefile="$T/${LKMM_HW_MAP_FILE}.theme"
|
||||
herdoptions="-model $LKMM_HW_CAT_FILE"
|
||||
hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`
|
||||
hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
|
||||
|
||||
# Don't run on litmus tests with complex synchronization
|
||||
if ! scripts/simpletest.sh $litmus
|
||||
then
|
||||
echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
|
||||
exit 254
|
||||
fi
|
||||
|
||||
# Generate the assembly code and run herd7 on it.
|
||||
gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
|
||||
jingle7 -v -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
|
||||
if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out
|
||||
then
|
||||
echo ' !!! ' jingle7 failed, errors in $hwlitmus.err
|
||||
cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err
|
||||
exit 253
|
||||
fi
|
||||
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
|
||||
|
||||
exit $?
|
||||
@ -13,7 +13,9 @@
|
||||
#
|
||||
# Copyright IBM Corporation, 2018
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
. scripts/hwfnseg.sh
|
||||
|
||||
T=/tmp/runlitmushist.sh.$$
|
||||
trap 'rm -rf $T' 0
|
||||
@ -30,15 +32,12 @@ fi
|
||||
# Prefixes for per-CPU scripts
|
||||
for ((i=0;i<$LKMM_JOBS;i++))
|
||||
do
|
||||
echo dir="$LKMM_DESTDIR" > $T/$i.sh
|
||||
echo T=$T >> $T/$i.sh
|
||||
echo herdoptions=\"$LKMM_HERD_OPTIONS\" >> $T/$i.sh
|
||||
cat << '___EOF___' >> $T/$i.sh
|
||||
runtest () {
|
||||
echo ' ... ' /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 '>' $dir/$1.out '2>&1'
|
||||
if /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 > $dir/$1.out 2>&1
|
||||
if scripts/runlitmus.sh $1
|
||||
then
|
||||
if ! grep -q '^Observation ' $dir/$1.out
|
||||
if ! grep -q '^Observation ' $LKMM_DESTDIR/$1$2.out
|
||||
then
|
||||
echo ' !!! Herd failed, no Observation:' $1
|
||||
fi
|
||||
@ -47,10 +46,16 @@ do
|
||||
if test "$exitcode" -eq 124
|
||||
then
|
||||
exitmsg="timed out"
|
||||
elif test "$exitcode" -eq 253
|
||||
then
|
||||
exitmsg=
|
||||
else
|
||||
exitmsg="failed, exit code $exitcode"
|
||||
fi
|
||||
echo ' !!! Herd' ${exitmsg}: $1
|
||||
if test -n "$exitmsg"
|
||||
then
|
||||
echo ' !!! Herd' ${exitmsg}: $1
|
||||
fi
|
||||
fi
|
||||
}
|
||||
___EOF___
|
||||
@ -59,11 +64,13 @@ done
|
||||
awk -v q="'" -v b='\\' '
|
||||
{
|
||||
print "echo `grep " q "^P[0-9]" b "+(" q " " $0 " | tail -1 | sed -e " q "s/^P" b "([0-9]" b "+" b ")(.*$/" b "1/" q "` " $0
|
||||
}' | bash |
|
||||
sort -k1n |
|
||||
awk -v ncpu=$LKMM_JOBS -v t=$T '
|
||||
}' | sh | sort -k1n |
|
||||
awk -v dq='"' -v hwfnseg="$hwfnseg" -v ncpu="$LKMM_JOBS" -v t="$T" '
|
||||
{
|
||||
print "runtest " $2 >> t "/" NR % ncpu ".sh";
|
||||
print "if test -z " dq hwfnseg dq " || scripts/simpletest.sh " dq $2 dq
|
||||
print "then"
|
||||
print "\techo runtest " dq $2 dq " " hwfnseg " >> " t "/" NR % ncpu ".sh";
|
||||
print "fi"
|
||||
}
|
||||
|
||||
END {
|
||||
|
||||
35
tools/memory-model/scripts/simpletest.sh
Executable file
35
tools/memory-model/scripts/simpletest.sh
Executable file
@ -0,0 +1,35 @@
|
||||
#!/bin/sh
|
||||
# SPDX-License-Identifier: GPL-2.0+
|
||||
#
|
||||
# Give zero status if this is a simple test and non-zero otherwise.
|
||||
# Simple tests do not contain locking, RCU, or SRCU.
|
||||
#
|
||||
# Usage:
|
||||
# simpletest.sh file.litmus
|
||||
#
|
||||
# Copyright IBM Corporation, 2019
|
||||
#
|
||||
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
|
||||
|
||||
|
||||
litmus=$1
|
||||
|
||||
if test -f "$litmus" -a -r "$litmus"
|
||||
then
|
||||
:
|
||||
else
|
||||
echo ' --- ' error: \"$litmus\" is not a readable file
|
||||
exit 255
|
||||
fi
|
||||
exclude="^[[:space:]]*\("
|
||||
exclude="${exclude}spin_lock(\|spin_unlock(\|spin_trylock(\|spin_is_locked("
|
||||
exclude="${exclude}\|rcu_read_lock(\|rcu_read_unlock("
|
||||
exclude="${exclude}\|synchronize_rcu(\|synchronize_rcu_expedited("
|
||||
exclude="${exclude}\|srcu_read_lock(\|srcu_read_unlock("
|
||||
exclude="${exclude}\|synchronize_srcu(\|synchronize_srcu_expedited("
|
||||
exclude="${exclude}\)"
|
||||
if grep -q $exclude $litmus
|
||||
then
|
||||
exit 255
|
||||
fi
|
||||
exit 0
|
||||
Loading…
Reference in New Issue
Block a user