Hello!
This series provides LKMM updates:
1. Document that the LKMM can easily miss control dependencies.
2. Move Documentation description to Documentation/README.
3. Document categories of ordering primitives.
4. Fix a typo in CPU MEMORY BARRIERS section.
5. Add a glossary of LKMM terms.
6. Add types to litmus tests.
7. Use "buf" and "flag" for message-passing tests.
8. Label MP tests' producers and consumers.
Thanx, Paul
------------------------------------------------------------------------
Documentation/memory-barriers.txt | 2
tools/memory-model/Documentation/README | 78 +
tools/memory-model/Documentation/control-dependencies.txt | 258 ++++
tools/memory-model/Documentation/glossary.txt | 155 ++
tools/memory-model/Documentation/litmus-tests.txt | 17
tools/memory-model/Documentation/ordering.txt | 557 ++++++++++
tools/memory-model/README | 22
tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4
tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4
tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus | 4
tools/memory-model/litmus-tests/CoWW+poonceonce.litmus | 4
tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus | 5
tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5
tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7
tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6
tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 6
tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus | 5
tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus | 5
tools/memory-model/litmus-tests/LB+poonceonces.litmus | 5
tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 27
tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 23
tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 8
tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 8
tools/memory-model/litmus-tests/MP+polocks.litmus | 28
tools/memory-model/litmus-tests/MP+poonceonces.litmus | 27
tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus | 27
tools/memory-model/litmus-tests/MP+porevlocks.litmus | 28
tools/memory-model/litmus-tests/R+fencembonceonces.litmus | 5
tools/memory-model/litmus-tests/R+poonceonces.litmus | 5
tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus | 5
tools/memory-model/litmus-tests/S+poonceonces.litmus | 5
tools/memory-model/litmus-tests/SB+fencembonceonces.litmus | 5
tools/memory-model/litmus-tests/SB+poonceonces.litmus | 5
tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus | 5
tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5
tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus | 5
tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus | 7
tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus | 7
tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6
39 files changed, 1267 insertions(+), 123 deletions(-)
From: "Paul E. McKenney" <[email protected]>
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 <[email protected]>
---
tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4 +++-
tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4 +++-
tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus | 4 +++-
tools/memory-model/litmus-tests/CoWW+poonceonce.litmus | 4 +++-
.../litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus | 5 ++++-
tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5 ++++-
.../litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6 +++++-
.../ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 6 +++++-
.../litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus | 5 ++++-
.../litmus-tests/LB+poacquireonce+pooncerelease.litmus | 5 ++++-
tools/memory-model/litmus-tests/LB+poonceonces.litmus | 5 ++++-
.../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 5 ++++-
tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 5 +++--
.../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 2 ++
.../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 2 ++
tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++++-
tools/memory-model/litmus-tests/MP+poonceonces.litmus | 5 ++++-
.../litmus-tests/MP+pooncerelease+poacquireonce.litmus | 5 ++++-
tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++++-
tools/memory-model/litmus-tests/R+fencembonceonces.litmus | 5 ++++-
tools/memory-model/litmus-tests/R+poonceonces.litmus | 5 ++++-
.../litmus-tests/S+fencewmbonceonce+poacquireonce.litmus | 5 ++++-
tools/memory-model/litmus-tests/S+poonceonces.litmus | 5 ++++-
tools/memory-model/litmus-tests/SB+fencembonceonces.litmus | 5 ++++-
tools/memory-model/litmus-tests/SB+poonceonces.litmus | 5 ++++-
tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus | 5 ++++-
tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5 ++++-
.../litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus | 5 ++++-
.../litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus | 7 ++++++-
.../litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
.../Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6 +++++-
32 files changed, 130 insertions(+), 31 deletions(-)
diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
index 967f9f2..772544f 100644
--- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
@@ -7,7 +7,9 @@ C CoRR+poonceonce+Once
* reads from the same variable are ordered.
*)
-{}
+{
+ int x;
+}
P0(int *x)
{
diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
index 4635739..5faae98 100644
--- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
index bb068c9..77c9cc9 100644
--- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
index 0d9f0a9..85ef746 100644
--- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
+++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
@@ -7,7 +7,9 @@ C CoWW+poonceonce
* writes to the same variable are ordered.
*)
-{}
+{
+ int x;
+}
P0(int *x)
{
diff --git a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
index e729d27..87aa900 100644
--- a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
@@ -10,7 +10,10 @@ C IRIW+fencembonceonces+OnceOnce
* process? This litmus test exercises LKMM's "propagation" rule.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x)
{
diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
index 4b54dd6..f84022d 100644
--- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
@@ -10,7 +10,10 @@ C IRIW+poonceonces+OnceOnce
* different process?
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x)
{
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
index 094d58d..398f624 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
index b321aa6..212a432 100644
--- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
index 025b046..7afd856 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
index 4727f5a..c8a93c7 100644
--- a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
+++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
index 07b9904..2fa0295 100644
--- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
+++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
@@ -8,7 +8,10 @@ C LB+poacquireonce+pooncerelease
* to the other?
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
index 74c49cb..2107306 100644
--- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
@@ -7,7 +7,10 @@ C LB+poonceonces
* be prevented even with no explicit ordering?
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
index a273da9..e04b71b 100644
--- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index 97731b4..18df682 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -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)
diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
index 50f4d62..b1b1266 100644
--- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
+++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
@@ -11,6 +11,8 @@ C MP+polockmbonce+poacquiresilsil
*)
{
+ spinlock_t lo;
+ int x;
}
P0(spinlock_t *lo, int *x)
diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
index abf81e7..867c75d 100644
--- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
+++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
@@ -11,6 +11,8 @@ C MP+polockonce+poacquiresilsil
*)
{
+ spinlock_t lo;
+ int x;
}
P0(spinlock_t *lo, int *x)
diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
index 712a4fcd..63e0f67 100644
--- a/tools/memory-model/litmus-tests/MP+polocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 172f014..68180a4 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -7,7 +7,10 @@ C MP+poonceonces
* no ordering at all?
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index d52c684..19f3e68 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -8,7 +8,10 @@ C MP+pooncerelease+poacquireonce
* pattern.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
index 72c9276..4ac189a 100644
--- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
index 222a0b8..af9463b 100644
--- a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
@@ -9,7 +9,10 @@ C R+fencembonceonces
* cause the resulting test to be allowed.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
index 5386f12..bcd5574e 100644
--- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
@@ -8,7 +8,10 @@ C R+poonceonces
* store propagation delays.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
index 1847982..c36341d 100644
--- a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
@@ -7,7 +7,10 @@ C S+fencewmbonceonce+poacquireonce
* store against a subsequent store?
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
index 8c9c2f8..7775c23 100644
--- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
@@ -9,7 +9,10 @@ C S+poonceonces
* READ_ONCE(), is ordering preserved?
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
index ed5fff1..833cdfe 100644
--- a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
@@ -9,7 +9,10 @@ C SB+fencembonceonces
* suffice, but not much else.)
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
index 10d5507..c92211e 100644
--- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
@@ -8,7 +8,10 @@ C SB+poonceonces
* variable that the preceding process reads.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x, int *y)
{
diff --git a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
index 04a1660..84344b4 100644
--- a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
index 6a2bc12..4314947 100644
--- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
@@ -8,7 +8,10 @@ C WRC+poonceonces+Once
* test has no ordering at all.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x)
{
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
index e994725..554999c 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
@@ -10,7 +10,10 @@ C WRC+pooncerelease+fencermbonceonce+Once
* is A-cumulative in LKMM.
*)
-{}
+{
+ int x;
+ int y;
+}
P0(int *x)
{
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
index 415248f..265a95f 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
index 10a2aa0..0c9aea8 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
@@ -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)
{
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
index 88e70b8..661f9aa 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
@@ -14,7 +14,11 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
* involving locking.)
*)
-{}
+{
+ int x;
+ int y;
+ int z;
+}
P0(int *x, int *y)
{
--
2.9.5
From: "Paul E. McKenney" <[email protected]>
This commit moves the descriptions of the files residing in
tools/memory-model/Documentation to a README file in that directory,
leaving behind the description of tools/memory-model/Documentation/README
itself. After this change, tools/memory-model/Documentation/README
provides a guide to the files in the tools/memory-model/Documentation
directory, guiding people with different skills and needs to the most
appropriate starting point.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/Documentation/README | 59 +++++++++++++++++++++++++++++++++
tools/memory-model/README | 22 ++----------
2 files changed, 61 insertions(+), 20 deletions(-)
create mode 100644 tools/memory-model/Documentation/README
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
new file mode 100644
index 0000000..2d9539f
--- /dev/null
+++ b/tools/memory-model/Documentation/README
@@ -0,0 +1,59 @@
+It has been said that successful communication requires first identifying
+what your audience knows and then building a bridge from their current
+knowledge to what they need to know. Unfortunately, the expected
+Linux-kernel memory model (LKMM) audience might be anywhere from novice
+to expert both in kernel hacking and in understanding LKMM.
+
+This document therefore points out a number of places to start reading,
+depending on what you know and what you would like to learn. Please note
+that the documents later in this list assume that the reader understands
+the material provided by documents earlier in this list.
+
+o You are new to Linux-kernel concurrency: simple.txt
+
+o You are familiar with the Linux-kernel concurrency primitives
+ that you need, and just want to get started with LKMM litmus
+ tests: litmus-tests.txt
+
+o You are familiar with Linux-kernel concurrency, and would
+ like a detailed intuitive understanding of LKMM, including
+ situations involving more than two threads: recipes.txt
+
+o You are familiar with Linux-kernel concurrency and the use of
+ LKMM, and would like a quick reference: cheatsheet.txt
+
+o You are familiar with Linux-kernel concurrency and the use
+ of LKMM, and would like to learn about LKMM's requirements,
+ rationale, and implementation: explanation.txt
+
+o You are interested in the publications related to LKMM, including
+ hardware manuals, academic literature, standards-committee
+ working papers, and LWN articles: references.txt
+
+
+====================
+DESCRIPTION OF FILES
+====================
+
+README
+ This file.
+
+cheatsheet.txt
+ Quick-reference guide to the Linux-kernel memory model.
+
+explanation.txt
+ Detailed description of the memory model.
+
+litmus-tests.txt
+ The format, features, capabilities, and limitations of the litmus
+ tests that LKMM can evaluate.
+
+recipes.txt
+ Common memory-ordering patterns.
+
+references.txt
+ Background information.
+
+simple.txt
+ Starting point for someone new to Linux-kernel concurrency.
+ And also a reminder of the simpler approaches to concurrency!
diff --git a/tools/memory-model/README b/tools/memory-model/README
index c8144d4..39d08d1 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -161,26 +161,8 @@ running LKMM litmus tests.
DESCRIPTION OF FILES
====================
-Documentation/cheatsheet.txt
- Quick-reference guide to the Linux-kernel memory model.
-
-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!
+Documentation/README
+ Guide to the other documents in the Documentation/ directory.
linux-kernel.bell
Categorizes the relevant instructions, including memory
--
2.9.5
From: "Paul E. McKenney" <[email protected]>
This commit adds comments that label the MP tests' producer and consumer
processes, and also that label the "exists" clause as the bad outcome.
Reported-by: Johannes Weiner <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
.../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 6 +++---
tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 6 +++---
.../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 6 +++---
.../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 6 +++---
tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++---
tools/memory-model/litmus-tests/MP+poonceonces.litmus | 6 +++---
.../memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus | 6 +++---
tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++---
8 files changed, 24 insertions(+), 24 deletions(-)
diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
index f15e501..c5c168d 100644
--- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
@@ -13,14 +13,14 @@ C MP+fencewmbonceonce+fencermbonceonce
int flag;
}
-P0(int *buf, int *flag)
+P0(int *buf, int *flag) // Producer
{
WRITE_ONCE(*buf, 1);
smp_wmb();
WRITE_ONCE(*flag, 1);
}
-P1(int *buf, int *flag)
+P1(int *buf, int *flag) // Consumer
{
int r0;
int r1;
@@ -30,4 +30,4 @@ P1(int *buf, int *flag)
r1 = READ_ONCE(*buf);
}
-exists (1:r0=1 /\ 1:r1=0)
+exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index ed8ee9b..20ff626 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -15,13 +15,13 @@ C MP+onceassign+derefonce
int y=0;
}
-P0(int *x, int **p)
+P0(int *x, int **p) // Producer
{
WRITE_ONCE(*x, 1);
rcu_assign_pointer(*p, x);
}
-P1(int *x, int **p)
+P1(int *x, int **p) // Consumer
{
int *r0;
int r1;
@@ -32,4 +32,4 @@ P1(int *x, int **p)
rcu_read_unlock();
}
-exists (1:r0=x /\ 1:r1=0)
+exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
index b1b1266..153917a 100644
--- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
+++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
@@ -15,7 +15,7 @@ C MP+polockmbonce+poacquiresilsil
int x;
}
-P0(spinlock_t *lo, int *x)
+P0(spinlock_t *lo, int *x) // Producer
{
spin_lock(lo);
smp_mb__after_spinlock();
@@ -23,7 +23,7 @@ P0(spinlock_t *lo, int *x)
spin_unlock(lo);
}
-P1(spinlock_t *lo, int *x)
+P1(spinlock_t *lo, int *x) // Consumer
{
int r1;
int r2;
@@ -34,4 +34,4 @@ P1(spinlock_t *lo, int *x)
r3 = spin_is_locked(lo);
}
-exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
+exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
index 867c75d..aad6439 100644
--- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
+++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
@@ -15,14 +15,14 @@ C MP+polockonce+poacquiresilsil
int x;
}
-P0(spinlock_t *lo, int *x)
+P0(spinlock_t *lo, int *x) // Producer
{
spin_lock(lo);
WRITE_ONCE(*x, 1);
spin_unlock(lo);
}
-P1(spinlock_t *lo, int *x)
+P1(spinlock_t *lo, int *x) // Consumer
{
int r1;
int r2;
@@ -33,4 +33,4 @@ P1(spinlock_t *lo, int *x)
r3 = spin_is_locked(lo);
}
-exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
+exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
index 4b0c2ed..21cbca6 100644
--- a/tools/memory-model/litmus-tests/MP+polocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
@@ -17,7 +17,7 @@ C MP+polocks
int flag;
}
-P0(int *buf, int *flag, spinlock_t *mylock)
+P0(int *buf, int *flag, spinlock_t *mylock) // Producer
{
WRITE_ONCE(*buf, 1);
spin_lock(mylock);
@@ -25,7 +25,7 @@ P0(int *buf, int *flag, spinlock_t *mylock)
spin_unlock(mylock);
}
-P1(int *buf, int *flag, spinlock_t *mylock)
+P1(int *buf, int *flag, spinlock_t *mylock) // Consumer
{
int r0;
int r1;
@@ -36,4 +36,4 @@ P1(int *buf, int *flag, spinlock_t *mylock)
r1 = READ_ONCE(*buf);
}
-exists (1:r0=1 /\ 1:r1=0)
+exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 3010bba..9f9769d 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -12,13 +12,13 @@ C MP+poonceonces
int flag;
}
-P0(int *buf, int *flag)
+P0(int *buf, int *flag) // Producer
{
WRITE_ONCE(*buf, 1);
WRITE_ONCE(*flag, 1);
}
-P1(int *buf, int *flag)
+P1(int *buf, int *flag) // Consumer
{
int r0;
int r1;
@@ -27,4 +27,4 @@ P1(int *buf, int *flag)
r1 = READ_ONCE(*buf);
}
-exists (1:r0=1 /\ 1:r1=0)
+exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index 21e825d..cbe28e7 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -13,13 +13,13 @@ C MP+pooncerelease+poacquireonce
int flag;
}
-P0(int *buf, int *flag)
+P0(int *buf, int *flag) // Producer
{
WRITE_ONCE(*buf, 1);
smp_store_release(flag, 1);
}
-P1(int *buf, int *flag)
+P1(int *buf, int *flag) // Consumer
{
int r0;
int r1;
@@ -28,4 +28,4 @@ P1(int *buf, int *flag)
r1 = READ_ONCE(*buf);
}
-exists (1:r0=1 /\ 1:r1=0)
+exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
index 9691d55..012041b 100644
--- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
@@ -17,7 +17,7 @@ C MP+porevlocks
int flag;
}
-P0(int *buf, int *flag, spinlock_t *mylock)
+P0(int *buf, int *flag, spinlock_t *mylock) // Consumer
{
int r0;
int r1;
@@ -28,7 +28,7 @@ P0(int *buf, int *flag, spinlock_t *mylock)
spin_unlock(mylock);
}
-P1(int *buf, int *flag, spinlock_t *mylock)
+P1(int *buf, int *flag, spinlock_t *mylock) // Producer
{
spin_lock(mylock);
WRITE_ONCE(*buf, 1);
@@ -36,4 +36,4 @@ P1(int *buf, int *flag, spinlock_t *mylock)
WRITE_ONCE(*flag, 1);
}
-exists (0:r0=1 /\ 0:r1=0)
+exists (0:r0=1 /\ 0:r1=0) (* Bad outcome. *)
--
2.9.5
From: "Paul E. McKenney" <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/Documentation/glossary.txt | 155 ++++++++++++++++++++++++++
1 file changed, 155 insertions(+)
create mode 100644 tools/memory-model/Documentation/glossary.txt
diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
new file mode 100644
index 0000000..036fa28
--- /dev/null
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -0,0 +1,155 @@
+This document contains brief definitions of LKMM-related terms. Like most
+glossaries, it is not intended to be read front to back (except perhaps
+as a way of confirming a diagnosis of OCD), but rather to be searched
+for specific terms.
+
+
+Address Dependency: When the address of a later memory access is computed
+ based on the value returned by an earlier load, an "address
+ dependency" extends from that load extending to the later access.
+ Address dependencies are quite common in RCU read-side critical
+ sections:
+
+ 1 rcu_read_lock();
+ 2 p = rcu_dereference(gp);
+ 3 do_something(p->a);
+ 4 rcu_read_unlock();
+
+ In this case, because the address of "p->a" on line 3 is computed
+ from the value returned by the rcu_dereference() on line 2, the
+ address dependency extends from that rcu_dereference() to that
+ "p->a". In rare cases, optimizing compilers can destroy address
+ dependencies. Please see Documentation/RCU/rcu_dereference.txt
+ for more information.
+
+ See also "Control Dependency".
+
+Acquire: With respect to a lock, acquiring that lock, for example,
+ using spin_lock(). With respect to a non-lock shared variable,
+ a special operation that includes a load and which orders that
+ load before later memory references running on that same CPU.
+ An example special acquire operation is smp_load_acquire(),
+ but atomic_read_acquire() and atomic_xchg_acquire() also include
+ acquire loads.
+
+ When an acquire load returns the value stored by a release store
+ to that same variable, then all operations preceding that store
+ happen before any operations following that load acquire.
+
+ See also "Relaxed" and "Release".
+
+Coherence (co): When one CPU's store to a given variable overwrites
+ either the value from another CPU's store or some later value,
+ there is said to be a coherence link from the second CPU to
+ the first.
+
+ It is also possible to have a coherence link within a CPU, which
+ is a "coherence internal" (coi) link. The term "coherence
+ external" (coe) link is used when it is necessary to exclude
+ the coi case.
+
+ See also "From-reads" and "Reads-from".
+
+Control Dependency: When a later store's execution depends on a test
+ of a value computed from a value returned by an earlier load,
+ a "control dependency" extends from that load to that store.
+ For example:
+
+ 1 if (READ_ONCE(x))
+ 2 WRITE_ONCE(y, 1);
+
+ Here, the control dependency extends from the READ_ONCE() on
+ line 1 to the WRITE_ONCE() on line 2. Control dependencies are
+ fragile, and can be easily destroyed by optimizing compilers.
+ Please see control-dependencies.txt for more information.
+
+ See also "Address Dependency".
+
+Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
+ name suggests. And in a great many cases, a pair of CPUs is all
+ that is required. In other cases, the notion of pairing must be
+ extended to additional CPUs, and the result is called a "cycle".
+ In a cycle, each CPU's ordering interacts with that of the next:
+
+ CPU 0 CPU 1 CPU 2
+ WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1);
+ smp_mb(); smp_mb(); smp_mb();
+ r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x);
+
+ CPU 0's smp_mb() interacts with that of CPU 1, which interacts
+ with that of CPU 2, which in turn interacts with that of CPU 0
+ to complete the cycle. Because of the smp_mb() calls between
+ each pair of memory accesses, the outcome where r0, r1, and r2
+ are all equal to zero is forbidden by LKMM.
+
+ See also "Pairing".
+
+From-Reads (fr): When one CPU's store to a given variable happened
+ too late to affect the value returned by another CPU's
+ load from that same variable, there is said to be a from-reads
+ link from the load to the store.
+
+ It is also possible to have a from-reads link within a CPU, which
+ is a "from-reads internal" (fri) link. The term "from-reads
+ external" (fre) link is used when it is necessary to exclude
+ the fri case.
+
+ See also "Coherence" and "Reads-from".
+
+Fully Ordered: An operation such as smp_mb() that orders all of
+ its CPU's prior accesses with all of that CPU's subsequent
+ accesses, or a marked access such as atomic_add_return()
+ that orders all of its CPU's prior accesses, itself, and
+ all of its CPU's subsequent accesses.
+
+Marked Access: An access to a variable that uses an special function or
+ macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
+
+ See also "Unmarked Access".
+
+Pairing: "Memory-barrier pairing" reflects the fact that synchronizing
+ data between two CPUs requires that both CPUs their accesses.
+ Memory barriers thus tend to come in pairs, one executed by
+ one of the CPUs and the other by the other CPU. Of course,
+ pairing also occurs with other types of operations, so that a
+ smp_store_release() pairs with an smp_load_acquire() that reads
+ the value stored.
+
+ See also "Cycle".
+
+Reads-From (rf): When one CPU's load returns the value stored by some other
+ CPU, there is said to be a reads-from link from the second
+ CPU's store to the first CPU's load. Reads-from links have the
+ nice property that time must advance from the store to the load,
+ which means that algorithms using reads-from links can use lighter
+ weight ordering and synchronization compared to algorithms using
+ coherence and from-reads links.
+
+ It is also possible to have a reads-from link within a CPU, which
+ is a "reads-from internal" (rfi) link. The term "reads-from
+ external" (rfe) link is used when it is necessary to exclude
+ the rfi case.
+
+ See also Coherence" and "From-reads".
+
+Relaxed: A marked access that does not imply ordering, for example, a
+ READ_ONCE(), WRITE_ONCE(), a non-value-returning read-modify-write
+ operation, or a value-returning read-modify-write operation whose
+ name ends in "_relaxed".
+
+ See also "Acquire" and "Release".
+
+Release: With respect to a lock, releasing that lock, for example,
+ using spin_unlock(). With respect to a non-lock shared variable,
+ a special operation that includes a store and which orders that
+ store after earlier memory references that ran on that same CPU.
+ An example special release store is smp_store_release(), but
+ atomic_set_release() and atomic_cmpxchg_release() also include
+ release stores.
+
+ See also "Acquire" and "Relaxed".
+
+Unmarked Access: An access to a variable that uses normal C-language
+ syntax, for example, "a = b[2]";
+
+ See also "Marked Access".
--
2.9.5
Hi Paul,
On 2020/11/06 7:00, [email protected] wrote:
> From: "Paul E. McKenney" <[email protected]>
>
> This commit adds type information for global variables in the litmus
> tests in order to allow easier use with klitmus7.
IIUC, klitmus7 is happy with existing litmus tests under tools/memory-model.
So I don't think this change is necessary.
As a matter of fact, I was preparing a patch set to empty most of the
initialization blocks in perfbook's CodeSamples/formal/ litmus tests.
Thanks, Akira
>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4 +++-
> tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4 +++-
> tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus | 4 +++-
> tools/memory-model/litmus-tests/CoWW+poonceonce.litmus | 4 +++-
> .../litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus | 5 ++++-
> tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5 ++++-
> .../litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
> tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6 +++++-
> .../ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 6 +++++-
> .../litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus | 5 ++++-
> .../litmus-tests/LB+poacquireonce+pooncerelease.litmus | 5 ++++-
> tools/memory-model/litmus-tests/LB+poonceonces.litmus | 5 ++++-
> .../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 5 ++++-
> tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 5 +++--
> .../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 2 ++
> .../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 2 ++
> tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++++-
> tools/memory-model/litmus-tests/MP+poonceonces.litmus | 5 ++++-
> .../litmus-tests/MP+pooncerelease+poacquireonce.litmus | 5 ++++-
> tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++++-
> tools/memory-model/litmus-tests/R+fencembonceonces.litmus | 5 ++++-
> tools/memory-model/litmus-tests/R+poonceonces.litmus | 5 ++++-
> .../litmus-tests/S+fencewmbonceonce+poacquireonce.litmus | 5 ++++-
> tools/memory-model/litmus-tests/S+poonceonces.litmus | 5 ++++-
> tools/memory-model/litmus-tests/SB+fencembonceonces.litmus | 5 ++++-
> tools/memory-model/litmus-tests/SB+poonceonces.litmus | 5 ++++-
> tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus | 5 ++++-
> tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5 ++++-
> .../litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus | 5 ++++-
> .../litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus | 7 ++++++-
> .../litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
> .../Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6 +++++-
> 32 files changed, 130 insertions(+), 31 deletions(-)
>
> diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> index 967f9f2..772544f 100644
> --- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> @@ -7,7 +7,9 @@ C CoRR+poonceonce+Once
> * reads from the same variable are ordered.
> *)
>
> -{}
> +{
> + int x;
> +}
>
> P0(int *x)
> {
> diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> index 4635739..5faae98 100644
> --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> index bb068c9..77c9cc9 100644
> --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> index 0d9f0a9..85ef746 100644
> --- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> @@ -7,7 +7,9 @@ C CoWW+poonceonce
> * writes to the same variable are ordered.
> *)
>
> -{}
> +{
> + int x;
> +}
>
> P0(int *x)
> {
> diff --git a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> index e729d27..87aa900 100644
> --- a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> +++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> @@ -10,7 +10,10 @@ C IRIW+fencembonceonces+OnceOnce
> * process? This litmus test exercises LKMM's "propagation" rule.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x)
> {
> diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> index 4b54dd6..f84022d 100644
> --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> @@ -10,7 +10,10 @@ C IRIW+poonceonces+OnceOnce
> * different process?
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x)
> {
> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> index 094d58d..398f624 100644
> --- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> index b321aa6..212a432 100644
> --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> index 025b046..7afd856 100644
> --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> index 4727f5a..c8a93c7 100644
> --- a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> index 07b9904..2fa0295 100644
> --- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> @@ -8,7 +8,10 @@ C LB+poacquireonce+pooncerelease
> * to the other?
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> index 74c49cb..2107306 100644
> --- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> @@ -7,7 +7,10 @@ C LB+poonceonces
> * be prevented even with no explicit ordering?
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> index a273da9..e04b71b 100644
> --- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> index 97731b4..18df682 100644
> --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> @@ -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)
> diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> index 50f4d62..b1b1266 100644
> --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> @@ -11,6 +11,8 @@ C MP+polockmbonce+poacquiresilsil
> *)
>
> {
> + spinlock_t lo;
> + int x;
> }
>
> P0(spinlock_t *lo, int *x)
> diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> index abf81e7..867c75d 100644
> --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> @@ -11,6 +11,8 @@ C MP+polockonce+poacquiresilsil
> *)
>
> {
> + spinlock_t lo;
> + int x;
> }
>
> P0(spinlock_t *lo, int *x)
> diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
> index 712a4fcd..63e0f67 100644
> --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> index 172f014..68180a4 100644
> --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> @@ -7,7 +7,10 @@ C MP+poonceonces
> * no ordering at all?
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> index d52c684..19f3e68 100644
> --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> @@ -8,7 +8,10 @@ C MP+pooncerelease+poacquireonce
> * pattern.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> index 72c9276..4ac189a 100644
> --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> index 222a0b8..af9463b 100644
> --- a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> @@ -9,7 +9,10 @@ C R+fencembonceonces
> * cause the resulting test to be allowed.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> index 5386f12..bcd5574e 100644
> --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> @@ -8,7 +8,10 @@ C R+poonceonces
> * store propagation delays.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> index 1847982..c36341d 100644
> --- a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> +++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> @@ -7,7 +7,10 @@ C S+fencewmbonceonce+poacquireonce
> * store against a subsequent store?
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> index 8c9c2f8..7775c23 100644
> --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> @@ -9,7 +9,10 @@ C S+poonceonces
> * READ_ONCE(), is ordering preserved?
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> index ed5fff1..833cdfe 100644
> --- a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> @@ -9,7 +9,10 @@ C SB+fencembonceonces
> * suffice, but not much else.)
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> index 10d5507..c92211e 100644
> --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> @@ -8,7 +8,10 @@ C SB+poonceonces
> * variable that the preceding process reads.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x, int *y)
> {
> diff --git a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> index 04a1660..84344b4 100644
> --- a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> +++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> index 6a2bc12..4314947 100644
> --- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> @@ -8,7 +8,10 @@ C WRC+poonceonces+Once
> * test has no ordering at all.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x)
> {
> diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> index e994725..554999c 100644
> --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> @@ -10,7 +10,10 @@ C WRC+pooncerelease+fencermbonceonce+Once
> * is A-cumulative in LKMM.
> *)
>
> -{}
> +{
> + int x;
> + int y;
> +}
>
> P0(int *x)
> {
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> index 415248f..265a95f 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> index 10a2aa0..0c9aea8 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> @@ -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)
> {
> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> index 88e70b8..661f9aa 100644
> --- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> @@ -14,7 +14,11 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
> * involving locking.)
> *)
>
> -{}
> +{
> + int x;
> + int y;
> + int z;
> +}
>
> P0(int *x, int *y)
> {
>
On Fri, Nov 06, 2020 at 07:41:48AM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> On 2020/11/06 7:00, [email protected] wrote:
> > From: "Paul E. McKenney" <[email protected]>
> >
> > This commit adds type information for global variables in the litmus
> > tests in order to allow easier use with klitmus7.
>
> IIUC, klitmus7 is happy with existing litmus tests under tools/memory-model.
> So I don't think this change is necessary.
>
> As a matter of fact, I was preparing a patch set to empty most of the
> initialization blocks in perfbook's CodeSamples/formal/ litmus tests.
Heh! Someone asked for this change several months back, and I failed
to record who it was. If they don't object, I will remove this patch.
Thanx, Paul
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4 +++-
> > tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4 +++-
> > tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus | 4 +++-
> > tools/memory-model/litmus-tests/CoWW+poonceonce.litmus | 4 +++-
> > .../litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5 ++++-
> > .../litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
> > tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6 +++++-
> > .../ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 6 +++++-
> > .../litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus | 5 ++++-
> > .../litmus-tests/LB+poacquireonce+pooncerelease.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/LB+poonceonces.litmus | 5 ++++-
> > .../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 5 +++--
> > .../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 2 ++
> > .../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 2 ++
> > tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++++-
> > tools/memory-model/litmus-tests/MP+poonceonces.litmus | 5 ++++-
> > .../litmus-tests/MP+pooncerelease+poacquireonce.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++++-
> > tools/memory-model/litmus-tests/R+fencembonceonces.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/R+poonceonces.litmus | 5 ++++-
> > .../litmus-tests/S+fencewmbonceonce+poacquireonce.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/S+poonceonces.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/SB+fencembonceonces.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/SB+poonceonces.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus | 5 ++++-
> > tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5 ++++-
> > .../litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus | 5 ++++-
> > .../litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus | 7 ++++++-
> > .../litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
> > .../Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6 +++++-
> > 32 files changed, 130 insertions(+), 31 deletions(-)
> >
> > diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > index 967f9f2..772544f 100644
> > --- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> > @@ -7,7 +7,9 @@ C CoRR+poonceonce+Once
> > * reads from the same variable are ordered.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > +}
> >
> > P0(int *x)
> > {
> > diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > index 4635739..5faae98 100644
> > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > index bb068c9..77c9cc9 100644
> > --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > index 0d9f0a9..85ef746 100644
> > --- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> > @@ -7,7 +7,9 @@ C CoWW+poonceonce
> > * writes to the same variable are ordered.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > +}
> >
> > P0(int *x)
> > {
> > diff --git a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> > index e729d27..87aa900 100644
> > --- a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> > +++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> > @@ -10,7 +10,10 @@ C IRIW+fencembonceonces+OnceOnce
> > * process? This litmus test exercises LKMM's "propagation" rule.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x)
> > {
> > diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > index 4b54dd6..f84022d 100644
> > --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> > @@ -10,7 +10,10 @@ C IRIW+poonceonces+OnceOnce
> > * different process?
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x)
> > {
> > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > index 094d58d..398f624 100644
> > --- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > index b321aa6..212a432 100644
> > --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > index 025b046..7afd856 100644
> > --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> > index 4727f5a..c8a93c7 100644
> > --- a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > index 07b9904..2fa0295 100644
> > --- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> > @@ -8,7 +8,10 @@ C LB+poacquireonce+pooncerelease
> > * to the other?
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > index 74c49cb..2107306 100644
> > --- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> > @@ -7,7 +7,10 @@ C LB+poonceonces
> > * be prevented even with no explicit ordering?
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> > index a273da9..e04b71b 100644
> > --- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > index 97731b4..18df682 100644
> > --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> > @@ -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)
> > diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> > index 50f4d62..b1b1266 100644
> > --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> > @@ -11,6 +11,8 @@ C MP+polockmbonce+poacquiresilsil
> > *)
> >
> > {
> > + spinlock_t lo;
> > + int x;
> > }
> >
> > P0(spinlock_t *lo, int *x)
> > diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> > index abf81e7..867c75d 100644
> > --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> > @@ -11,6 +11,8 @@ C MP+polockonce+poacquiresilsil
> > *)
> >
> > {
> > + spinlock_t lo;
> > + int x;
> > }
> >
> > P0(spinlock_t *lo, int *x)
> > diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
> > index 712a4fcd..63e0f67 100644
> > --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > index 172f014..68180a4 100644
> > --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> > @@ -7,7 +7,10 @@ C MP+poonceonces
> > * no ordering at all?
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > index d52c684..19f3e68 100644
> > --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> > @@ -8,7 +8,10 @@ C MP+pooncerelease+poacquireonce
> > * pattern.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > index 72c9276..4ac189a 100644
> > --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> > index 222a0b8..af9463b 100644
> > --- a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> > @@ -9,7 +9,10 @@ C R+fencembonceonces
> > * cause the resulting test to be allowed.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > index 5386f12..bcd5574e 100644
> > --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> > @@ -8,7 +8,10 @@ C R+poonceonces
> > * store propagation delays.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> > index 1847982..c36341d 100644
> > --- a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> > +++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> > @@ -7,7 +7,10 @@ C S+fencewmbonceonce+poacquireonce
> > * store against a subsequent store?
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > index 8c9c2f8..7775c23 100644
> > --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> > @@ -9,7 +9,10 @@ C S+poonceonces
> > * READ_ONCE(), is ordering preserved?
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> > index ed5fff1..833cdfe 100644
> > --- a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> > @@ -9,7 +9,10 @@ C SB+fencembonceonces
> > * suffice, but not much else.)
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > index 10d5507..c92211e 100644
> > --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> > @@ -8,7 +8,10 @@ C SB+poonceonces
> > * variable that the preceding process reads.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x, int *y)
> > {
> > diff --git a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> > index 04a1660..84344b4 100644
> > --- a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> > +++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > index 6a2bc12..4314947 100644
> > --- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> > @@ -8,7 +8,10 @@ C WRC+poonceonces+Once
> > * test has no ordering at all.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x)
> > {
> > diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> > index e994725..554999c 100644
> > --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> > +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> > @@ -10,7 +10,10 @@ C WRC+pooncerelease+fencermbonceonce+Once
> > * is A-cumulative in LKMM.
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > +}
> >
> > P0(int *x)
> > {
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > index 415248f..265a95f 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > index 10a2aa0..0c9aea8 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> > @@ -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)
> > {
> > diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> > index 88e70b8..661f9aa 100644
> > --- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> > +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> > @@ -14,7 +14,11 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
> > * involving locking.)
> > *)
> >
> > -{}
> > +{
> > + int x;
> > + int y;
> > + int z;
> > +}
> >
> > P0(int *x, int *y)
> > {
> >
On Thu, Nov 05, 2020 at 02:00:14PM -0800, [email protected] wrote:
> From: "Paul E. McKenney" <[email protected]>
>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> tools/memory-model/Documentation/glossary.txt | 155 ++++++++++++++++++++++++++
> 1 file changed, 155 insertions(+)
> create mode 100644 tools/memory-model/Documentation/glossary.txt
>
> diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> new file mode 100644
> index 0000000..036fa28
> --- /dev/null
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -0,0 +1,155 @@
> +This document contains brief definitions of LKMM-related terms. Like most
> +glossaries, it is not intended to be read front to back (except perhaps
> +as a way of confirming a diagnosis of OCD), but rather to be searched
> +for specific terms.
> +
> +
> +Address Dependency: When the address of a later memory access is computed
> + based on the value returned by an earlier load, an "address
> + dependency" extends from that load extending to the later access.
> + Address dependencies are quite common in RCU read-side critical
> + sections:
> +
> + 1 rcu_read_lock();
> + 2 p = rcu_dereference(gp);
> + 3 do_something(p->a);
> + 4 rcu_read_unlock();
> +
> + In this case, because the address of "p->a" on line 3 is computed
> + from the value returned by the rcu_dereference() on line 2, the
> + address dependency extends from that rcu_dereference() to that
> + "p->a". In rare cases, optimizing compilers can destroy address
> + dependencies. Please see Documentation/RCU/rcu_dereference.txt
> + for more information.
> +
> + See also "Control Dependency".
> +
> +Acquire: With respect to a lock, acquiring that lock, for example,
> + using spin_lock(). With respect to a non-lock shared variable,
> + a special operation that includes a load and which orders that
> + load before later memory references running on that same CPU.
> + An example special acquire operation is smp_load_acquire(),
> + but atomic_read_acquire() and atomic_xchg_acquire() also include
> + acquire loads.
> +
> + When an acquire load returns the value stored by a release store
> + to that same variable, then all operations preceding that store
Change this to:
When an acquire load reads-from a release store
, and put a reference to "Reads-from"? I think this makes the document
more consistent in that it makes clear "an acquire load returns the
value stored by a release store to the same variable" is not a special
case, it's simple a "Reads-from".
> + happen before any operations following that load acquire.
Add a reference to the definition of "happen before" in explanation.txt?
Regards,
Boqun
> +
> + See also "Relaxed" and "Release".
> +
[...]
On Thu, Nov 05, 2020 at 02:00:14PM -0800, [email protected] wrote:
> From: "Paul E. McKenney" <[email protected]>
>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> tools/memory-model/Documentation/glossary.txt | 155 ++++++++++++++++++++++++++
> 1 file changed, 155 insertions(+)
> create mode 100644 tools/memory-model/Documentation/glossary.txt
>
> diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> new file mode 100644
> index 0000000..036fa28
> --- /dev/null
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -0,0 +1,155 @@
> +This document contains brief definitions of LKMM-related terms. Like most
> +glossaries, it is not intended to be read front to back (except perhaps
> +as a way of confirming a diagnosis of OCD), but rather to be searched
> +for specific terms.
> +
> +
> +Address Dependency: When the address of a later memory access is computed
> + based on the value returned by an earlier load, an "address
> + dependency" extends from that load extending to the later access.
> + Address dependencies are quite common in RCU read-side critical
> + sections:
> +
> + 1 rcu_read_lock();
> + 2 p = rcu_dereference(gp);
> + 3 do_something(p->a);
> + 4 rcu_read_unlock();
> +
> + In this case, because the address of "p->a" on line 3 is computed
> + from the value returned by the rcu_dereference() on line 2, the
> + address dependency extends from that rcu_dereference() to that
> + "p->a". In rare cases, optimizing compilers can destroy address
> + dependencies. Please see Documentation/RCU/rcu_dereference.txt
> + for more information.
> +
> + See also "Control Dependency".
There should also be an entry for "Data Dependency", linked from here
and from Control Dependency.
> +Marked Access: An access to a variable that uses an special function or
> + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
How about "r1 = READ_ONCE(x)"?
Alan
On Fri, Nov 06, 2020 at 09:47:22AM +0800, Boqun Feng wrote:
> On Thu, Nov 05, 2020 at 02:00:14PM -0800, [email protected] wrote:
> > From: "Paul E. McKenney" <[email protected]>
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > tools/memory-model/Documentation/glossary.txt | 155 ++++++++++++++++++++++++++
> > 1 file changed, 155 insertions(+)
> > create mode 100644 tools/memory-model/Documentation/glossary.txt
> >
> > diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> > new file mode 100644
> > index 0000000..036fa28
> > --- /dev/null
> > +++ b/tools/memory-model/Documentation/glossary.txt
> > @@ -0,0 +1,155 @@
> > +This document contains brief definitions of LKMM-related terms. Like most
> > +glossaries, it is not intended to be read front to back (except perhaps
> > +as a way of confirming a diagnosis of OCD), but rather to be searched
> > +for specific terms.
> > +
> > +
> > +Address Dependency: When the address of a later memory access is computed
> > + based on the value returned by an earlier load, an "address
> > + dependency" extends from that load extending to the later access.
> > + Address dependencies are quite common in RCU read-side critical
> > + sections:
> > +
> > + 1 rcu_read_lock();
> > + 2 p = rcu_dereference(gp);
> > + 3 do_something(p->a);
> > + 4 rcu_read_unlock();
> > +
> > + In this case, because the address of "p->a" on line 3 is computed
> > + from the value returned by the rcu_dereference() on line 2, the
> > + address dependency extends from that rcu_dereference() to that
> > + "p->a". In rare cases, optimizing compilers can destroy address
> > + dependencies. Please see Documentation/RCU/rcu_dereference.txt
> > + for more information.
> > +
> > + See also "Control Dependency".
> > +
> > +Acquire: With respect to a lock, acquiring that lock, for example,
> > + using spin_lock(). With respect to a non-lock shared variable,
> > + a special operation that includes a load and which orders that
> > + load before later memory references running on that same CPU.
> > + An example special acquire operation is smp_load_acquire(),
> > + but atomic_read_acquire() and atomic_xchg_acquire() also include
> > + acquire loads.
> > +
> > + When an acquire load returns the value stored by a release store
> > + to that same variable, then all operations preceding that store
>
> Change this to:
>
> When an acquire load reads-from a release store
>
> , and put a reference to "Reads-from"? I think this makes the document
> more consistent in that it makes clear "an acquire load returns the
> value stored by a release store to the same variable" is not a special
> case, it's simple a "Reads-from".
>
> > + happen before any operations following that load acquire.
>
> Add a reference to the definition of "happen before" in explanation.txt?
How about as shown below? I currently am carrying this as a separate
commit, but I might merge it into this one later on.
Thanx, Paul
------------------------------------------------------------------------
commit 774a52cd3d80d6b657ae6c14c10bd9fc437068f3
Author: Paul E. McKenney <[email protected]>
Date: Fri Nov 6 09:58:01 2020 -0800
tools/memory-model: Tie acquire loads to reads-from
This commit explicitly makes the connection between acquire loads and
the reads-from relation. It also adds an entry for happens-before,
and refers to the corresponding section of explanation.txt.
Reported-by: Boqun Feng <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
index 3924aca..383151b 100644
--- a/tools/memory-model/Documentation/glossary.txt
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -33,10 +33,11 @@ Acquire: With respect to a lock, acquiring that lock, for example,
acquire loads.
When an acquire load returns the value stored by a release store
- to that same variable, then all operations preceding that store
- happen before any operations following that load acquire.
+ to that same variable, (in other words, the acquire load "reads
+ from" the release store), then all operations preceding that
+ store "happen before" any operations following that load acquire.
- See also "Relaxed" and "Release".
+ See also "Happens-Before", "Reads-From", "Relaxed", and "Release".
Coherence (co): When one CPU's store to a given variable overwrites
either the value from another CPU's store or some later value,
@@ -102,6 +103,11 @@ Fully Ordered: An operation such as smp_mb() that orders all of
that orders all of its CPU's prior accesses, itself, and
all of its CPU's subsequent accesses.
+Happens-Before (hb): A relation between two accesses in which LKMM
+ guarantees the first access precedes the second. For more
+ detail, please see the "THE HAPPENS-BEFORE RELATION: hb"
+ section of explanation.txt.
+
Marked Access: An access to a variable that uses an special function or
macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> On Thu, Nov 05, 2020 at 02:00:14PM -0800, [email protected] wrote:
> > From: "Paul E. McKenney" <[email protected]>
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > tools/memory-model/Documentation/glossary.txt | 155 ++++++++++++++++++++++++++
> > 1 file changed, 155 insertions(+)
> > create mode 100644 tools/memory-model/Documentation/glossary.txt
> >
> > diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> > new file mode 100644
> > index 0000000..036fa28
> > --- /dev/null
> > +++ b/tools/memory-model/Documentation/glossary.txt
> > @@ -0,0 +1,155 @@
> > +This document contains brief definitions of LKMM-related terms. Like most
> > +glossaries, it is not intended to be read front to back (except perhaps
> > +as a way of confirming a diagnosis of OCD), but rather to be searched
> > +for specific terms.
> > +
> > +
> > +Address Dependency: When the address of a later memory access is computed
> > + based on the value returned by an earlier load, an "address
> > + dependency" extends from that load extending to the later access.
> > + Address dependencies are quite common in RCU read-side critical
> > + sections:
> > +
> > + 1 rcu_read_lock();
> > + 2 p = rcu_dereference(gp);
> > + 3 do_something(p->a);
> > + 4 rcu_read_unlock();
> > +
> > + In this case, because the address of "p->a" on line 3 is computed
> > + from the value returned by the rcu_dereference() on line 2, the
> > + address dependency extends from that rcu_dereference() to that
> > + "p->a". In rare cases, optimizing compilers can destroy address
> > + dependencies. Please see Documentation/RCU/rcu_dereference.txt
> > + for more information.
> > +
> > + See also "Control Dependency".
>
> There should also be an entry for "Data Dependency", linked from here
> and from Control Dependency.
>
> > +Marked Access: An access to a variable that uses an special function or
> > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
>
> How about "r1 = READ_ONCE(x)"?
Good catches! I am planning to squash the commit below into the
original. Does that cover it?
Thanx, Paul
------------------------------------------------------------------------
commit 27c694f5a049d3edac1f258b888d02650cec936a
Author: Paul E. McKenney <[email protected]>
Date: Fri Nov 6 10:02:41 2020 -0800
squash! tools/memory-model: Add a glossary of LKMM terms
[ paulmck: Apply Alan Stern feedback. ]
Signed-off-by: Paul E. McKenney <[email protected]>
diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
index 383151b..471bf13 100644
--- a/tools/memory-model/Documentation/glossary.txt
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -22,7 +22,7 @@ Address Dependency: When the address of a later memory access is computed
dependencies. Please see Documentation/RCU/rcu_dereference.txt
for more information.
- See also "Control Dependency".
+ See also "Control Dependency" and "Data Dependency".
Acquire: With respect to a lock, acquiring that lock, for example,
using spin_lock(). With respect to a non-lock shared variable,
@@ -109,7 +109,7 @@ Happens-Before (hb): A relation between two accesses in which LKMM
section of explanation.txt.
Marked Access: An access to a variable that uses an special function or
- macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
+ macro such as "r1 = READ_ONCE(x)" or "smp_store_release(&a, 1)".
See also "Unmarked Access".
On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > + See also "Control Dependency".
> >
> > There should also be an entry for "Data Dependency", linked from here
> > and from Control Dependency.
> >
> > > +Marked Access: An access to a variable that uses an special function or
> > > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> >
> > How about "r1 = READ_ONCE(x)"?
>
> Good catches! I am planning to squash the commit below into the
> original. Does that cover it?
No, because you didn't add a glossary entry for "Data Dependency" and
there's no link from "Control Dependency" to "Data Dependency".
Alan
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit 27c694f5a049d3edac1f258b888d02650cec936a
> Author: Paul E. McKenney <[email protected]>
> Date: Fri Nov 6 10:02:41 2020 -0800
>
> squash! tools/memory-model: Add a glossary of LKMM terms
>
> [ paulmck: Apply Alan Stern feedback. ]
> Signed-off-by: Paul E. McKenney <[email protected]>
>
> diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> index 383151b..471bf13 100644
> --- a/tools/memory-model/Documentation/glossary.txt
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -22,7 +22,7 @@ Address Dependency: When the address of a later memory access is computed
> dependencies. Please see Documentation/RCU/rcu_dereference.txt
> for more information.
>
> - See also "Control Dependency".
> + See also "Control Dependency" and "Data Dependency".
>
> Acquire: With respect to a lock, acquiring that lock, for example,
> using spin_lock(). With respect to a non-lock shared variable,
> @@ -109,7 +109,7 @@ Happens-Before (hb): A relation between two accesses in which LKMM
> section of explanation.txt.
>
> Marked Access: An access to a variable that uses an special function or
> - macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> + macro such as "r1 = READ_ONCE(x)" or "smp_store_release(&a, 1)".
>
> See also "Unmarked Access".
>
On Fri, Nov 06, 2020 at 02:23:51PM -0500, Alan Stern wrote:
> On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> > On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > > + See also "Control Dependency".
> > >
> > > There should also be an entry for "Data Dependency", linked from here
> > > and from Control Dependency.
> > >
> > > > +Marked Access: An access to a variable that uses an special function or
> > > > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > >
> > > How about "r1 = READ_ONCE(x)"?
> >
> > Good catches! I am planning to squash the commit below into the
> > original. Does that cover it?
>
> No, because you didn't add a glossary entry for "Data Dependency" and
> there's no link from "Control Dependency" to "Data Dependency".
Sigh. I was thinking "entry in the list", and didn't even thing to
check for an entry in the glossary as a whole. With the patch below
(on top of the one sent earlier), are we good?
Thanx, Paul
------------------------------------------------------------------------
commit 5a49c32551e83d30e304d6c3fbb660737ba2654e
Author: Paul E. McKenney <[email protected]>
Date: Fri Nov 6 11:57:25 2020 -0800
fixup! tools/memory-model: Add a glossary of LKMM terms
Signed-off-by: Paul E. McKenney <[email protected]>
diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
index 471bf13..b2da636 100644
--- a/tools/memory-model/Documentation/glossary.txt
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -64,7 +64,7 @@ Control Dependency: When a later store's execution depends on a test
fragile, and can be easily destroyed by optimizing compilers.
Please see control-dependencies.txt for more information.
- See also "Address Dependency".
+ See also "Address Dependency" and "Data Dependency".
Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
name suggests. And in a great many cases, a pair of CPUs is all
@@ -85,6 +85,23 @@ Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
See also "Pairing".
+Data Dependency: When the data written by a later store is computed based
+ on the value returned by an earlier load, a "data dependency"
+ extends from that load to that later store. For example:
+
+ 1 r1 = READ_ONCE(x);
+ 2 WRITE_ONCE(y, r1 + 1);
+
+ In this case, the data dependency extends from the READ_ONCE()
+ on line 1 to the WRITE_ONCE() on line 2. Data dependencies are
+ fragile and can be easily destroyed by optimizing compilers.
+ Because optimizing compilers put a great deal of effort into
+ working out what values integer variables might have, this is
+ especially true in cases where the dependency is carried through
+ an integer.
+
+ See also "Address Dependency" and "Control Dependency".
+
From-Reads (fr): When one CPU's store to a given variable happened
too late to affect the value returned by another CPU's
load from that same variable, there is said to be a from-reads
On Fri, Nov 06, 2020 at 11:59:12AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 02:23:51PM -0500, Alan Stern wrote:
> > On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> > > On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > > > + See also "Control Dependency".
> > > >
> > > > There should also be an entry for "Data Dependency", linked from here
> > > > and from Control Dependency.
> > > >
> > > > > +Marked Access: An access to a variable that uses an special function or
> > > > > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > > >
> > > > How about "r1 = READ_ONCE(x)"?
> > >
> > > Good catches! I am planning to squash the commit below into the
> > > original. Does that cover it?
> >
> > No, because you didn't add a glossary entry for "Data Dependency" and
> > there's no link from "Control Dependency" to "Data Dependency".
>
> Sigh. I was thinking "entry in the list", and didn't even thing to
> check for an entry in the glossary as a whole. With the patch below
> (on top of the one sent earlier), are we good?
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit 5a49c32551e83d30e304d6c3fbb660737ba2654e
> Author: Paul E. McKenney <[email protected]>
> Date: Fri Nov 6 11:57:25 2020 -0800
>
> fixup! tools/memory-model: Add a glossary of LKMM terms
>
> Signed-off-by: Paul E. McKenney <[email protected]>
>
> diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> index 471bf13..b2da636 100644
> --- a/tools/memory-model/Documentation/glossary.txt
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -64,7 +64,7 @@ Control Dependency: When a later store's execution depends on a test
> fragile, and can be easily destroyed by optimizing compilers.
> Please see control-dependencies.txt for more information.
>
> - See also "Address Dependency".
> + See also "Address Dependency" and "Data Dependency".
>
> Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
> name suggests. And in a great many cases, a pair of CPUs is all
> @@ -85,6 +85,23 @@ Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
>
> See also "Pairing".
>
> +Data Dependency: When the data written by a later store is computed based
> + on the value returned by an earlier load, a "data dependency"
> + extends from that load to that later store. For example:
> +
> + 1 r1 = READ_ONCE(x);
> + 2 WRITE_ONCE(y, r1 + 1);
> +
> + In this case, the data dependency extends from the READ_ONCE()
> + on line 1 to the WRITE_ONCE() on line 2. Data dependencies are
> + fragile and can be easily destroyed by optimizing compilers.
> + Because optimizing compilers put a great deal of effort into
> + working out what values integer variables might have, this is
> + especially true in cases where the dependency is carried through
> + an integer.
> +
> + See also "Address Dependency" and "Control Dependency".
> +
> From-Reads (fr): When one CPU's store to a given variable happened
> too late to affect the value returned by another CPU's
> load from that same variable, there is said to be a from-reads
Yes, this is better.
Is it really true that data dependencies are so easily destroyed? I
would expect that a true "semantic" dependency (i.e., one where the
value written really does vary according to the value read) would be
rather hard to second guess.
Alan
On Fri, Nov 06, 2020 at 03:40:08PM -0500, Alan Stern wrote:
> On Fri, Nov 06, 2020 at 11:59:12AM -0800, Paul E. McKenney wrote:
> > On Fri, Nov 06, 2020 at 02:23:51PM -0500, Alan Stern wrote:
> > > On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> > > > On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > > > > + See also "Control Dependency".
> > > > >
> > > > > There should also be an entry for "Data Dependency", linked from here
> > > > > and from Control Dependency.
> > > > >
> > > > > > +Marked Access: An access to a variable that uses an special function or
> > > > > > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > > > >
> > > > > How about "r1 = READ_ONCE(x)"?
> > > >
> > > > Good catches! I am planning to squash the commit below into the
> > > > original. Does that cover it?
> > >
> > > No, because you didn't add a glossary entry for "Data Dependency" and
> > > there's no link from "Control Dependency" to "Data Dependency".
> >
> > Sigh. I was thinking "entry in the list", and didn't even thing to
> > check for an entry in the glossary as a whole. With the patch below
> > (on top of the one sent earlier), are we good?
> >
> > Thanx, Paul
> >
> > ------------------------------------------------------------------------
> >
> > commit 5a49c32551e83d30e304d6c3fbb660737ba2654e
> > Author: Paul E. McKenney <[email protected]>
> > Date: Fri Nov 6 11:57:25 2020 -0800
> >
> > fixup! tools/memory-model: Add a glossary of LKMM terms
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> >
> > diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> > index 471bf13..b2da636 100644
> > --- a/tools/memory-model/Documentation/glossary.txt
> > +++ b/tools/memory-model/Documentation/glossary.txt
> > @@ -64,7 +64,7 @@ Control Dependency: When a later store's execution depends on a test
> > fragile, and can be easily destroyed by optimizing compilers.
> > Please see control-dependencies.txt for more information.
> >
> > - See also "Address Dependency".
> > + See also "Address Dependency" and "Data Dependency".
> >
> > Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
> > name suggests. And in a great many cases, a pair of CPUs is all
> > @@ -85,6 +85,23 @@ Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
> >
> > See also "Pairing".
> >
> > +Data Dependency: When the data written by a later store is computed based
> > + on the value returned by an earlier load, a "data dependency"
> > + extends from that load to that later store. For example:
> > +
> > + 1 r1 = READ_ONCE(x);
> > + 2 WRITE_ONCE(y, r1 + 1);
> > +
> > + In this case, the data dependency extends from the READ_ONCE()
> > + on line 1 to the WRITE_ONCE() on line 2. Data dependencies are
> > + fragile and can be easily destroyed by optimizing compilers.
> > + Because optimizing compilers put a great deal of effort into
> > + working out what values integer variables might have, this is
> > + especially true in cases where the dependency is carried through
> > + an integer.
> > +
> > + See also "Address Dependency" and "Control Dependency".
> > +
> > From-Reads (fr): When one CPU's store to a given variable happened
> > too late to affect the value returned by another CPU's
> > load from that same variable, there is said to be a from-reads
>
> Yes, this is better.
Thank you for bearing with me on this!
> Is it really true that data dependencies are so easily destroyed? I
> would expect that a true "semantic" dependency (i.e., one where the
> value written really does vary according to the value read) would be
> rather hard to second guess.
The usual optimizations apply, for but one example:
r1 = READ_ONCE(x);
WRITE_ONCE(y, (r1 + 1) % MAX_ELEMENTS);
If MAX_ELEMENTS is 1, so long, data dependency!
With pointers, the compiler has fewer optimization opportunities,
but there are still cases where it can break the dependency.
Or transform it to a control dependency.
Thanx, Paul
On Fri, Nov 06, 2020 at 01:04:13PM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 03:40:08PM -0500, Alan Stern wrote:
> > Is it really true that data dependencies are so easily destroyed? I
> > would expect that a true "semantic" dependency (i.e., one where the
> > value written really does vary according to the value read) would be
> > rather hard to second guess.
>
> The usual optimizations apply, for but one example:
>
> r1 = READ_ONCE(x);
> WRITE_ONCE(y, (r1 + 1) % MAX_ELEMENTS);
>
> If MAX_ELEMENTS is 1, so long, data dependency!
Sure, but if MAX_ELEMENTS is 1 then the value written will always be 0
no matter what value r1 has, so it isn't a semantic dependency.
Presumably a semantic data dependency would be much more robust.
I wonder if it's worth pointing out this distinction to the reader.
> With pointers, the compiler has fewer optimization opportunities,
> but there are still cases where it can break the dependency.
> Or transform it to a control dependency.
Transforming a data dependency into a control dependency wouldn't make
any important difference; the hardware would still provide the desired
ordering.
Alan
On Fri, Nov 06, 2020 at 10:01:02AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 09:47:22AM +0800, Boqun Feng wrote:
> > On Thu, Nov 05, 2020 at 02:00:14PM -0800, [email protected] wrote:
> > > From: "Paul E. McKenney" <[email protected]>
> > >
> > > Signed-off-by: Paul E. McKenney <[email protected]>
> > > ---
> > > tools/memory-model/Documentation/glossary.txt | 155 ++++++++++++++++++++++++++
> > > 1 file changed, 155 insertions(+)
> > > create mode 100644 tools/memory-model/Documentation/glossary.txt
> > >
> > > diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> > > new file mode 100644
> > > index 0000000..036fa28
> > > --- /dev/null
> > > +++ b/tools/memory-model/Documentation/glossary.txt
> > > @@ -0,0 +1,155 @@
> > > +This document contains brief definitions of LKMM-related terms. Like most
> > > +glossaries, it is not intended to be read front to back (except perhaps
> > > +as a way of confirming a diagnosis of OCD), but rather to be searched
> > > +for specific terms.
> > > +
> > > +
> > > +Address Dependency: When the address of a later memory access is computed
> > > + based on the value returned by an earlier load, an "address
> > > + dependency" extends from that load extending to the later access.
> > > + Address dependencies are quite common in RCU read-side critical
> > > + sections:
> > > +
> > > + 1 rcu_read_lock();
> > > + 2 p = rcu_dereference(gp);
> > > + 3 do_something(p->a);
> > > + 4 rcu_read_unlock();
> > > +
> > > + In this case, because the address of "p->a" on line 3 is computed
> > > + from the value returned by the rcu_dereference() on line 2, the
> > > + address dependency extends from that rcu_dereference() to that
> > > + "p->a". In rare cases, optimizing compilers can destroy address
> > > + dependencies. Please see Documentation/RCU/rcu_dereference.txt
> > > + for more information.
> > > +
> > > + See also "Control Dependency".
> > > +
> > > +Acquire: With respect to a lock, acquiring that lock, for example,
> > > + using spin_lock(). With respect to a non-lock shared variable,
> > > + a special operation that includes a load and which orders that
> > > + load before later memory references running on that same CPU.
> > > + An example special acquire operation is smp_load_acquire(),
> > > + but atomic_read_acquire() and atomic_xchg_acquire() also include
> > > + acquire loads.
> > > +
> > > + When an acquire load returns the value stored by a release store
> > > + to that same variable, then all operations preceding that store
> >
> > Change this to:
> >
> > When an acquire load reads-from a release store
> >
> > , and put a reference to "Reads-from"? I think this makes the document
> > more consistent in that it makes clear "an acquire load returns the
> > value stored by a release store to the same variable" is not a special
> > case, it's simple a "Reads-from".
> >
> > > + happen before any operations following that load acquire.
> >
> > Add a reference to the definition of "happen before" in explanation.txt?
>
> How about as shown below? I currently am carrying this as a separate
> commit, but I might merge it into this one later on.
>
Looks good to me, thanks!
Regards,
Boqun
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit 774a52cd3d80d6b657ae6c14c10bd9fc437068f3
> Author: Paul E. McKenney <[email protected]>
> Date: Fri Nov 6 09:58:01 2020 -0800
>
> tools/memory-model: Tie acquire loads to reads-from
>
> This commit explicitly makes the connection between acquire loads and
> the reads-from relation. It also adds an entry for happens-before,
> and refers to the corresponding section of explanation.txt.
>
> Reported-by: Boqun Feng <[email protected]>
> Signed-off-by: Paul E. McKenney <[email protected]>
>
> diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt
> index 3924aca..383151b 100644
> --- a/tools/memory-model/Documentation/glossary.txt
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -33,10 +33,11 @@ Acquire: With respect to a lock, acquiring that lock, for example,
> acquire loads.
>
> When an acquire load returns the value stored by a release store
> - to that same variable, then all operations preceding that store
> - happen before any operations following that load acquire.
> + to that same variable, (in other words, the acquire load "reads
> + from" the release store), then all operations preceding that
> + store "happen before" any operations following that load acquire.
>
> - See also "Relaxed" and "Release".
> + See also "Happens-Before", "Reads-From", "Relaxed", and "Release".
>
> Coherence (co): When one CPU's store to a given variable overwrites
> either the value from another CPU's store or some later value,
> @@ -102,6 +103,11 @@ Fully Ordered: An operation such as smp_mb() that orders all of
> that orders all of its CPU's prior accesses, itself, and
> all of its CPU's subsequent accesses.
>
> +Happens-Before (hb): A relation between two accesses in which LKMM
> + guarantees the first access precedes the second. For more
> + detail, please see the "THE HAPPENS-BEFORE RELATION: hb"
> + section of explanation.txt.
> +
> Marked Access: An access to a variable that uses an special function or
> macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
>
On Thu, 5 Nov 2020 14:56:05 -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 07:41:48AM +0900, Akira Yokosawa wrote:
>> Hi Paul,
>>
>> On 2020/11/06 7:00, [email protected] wrote:
>>> From: "Paul E. McKenney" <[email protected]>
>>>
>>> This commit adds type information for global variables in the litmus
>>> tests in order to allow easier use with klitmus7.
>>
>> IIUC, klitmus7 is happy with existing litmus tests under tools/memory-model.
>> So I don't think this change is necessary.
>>
>> As a matter of fact, I was preparing a patch set to empty most of the
>> initialization blocks in perfbook's CodeSamples/formal/ litmus tests.
>
> Heh! Someone asked for this change several months back, and I failed
> to record who it was. If they don't object, I will remove this patch.
Hi Paul,
I'm seeing this patch still alive in the updated for-mingo-lkmm branch.
Have you got some objection?
Thanks, Akira
>
> Thanx, Paul
>
>>>
>>> Signed-off-by: Paul E. McKenney <[email protected]>
>>> ---
>>> tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4 +++-
>>> tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4 +++-
>>> tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus | 4 +++-
>>> tools/memory-model/litmus-tests/CoWW+poonceonce.litmus | 4 +++-
>>> .../litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5 ++++-
>>> .../litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
>>> tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6 +++++-
>>> .../ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 6 +++++-
>>> .../litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus | 5 ++++-
>>> .../litmus-tests/LB+poacquireonce+pooncerelease.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/LB+poonceonces.litmus | 5 ++++-
>>> .../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 5 +++--
>>> .../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 2 ++
>>> .../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 2 ++
>>> tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++++-
>>> tools/memory-model/litmus-tests/MP+poonceonces.litmus | 5 ++++-
>>> .../litmus-tests/MP+pooncerelease+poacquireonce.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++++-
>>> tools/memory-model/litmus-tests/R+fencembonceonces.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/R+poonceonces.litmus | 5 ++++-
>>> .../litmus-tests/S+fencewmbonceonce+poacquireonce.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/S+poonceonces.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/SB+fencembonceonces.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/SB+poonceonces.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus | 5 ++++-
>>> tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5 ++++-
>>> .../litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus | 5 ++++-
>>> .../litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus | 7 ++++++-
>>> .../litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
>>> .../Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6 +++++-
>>> 32 files changed, 130 insertions(+), 31 deletions(-)
>>>
>>> diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
>>> index 967f9f2..772544f 100644
>>> --- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
>>> +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
>>> @@ -7,7 +7,9 @@ C CoRR+poonceonce+Once
>>> * reads from the same variable are ordered.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> +}
>>>
>>> P0(int *x)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
>>> index 4635739..5faae98 100644
>>> --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
>>> +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
>>> index bb068c9..77c9cc9 100644
>>> --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
>>> +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
>>> index 0d9f0a9..85ef746 100644
>>> --- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
>>> @@ -7,7 +7,9 @@ C CoWW+poonceonce
>>> * writes to the same variable are ordered.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> +}
>>>
>>> P0(int *x)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
>>> index e729d27..87aa900 100644
>>> --- a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
>>> +++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
>>> @@ -10,7 +10,10 @@ C IRIW+fencembonceonces+OnceOnce
>>> * process? This litmus test exercises LKMM's "propagation" rule.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
>>> index 4b54dd6..f84022d 100644
>>> --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
>>> +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
>>> @@ -10,7 +10,10 @@ C IRIW+poonceonces+OnceOnce
>>> * different process?
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
>>> index 094d58d..398f624 100644
>>> --- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
>>> index b321aa6..212a432 100644
>>> --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
>>> index 025b046..7afd856 100644
>>> --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
>>> index 4727f5a..c8a93c7 100644
>>> --- a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
>>> index 07b9904..2fa0295 100644
>>> --- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
>>> +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
>>> @@ -8,7 +8,10 @@ C LB+poacquireonce+pooncerelease
>>> * to the other?
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
>>> index 74c49cb..2107306 100644
>>> --- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
>>> @@ -7,7 +7,10 @@ C LB+poonceonces
>>> * be prevented even with no explicit ordering?
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
>>> index a273da9..e04b71b 100644
>>> --- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
>>> index 97731b4..18df682 100644
>>> --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
>>> @@ -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)
>>> diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
>>> index 50f4d62..b1b1266 100644
>>> --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
>>> @@ -11,6 +11,8 @@ C MP+polockmbonce+poacquiresilsil
>>> *)
>>>
>>> {
>>> + spinlock_t lo;
>>> + int x;
>>> }
>>>
>>> P0(spinlock_t *lo, int *x)
>>> diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
>>> index abf81e7..867c75d 100644
>>> --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
>>> @@ -11,6 +11,8 @@ C MP+polockonce+poacquiresilsil
>>> *)
>>>
>>> {
>>> + spinlock_t lo;
>>> + int x;
>>> }
>>>
>>> P0(spinlock_t *lo, int *x)
>>> diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
>>> index 712a4fcd..63e0f67 100644
>>> --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
>>> index 172f014..68180a4 100644
>>> --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
>>> @@ -7,7 +7,10 @@ C MP+poonceonces
>>> * no ordering at all?
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
>>> index d52c684..19f3e68 100644
>>> --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
>>> @@ -8,7 +8,10 @@ C MP+pooncerelease+poacquireonce
>>> * pattern.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
>>> index 72c9276..4ac189a 100644
>>> --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
>>> +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
>>> index 222a0b8..af9463b 100644
>>> --- a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
>>> @@ -9,7 +9,10 @@ C R+fencembonceonces
>>> * cause the resulting test to be allowed.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
>>> index 5386f12..bcd5574e 100644
>>> --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
>>> @@ -8,7 +8,10 @@ C R+poonceonces
>>> * store propagation delays.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
>>> index 1847982..c36341d 100644
>>> --- a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
>>> @@ -7,7 +7,10 @@ C S+fencewmbonceonce+poacquireonce
>>> * store against a subsequent store?
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
>>> index 8c9c2f8..7775c23 100644
>>> --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
>>> @@ -9,7 +9,10 @@ C S+poonceonces
>>> * READ_ONCE(), is ordering preserved?
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
>>> index ed5fff1..833cdfe 100644
>>> --- a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
>>> @@ -9,7 +9,10 @@ C SB+fencembonceonces
>>> * suffice, but not much else.)
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
>>> index 10d5507..c92211e 100644
>>> --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
>>> @@ -8,7 +8,10 @@ C SB+poonceonces
>>> * variable that the preceding process reads.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
>>> index 04a1660..84344b4 100644
>>> --- a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
>>> +++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
>>> index 6a2bc12..4314947 100644
>>> --- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
>>> +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
>>> @@ -8,7 +8,10 @@ C WRC+poonceonces+Once
>>> * test has no ordering at all.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
>>> index e994725..554999c 100644
>>> --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
>>> +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
>>> @@ -10,7 +10,10 @@ C WRC+pooncerelease+fencermbonceonce+Once
>>> * is A-cumulative in LKMM.
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> +}
>>>
>>> P0(int *x)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
>>> index 415248f..265a95f 100644
>>> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
>>> index 10a2aa0..0c9aea8 100644
>>> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
>>> @@ -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)
>>> {
>>> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
>>> index 88e70b8..661f9aa 100644
>>> --- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
>>> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
>>> @@ -14,7 +14,11 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
>>> * involving locking.)
>>> *)
>>>
>>> -{}
>>> +{
>>> + int x;
>>> + int y;
>>> + int z;
>>> +}
>>>
>>> P0(int *x, int *y)
>>> {
>>>
On Wed, Nov 25, 2020 at 08:34:47PM +0900, Akira Yokosawa wrote:
> On Thu, 5 Nov 2020 14:56:05 -0800, Paul E. McKenney wrote:
> > On Fri, Nov 06, 2020 at 07:41:48AM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> On 2020/11/06 7:00, [email protected] wrote:
> >>> From: "Paul E. McKenney" <[email protected]>
> >>>
> >>> This commit adds type information for global variables in the litmus
> >>> tests in order to allow easier use with klitmus7.
> >>
> >> IIUC, klitmus7 is happy with existing litmus tests under tools/memory-model.
> >> So I don't think this change is necessary.
> >>
> >> As a matter of fact, I was preparing a patch set to empty most of the
> >> initialization blocks in perfbook's CodeSamples/formal/ litmus tests.
> >
> > Heh! Someone asked for this change several months back, and I failed
> > to record who it was. If they don't object, I will remove this patch.
>
> Hi Paul,
>
> I'm seeing this patch still alive in the updated for-mingo-lkmm branch.
> Have you got some objection?
From git, which was not able to trivially revert. If you send me a
patch on top that removes the uneeded declarations and if someone
tests it with a klitmus run, I will take it for the merge window
following the upcoming one.
Thanx, Paul
> Thanks, Akira
>
> >
> > Thanx, Paul
> >
> >>>
> >>> Signed-off-by: Paul E. McKenney <[email protected]>
> >>> ---
> >>> tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4 +++-
> >>> tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4 +++-
> >>> tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus | 4 +++-
> >>> tools/memory-model/litmus-tests/CoWW+poonceonce.litmus | 4 +++-
> >>> .../litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5 ++++-
> >>> .../litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
> >>> tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6 +++++-
> >>> .../ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 6 +++++-
> >>> .../litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus | 5 ++++-
> >>> .../litmus-tests/LB+poacquireonce+pooncerelease.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/LB+poonceonces.litmus | 5 ++++-
> >>> .../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 5 +++--
> >>> .../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 2 ++
> >>> .../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 2 ++
> >>> tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++++-
> >>> tools/memory-model/litmus-tests/MP+poonceonces.litmus | 5 ++++-
> >>> .../litmus-tests/MP+pooncerelease+poacquireonce.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++++-
> >>> tools/memory-model/litmus-tests/R+fencembonceonces.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/R+poonceonces.litmus | 5 ++++-
> >>> .../litmus-tests/S+fencewmbonceonce+poacquireonce.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/S+poonceonces.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/SB+fencembonceonces.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/SB+poonceonces.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus | 5 ++++-
> >>> tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5 ++++-
> >>> .../litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus | 5 ++++-
> >>> .../litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus | 7 ++++++-
> >>> .../litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus | 7 ++++++-
> >>> .../Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6 +++++-
> >>> 32 files changed, 130 insertions(+), 31 deletions(-)
> >>>
> >>> diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> >>> index 967f9f2..772544f 100644
> >>> --- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> >>> +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
> >>> @@ -7,7 +7,9 @@ C CoRR+poonceonce+Once
> >>> * reads from the same variable are ordered.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> +}
> >>>
> >>> P0(int *x)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> >>> index 4635739..5faae98 100644
> >>> --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> >>> +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> >>> index bb068c9..77c9cc9 100644
> >>> --- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> >>> +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> >>> index 0d9f0a9..85ef746 100644
> >>> --- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
> >>> @@ -7,7 +7,9 @@ C CoWW+poonceonce
> >>> * writes to the same variable are ordered.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> +}
> >>>
> >>> P0(int *x)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> >>> index e729d27..87aa900 100644
> >>> --- a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
> >>> @@ -10,7 +10,10 @@ C IRIW+fencembonceonces+OnceOnce
> >>> * process? This litmus test exercises LKMM's "propagation" rule.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> >>> index 4b54dd6..f84022d 100644
> >>> --- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
> >>> @@ -10,7 +10,10 @@ C IRIW+poonceonces+OnceOnce
> >>> * different process?
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >>> index 094d58d..398f624 100644
> >>> --- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> >>> index b321aa6..212a432 100644
> >>> --- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> >>> index 025b046..7afd856 100644
> >>> --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> >>> index 4727f5a..c8a93c7 100644
> >>> --- a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> >>> index 07b9904..2fa0295 100644
> >>> --- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> >>> +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
> >>> @@ -8,7 +8,10 @@ C LB+poacquireonce+pooncerelease
> >>> * to the other?
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> >>> index 74c49cb..2107306 100644
> >>> --- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
> >>> @@ -7,7 +7,10 @@ C LB+poonceonces
> >>> * be prevented even with no explicit ordering?
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> >>> index a273da9..e04b71b 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> >>> index 97731b4..18df682 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
> >>> @@ -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)
> >>> diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> >>> index 50f4d62..b1b1266 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> >>> @@ -11,6 +11,8 @@ C MP+polockmbonce+poacquiresilsil
> >>> *)
> >>>
> >>> {
> >>> + spinlock_t lo;
> >>> + int x;
> >>> }
> >>>
> >>> P0(spinlock_t *lo, int *x)
> >>> diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> >>> index abf81e7..867c75d 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> >>> @@ -11,6 +11,8 @@ C MP+polockonce+poacquiresilsil
> >>> *)
> >>>
> >>> {
> >>> + spinlock_t lo;
> >>> + int x;
> >>> }
> >>>
> >>> P0(spinlock_t *lo, int *x)
> >>> diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
> >>> index 712a4fcd..63e0f67 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+polocks.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> >>> index 172f014..68180a4 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
> >>> @@ -7,7 +7,10 @@ C MP+poonceonces
> >>> * no ordering at all?
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> >>> index d52c684..19f3e68 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
> >>> @@ -8,7 +8,10 @@ C MP+pooncerelease+poacquireonce
> >>> * pattern.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> >>> index 72c9276..4ac189a 100644
> >>> --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> >>> +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> >>> index 222a0b8..af9463b 100644
> >>> --- a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
> >>> @@ -9,7 +9,10 @@ C R+fencembonceonces
> >>> * cause the resulting test to be allowed.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> >>> index 5386f12..bcd5574e 100644
> >>> --- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
> >>> @@ -8,7 +8,10 @@ C R+poonceonces
> >>> * store propagation delays.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> >>> index 1847982..c36341d 100644
> >>> --- a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
> >>> @@ -7,7 +7,10 @@ C S+fencewmbonceonce+poacquireonce
> >>> * store against a subsequent store?
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> >>> index 8c9c2f8..7775c23 100644
> >>> --- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
> >>> @@ -9,7 +9,10 @@ C S+poonceonces
> >>> * READ_ONCE(), is ordering preserved?
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> >>> index ed5fff1..833cdfe 100644
> >>> --- a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
> >>> @@ -9,7 +9,10 @@ C SB+fencembonceonces
> >>> * suffice, but not much else.)
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> >>> index 10d5507..c92211e 100644
> >>> --- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
> >>> @@ -8,7 +8,10 @@ C SB+poonceonces
> >>> * variable that the preceding process reads.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> >>> index 04a1660..84344b4 100644
> >>> --- a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> >>> +++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> >>> index 6a2bc12..4314947 100644
> >>> --- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> >>> +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
> >>> @@ -8,7 +8,10 @@ C WRC+poonceonces+Once
> >>> * test has no ordering at all.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> >>> index e994725..554999c 100644
> >>> --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> >>> +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
> >>> @@ -10,7 +10,10 @@ C WRC+pooncerelease+fencermbonceonce+Once
> >>> * is A-cumulative in LKMM.
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> +}
> >>>
> >>> P0(int *x)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> >>> index 415248f..265a95f 100644
> >>> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> >>> index 10a2aa0..0c9aea8 100644
> >>> --- a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus
> >>> @@ -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)
> >>> {
> >>> diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> >>> index 88e70b8..661f9aa 100644
> >>> --- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> >>> +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
> >>> @@ -14,7 +14,11 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
> >>> * involving locking.)
> >>> *)
> >>>
> >>> -{}
> >>> +{
> >>> + int x;
> >>> + int y;
> >>> + int z;
> >>> +}
> >>>
> >>> P0(int *x, int *y)
> >>> {
> >>>
On Fri, 27 Nov 2020 07:46:52 -0800, Paul E. McKenney wrote:
> On Wed, Nov 25, 2020 at 08:34:47PM +0900, Akira Yokosawa wrote:
[...]
>> Hi Paul,
>>
>> I'm seeing this patch still alive in the updated for-mingo-lkmm branch.
>> Have you got some objection?
>
> From git, which was not able to trivially revert.
;-) ;-)
> If you send me a
> patch on top that removes the uneeded declarations and if someone
> tests it with a klitmus run, I will take it for the merge window
> following the upcoming one.
Got it!
I'm submitting a patch set in reply to this mail.
1/2 is the removal of those redundant type declarations.
2/2 is an obvious fix of typo I made in the klitmus7 compat table.
Thanks, Akira
>
> Thanx, Paul
>
>> Thanks, Akira
>>