Skip to content

Commit

Permalink
tools/memory-model: Add types to litmus tests
Browse files Browse the repository at this point in the history
This commit adds type information for global variables in the litmus
tests in order to allow easier use with klitmus7.

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
  • Loading branch information
Paul E. McKenney committed Nov 7, 2020
1 parent 0a27ce6 commit 1947bfc
Show file tree
Hide file tree
Showing 32 changed files with 130 additions and 31 deletions.
4 changes: 3 additions & 1 deletion tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ C CoRR+poonceonce+Once
* reads from the same variable are ordered.
*)

{}
{
int x;
}

P0(int *x)
{
Expand Down
4 changes: 3 additions & 1 deletion tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ C CoRW+poonceonce+Once
* a given variable and a later write to that same variable are ordered.
*)

{}
{
int x;
}

P0(int *x)
{
Expand Down
4 changes: 3 additions & 1 deletion tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ C CoWR+poonceonce+Once
* given variable and a later read from that same variable are ordered.
*)

{}
{
int x;
}

P0(int *x)
{
Expand Down
4 changes: 3 additions & 1 deletion tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ C CoWW+poonceonce
* writes to the same variable are ordered.
*)

{}
{
int x;
}

P0(int *x)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ C IRIW+fencembonceonces+OnceOnce
* process? This litmus test exercises LKMM's "propagation" rule.
*)

{}
{
int x;
int y;
}

P0(int *x)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ C IRIW+poonceonces+OnceOnce
* different process?
*)

{}
{
int x;
int y;
}

P0(int *x)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,12 @@ C ISA2+pooncelock+pooncelock+pombonce
* (in P0() and P1()) is visible to external process P2().
*)

{}
{
spinlock_t mylock;
int x;
int y;
int z;
}

P0(int *x, int *y, spinlock_t *mylock)
{
Expand Down
6 changes: 5 additions & 1 deletion tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,11 @@ C ISA2+poonceonces
* of the smp_load_acquire() invocations are replaced by READ_ONCE()?
*)

{}
{
int x;
int y;
int z;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,11 @@ C ISA2+pooncerelease+poacquirerelease+poacquireonce
* (AKA non-rf) link, so release-acquire is all that is needed.
*)

{}
{
int x;
int y;
int z;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,10 @@ C LB+fencembonceonce+ctrlonceonce
* another control dependency and order would still be maintained.)
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ C LB+poacquireonce+pooncerelease
* to the other?
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/LB+poonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,10 @@ C LB+poonceonces
* be prevented even with no explicit ordering?
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ C MP+fencewmbonceonce+fencermbonceonce
* is usually better to use smp_store_release() and smp_load_acquire().
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,9 @@ C MP+onceassign+derefonce
*)

{
y=z;
z=0;
int x;
int *y=z;
int z=0;
}

P0(int *x, int **y)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ C MP+polockmbonce+poacquiresilsil
*)

{
spinlock_t lo;
int x;
}

P0(spinlock_t *lo, int *x)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ C MP+polockonce+poacquiresilsil
*)

{
spinlock_t lo;
int x;
}

P0(spinlock_t *lo, int *x)
Expand Down
6 changes: 5 additions & 1 deletion tools/memory-model/litmus-tests/MP+polocks.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,11 @@ C MP+polocks
* to see all prior accesses by those other CPUs.
*)

{}
{
spinlock_t mylock;
int x;
int y;
}

P0(int *x, int *y, spinlock_t *mylock)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/MP+poonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,10 @@ C MP+poonceonces
* no ordering at all?
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ C MP+pooncerelease+poacquireonce
* pattern.
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
6 changes: 5 additions & 1 deletion tools/memory-model/litmus-tests/MP+porevlocks.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,11 @@ C MP+porevlocks
* see all prior accesses by those other CPUs.
*)

{}
{
spinlock_t mylock;
int x;
int y;
}

P0(int *x, int *y, spinlock_t *mylock)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/R+fencembonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@ C R+fencembonceonces
* cause the resulting test to be allowed.
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/R+poonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ C R+poonceonces
* store propagation delays.
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,10 @@ C S+fencewmbonceonce+poacquireonce
* store against a subsequent store?
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/S+poonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@ C S+poonceonces
* READ_ONCE(), is ordering preserved?
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@ C SB+fencembonceonces
* suffice, but not much else.)
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/SB+poonceonces.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ C SB+poonceonces
* variable that the preceding process reads.
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@ C SB+rfionceonce-poonceonces
* This litmus test demonstrates that LKMM is not fully multicopy atomic.
*)

{}
{
int x;
int y;
}

P0(int *x, int *y)
{
Expand Down
5 changes: 4 additions & 1 deletion tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ C WRC+poonceonces+Once
* test has no ordering at all.
*)

{}
{
int x;
int y;
}

P0(int *x)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ C WRC+pooncerelease+fencermbonceonce+Once
* is A-cumulative in LKMM.
*)

{}
{
int x;
int y;
}

P0(int *x)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,12 @@ C Z6.0+pooncelock+poonceLock+pombonce
* by CPUs not holding that lock.
*)

{}
{
spinlock_t mylock;
int x;
int y;
int z;
}

P0(int *x, int *y, spinlock_t *mylock)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,12 @@ C Z6.0+pooncelock+pooncelock+pombonce
* seen as ordered by a third process not holding that lock.
*)

{}
{
spinlock_t mylock;
int x;
int y;
int z;
}

P0(int *x, int *y, spinlock_t *mylock)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,11 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
* involving locking.)
*)

{}
{
int x;
int y;
int z;
}

P0(int *x, int *y)
{
Expand Down

0 comments on commit 1947bfc

Please sign in to comment.