* [PATCH memory-model 1/8] tools: memory-model: Document that the LKMM can easily miss control dependencies
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
@ 2020-11-05 22:00 ` paulmck
2020-11-05 22:00 ` [PATCH memory-model 2/8] tools/memory-model: Move Documentation description to Documentation/README paulmck
` (6 subsequent siblings)
7 siblings, 0 replies; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E . McKenney
From: Alan Stern <stern@rowland.harvard.edu>
Add a small section to the litmus-tests.txt documentation file for
the Linux Kernel Memory Model explaining that the memory model often
fails to recognize certain control dependencies.
Suggested-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
tools/memory-model/Documentation/litmus-tests.txt | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt
index 2f840dc..8a9d5d2 100644
--- a/tools/memory-model/Documentation/litmus-tests.txt
+++ b/tools/memory-model/Documentation/litmus-tests.txt
@@ -946,6 +946,23 @@ Limitations of the Linux-kernel memory model (LKMM) include:
carrying a dependency, then the compiler can break that dependency
by substituting a constant of that value.
+ Conversely, LKMM sometimes doesn't recognize that a particular
+ optimization is not allowed, and as a result, thinks that a
+ dependency is not present (because the optimization would break it).
+ The memory model misses some pretty obvious control dependencies
+ because of this limitation. A simple example is:
+
+ r1 = READ_ONCE(x);
+ if (r1 == 0)
+ smp_mb();
+ WRITE_ONCE(y, 1);
+
+ There is a control dependency from the READ_ONCE to the WRITE_ONCE,
+ even when r1 is nonzero, but LKMM doesn't realize this and thinks
+ that the write may execute before the read if r1 != 0. (Yes, that
+ doesn't make sense if you think about it, but the memory model's
+ intelligence is limited.)
+
2. Multiple access sizes for a single variable are not supported,
and neither are misaligned or partially overlapping accesses.
--
2.9.5
^ permalink raw reply related [flat|nested] 29+ messages in thread* [PATCH memory-model 2/8] tools/memory-model: Move Documentation description to Documentation/README
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
2020-11-05 22:00 ` [PATCH memory-model 1/8] tools: memory-model: Document that the LKMM can easily miss control dependencies paulmck
@ 2020-11-05 22:00 ` paulmck
2020-11-05 22:00 ` [PATCH memory-model 3/8] tools/memory-model: Document categories of ordering primitives paulmck
` (5 subsequent siblings)
7 siblings, 0 replies; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E. McKenney
From: "Paul E. McKenney" <paulmck@kernel.org>
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 <paulmck@kernel.org>
---
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
^ permalink raw reply related [flat|nested] 29+ messages in thread* [PATCH memory-model 3/8] tools/memory-model: Document categories of ordering primitives
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
2020-11-05 22:00 ` [PATCH memory-model 1/8] tools: memory-model: Document that the LKMM can easily miss control dependencies paulmck
2020-11-05 22:00 ` [PATCH memory-model 2/8] tools/memory-model: Move Documentation description to Documentation/README paulmck
@ 2020-11-05 22:00 ` paulmck
2020-11-06 16:56 ` Alan Stern
2020-11-05 22:00 ` [PATCH memory-model 4/8] docs/memory-barriers.txt: Fix a typo in CPU MEMORY BARRIERS section paulmck
` (4 subsequent siblings)
7 siblings, 1 reply; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E. McKenney
From: "Paul E. McKenney" <paulmck@kernel.org>
The Linux kernel has a number of categories of ordering primitives, which
are recorded in the LKMM implementation and hinted at by cheatsheet.txt.
But there is no overview of these categories, and such an overview
is needed in order to understand multithreaded LKMM litmus tests.
This commit therefore adds an ordering.txt as well as extracting a
control-dependencies.txt from memory-barriers.txt. It also updates the
README file.
[ paulmck: Apply Akira Yokosawa file-placement feedback. ]
[ paulmck: Apply Alan Stern feedback. ]
[ paulmck: Apply self-review feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
tools/memory-model/Documentation/README | 19 +-
.../Documentation/control-dependencies.txt | 258 ++++++++++
tools/memory-model/Documentation/ordering.txt | 557 +++++++++++++++++++++
3 files changed, 833 insertions(+), 1 deletion(-)
create mode 100644 tools/memory-model/Documentation/control-dependencies.txt
create mode 100644 tools/memory-model/Documentation/ordering.txt
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
index 2d9539f..a50ea81 100644
--- a/tools/memory-model/Documentation/README
+++ b/tools/memory-model/Documentation/README
@@ -11,6 +11,12 @@ the material provided by documents earlier in this list.
o You are new to Linux-kernel concurrency: simple.txt
+o You have some background in Linux-kernel concurrency, and would
+ like an overview of the types of low-level concurrency primitives
+ that the Linux kernel provides: ordering.txt
+
+ Here, "low level" means atomic operations to single variables.
+
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
@@ -19,6 +25,9 @@ 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 would like a detailed understanding of what your compiler can
+ and cannot do to control dependencies: control-dependencies.txt
+
o You are familiar with Linux-kernel concurrency and the use of
LKMM, and would like a quick reference: cheatsheet.txt
@@ -41,13 +50,21 @@ README
cheatsheet.txt
Quick-reference guide to the Linux-kernel memory model.
+control-dependencies.txt
+ Guide to preventing compiler optimizations from destroying
+ your control dependencies.
+
explanation.txt
- Detailed description of the memory model.
+ Detailed description of the memory model in detail.
litmus-tests.txt
The format, features, capabilities, and limitations of the litmus
tests that LKMM can evaluate.
+ordering.txt
+ Overview of the Linux kernel's low-level memory-ordering
+ primitives by category.
+
recipes.txt
Common memory-ordering patterns.
diff --git a/tools/memory-model/Documentation/control-dependencies.txt b/tools/memory-model/Documentation/control-dependencies.txt
new file mode 100644
index 0000000..8b743d20
--- /dev/null
+++ b/tools/memory-model/Documentation/control-dependencies.txt
@@ -0,0 +1,258 @@
+CONTROL DEPENDENCIES
+====================
+
+A major difficulty with control dependencies is that current compilers
+do not support them. One purpose of this document is therefore to
+help you prevent your compiler from breaking your code. However,
+control dependencies also pose other challenges, which leads to the
+second purpose of this document, namely to help you to avoid breaking
+your own code, even in the absence of help from your compiler.
+
+One such challenge is that control dependencies order only later stores.
+Therefore, a load-load control dependency will not preserve ordering
+unless a read memory barrier is provided. Consider the following code:
+
+ q = READ_ONCE(a);
+ if (q)
+ p = READ_ONCE(b);
+
+This is not guaranteed to provide any ordering because some types of CPUs
+are permitted to predict the result of the load from "b". This prediction
+can cause other CPUs to see this load as having happened before the load
+from "a". This means that an explicit read barrier is required, for example
+as follows:
+
+ q = READ_ONCE(a);
+ if (q) {
+ smp_rmb();
+ p = READ_ONCE(b);
+ }
+
+However, stores are not speculated. This means that ordering is
+(usually) guaranteed for load-store control dependencies, as in the
+following example:
+
+ q = READ_ONCE(a);
+ if (q)
+ WRITE_ONCE(b, 1);
+
+Control dependencies can pair with each other and with other types
+of ordering. But please note that neither the READ_ONCE() nor the
+WRITE_ONCE() are optional. Without the READ_ONCE(), the compiler might
+fuse the load from "a" with other loads. Without the WRITE_ONCE(),
+the compiler might fuse the store to "b" with other stores. Worse yet,
+the compiler might convert the store into a load and a check followed
+by a store, and this compiler-generated load would not be ordered by
+the control dependency.
+
+Furthermore, if the compiler is able to prove that the value of variable
+"a" is always non-zero, it would be well within its rights to optimize
+the original example by eliminating the "if" statement as follows:
+
+ q = a;
+ b = 1; /* BUG: Compiler and CPU can both reorder!!! */
+
+So don't leave out either the READ_ONCE() or the WRITE_ONCE().
+In particular, although READ_ONCE() does force the compiler to emit a
+load, it does *not* force the compiler to actually use the loaded value.
+
+It is tempting to try use control dependencies to enforce ordering on
+identical stores on both branches of the "if" statement as follows:
+
+ q = READ_ONCE(a);
+ if (q) {
+ barrier();
+ WRITE_ONCE(b, 1);
+ do_something();
+ } else {
+ barrier();
+ WRITE_ONCE(b, 1);
+ do_something_else();
+ }
+
+Unfortunately, current compilers will transform this as follows at high
+optimization levels:
+
+ q = READ_ONCE(a);
+ barrier();
+ WRITE_ONCE(b, 1); /* BUG: No ordering vs. load from a!!! */
+ if (q) {
+ /* WRITE_ONCE(b, 1); -- moved up, BUG!!! */
+ do_something();
+ } else {
+ /* WRITE_ONCE(b, 1); -- moved up, BUG!!! */
+ do_something_else();
+ }
+
+Now there is no conditional between the load from "a" and the store to
+"b", which means that the CPU is within its rights to reorder them: The
+conditional is absolutely required, and must be present in the final
+assembly code, after all of the compiler and link-time optimizations
+have been applied. Therefore, if you need ordering in this example,
+you must use explicit memory ordering, for example, smp_store_release():
+
+ q = READ_ONCE(a);
+ if (q) {
+ smp_store_release(&b, 1);
+ do_something();
+ } else {
+ smp_store_release(&b, 1);
+ do_something_else();
+ }
+
+Without explicit memory ordering, control-dependency-based ordering is
+guaranteed only when the stores differ, for example:
+
+ q = READ_ONCE(a);
+ if (q) {
+ WRITE_ONCE(b, 1);
+ do_something();
+ } else {
+ WRITE_ONCE(b, 2);
+ do_something_else();
+ }
+
+The initial READ_ONCE() is still required to prevent the compiler from
+knowing too much about the value of "a".
+
+But please note that you need to be careful what you do with the local
+variable "q", otherwise the compiler might be able to guess the value
+and again remove the conditional branch that is absolutely required to
+preserve ordering. For example:
+
+ q = READ_ONCE(a);
+ if (q % MAX) {
+ WRITE_ONCE(b, 1);
+ do_something();
+ } else {
+ WRITE_ONCE(b, 2);
+ do_something_else();
+ }
+
+If MAX is compile-time defined to be 1, then the compiler knows that
+(q % MAX) must be equal to zero, regardless of the value of "q".
+The compiler is therefore within its rights to transform the above code
+into the following:
+
+ q = READ_ONCE(a);
+ WRITE_ONCE(b, 2);
+ do_something_else();
+
+Given this transformation, the CPU is not required to respect the ordering
+between the load from variable "a" and the store to variable "b". It is
+tempting to add a barrier(), but this does not help. The conditional
+is gone, and the barrier won't bring it back. Therefore, if you need
+to relying on control dependencies to produce this ordering, you should
+make sure that MAX is greater than one, perhaps as follows:
+
+ q = READ_ONCE(a);
+ BUILD_BUG_ON(MAX <= 1); /* Order load from a with store to b. */
+ if (q % MAX) {
+ WRITE_ONCE(b, 1);
+ do_something();
+ } else {
+ WRITE_ONCE(b, 2);
+ do_something_else();
+ }
+
+Please note once again that each leg of the "if" statement absolutely
+must store different values to "b". As in previous examples, if the two
+values were identical, the compiler could pull this store outside of the
+"if" statement, destroying the control dependency's ordering properties.
+
+You must also be careful avoid relying too much on boolean short-circuit
+evaluation. Consider this example:
+
+ q = READ_ONCE(a);
+ if (q || 1 > 0)
+ WRITE_ONCE(b, 1);
+
+Because the first condition cannot fault and the second condition is
+always true, the compiler can transform this example as follows, again
+destroying the control dependency's ordering:
+
+ q = READ_ONCE(a);
+ WRITE_ONCE(b, 1);
+
+This is yet another example showing the importance of preventing the
+compiler from out-guessing your code. Again, although READ_ONCE() really
+does force the compiler to emit code for a given load, the compiler is
+within its rights to discard the loaded value.
+
+In addition, control dependencies apply only to the then-clause and
+else-clause of the "if" statement in question. In particular, they do
+not necessarily order the code following the entire "if" statement:
+
+ q = READ_ONCE(a);
+ if (q) {
+ WRITE_ONCE(b, 1);
+ } else {
+ WRITE_ONCE(b, 2);
+ }
+ WRITE_ONCE(c, 1); /* BUG: No ordering against the read from "a". */
+
+It is tempting to argue that there in fact is ordering because the
+compiler cannot reorder volatile accesses and also cannot reorder
+the writes to "b" with the condition. Unfortunately for this line
+of reasoning, the compiler might compile the two writes to "b" as
+conditional-move instructions, as in this fanciful pseudo-assembly
+language:
+
+ ld r1,a
+ cmp r1,$0
+ cmov,ne r4,$1
+ cmov,eq r4,$2
+ st r4,b
+ st $1,c
+
+The control dependencies would then extend only to the pair of cmov
+instructions and the store depending on them. This means that a weakly
+ordered CPU would have no dependency of any sort between the load from
+"a" and the store to "c". In short, control dependencies provide ordering
+only to the stores in the then-clause and else-clause of the "if" statement
+in question (including functions invoked by those two clauses), and not
+to code following that "if" statement.
+
+
+In summary:
+
+ (*) Control dependencies can order prior loads against later stores.
+ However, they do *not* guarantee any other sort of ordering:
+ Not prior loads against later loads, nor prior stores against
+ later anything. If you need these other forms of ordering, use
+ smp_load_acquire(), smp_store_release(), or, in the case of prior
+ stores and later loads, smp_mb().
+
+ (*) If both legs of the "if" statement contain identical stores to
+ the same variable, then you must explicitly order those stores,
+ either by preceding both of them with smp_mb() or by using
+ smp_store_release(). Please note that it is *not* sufficient to use
+ barrier() at beginning and end of each leg of the "if" statement
+ because, as shown by the example above, optimizing compilers can
+ destroy the control dependency while respecting the letter of the
+ barrier() law.
+
+ (*) Control dependencies require at least one run-time conditional
+ between the prior load and the subsequent store, and this
+ conditional must involve the prior load. If the compiler is able
+ to optimize the conditional away, it will have also optimized
+ away the ordering. Careful use of READ_ONCE() and WRITE_ONCE()
+ can help to preserve the needed conditional.
+
+ (*) Control dependencies require that the compiler avoid reordering the
+ dependency into nonexistence. Careful use of READ_ONCE() or
+ atomic{,64}_read() can help to preserve your control dependency.
+
+ (*) Control dependencies apply only to the then-clause and else-clause
+ of the "if" statement containing the control dependency, including
+ any functions that these two clauses call. Control dependencies
+ do *not* apply to code beyond the end of that "if" statement.
+
+ (*) Control dependencies pair normally with other types of barriers.
+
+ (*) Control dependencies do *not* provide multicopy atomicity. If you
+ need all the CPUs to agree on the ordering of a given store against
+ all other accesses, use smp_mb().
+
+ (*) Compilers do not understand control dependencies. It is therefore
+ your job to ensure that they do not break your code.
diff --git a/tools/memory-model/Documentation/ordering.txt b/tools/memory-model/Documentation/ordering.txt
new file mode 100644
index 0000000..46369f4
--- /dev/null
+++ b/tools/memory-model/Documentation/ordering.txt
@@ -0,0 +1,557 @@
+This document gives an overview of the categories of memory-ordering
+operations provided by the Linux-kernel memory model (LKMM).
+
+
+Categories of Ordering
+======================
+
+This section lists LKMM's three top-level categories of memory-ordering
+operations in decreasing order of strength:
+
+1. Barriers (also known as "fences"). A barrier orders some or
+ all of the CPU's prior operations against some or all of its
+ subsequent operations.
+
+2. Ordered memory accesses. These operations order themselves
+ against some or all of the CPU's prior accesses or some or all
+ of the CPU's subsequent accesses, depending on the subcategory
+ of the operation.
+
+3. Unordered accesses, as the name indicates, have no ordering
+ properties except to the extent that they interact with an
+ operation in the previous categories. This being the real world,
+ some of these "unordered" operations provide limited ordering
+ in some special situations.
+
+Each of the above categories is described in more detail by one of the
+following sections.
+
+
+Barriers
+========
+
+Each of the following categories of barriers is described in its own
+subsection below:
+
+a. Full memory barriers.
+
+b. Read-modify-write (RMW) ordering augmentation barriers.
+
+c. Write memory barrier.
+
+d. Read memory barrier.
+
+e. Compiler barrier.
+
+Note well that many of these primitives generate absolutely no code
+in kernels built with CONFIG_SMP=n. Therefore, if you are writing
+a device driver, which must correctly order accesses to a physical
+device even in kernels built with CONFIG_SMP=n, please use the
+ordering primitives provided for that purpose. For example, instead of
+smp_mb(), use mb(). See the "Linux Kernel Device Drivers" book or the
+https://lwn.net/Articles/698014/ article for more information.
+
+
+Full Memory Barriers
+--------------------
+
+The Linux-kernel primitives that provide full ordering include:
+
+o The smp_mb() full memory barrier.
+
+o Value-returning RMW atomic operations whose names do not end in
+ _acquire, _release, or _relaxed.
+
+o RCU's grace-period primitives.
+
+First, the smp_mb() full memory barrier orders all of the CPU's prior
+accesses against all subsequent accesses from the viewpoint of all CPUs.
+In other words, all CPUs will agree that any earlier action taken
+by that CPU happened before any later action taken by that same CPU.
+For example, consider the following:
+
+ WRITE_ONCE(x, 1);
+ smp_mb(); // Order store to x before load from y.
+ r1 = READ_ONCE(y);
+
+All CPUs will agree that the store to "x" happened before the load
+from "y", as indicated by the comment. And yes, please comment your
+memory-ordering primitives. It is surprisingly hard to remember their
+purpose after even a few months.
+
+Second, some RMW atomic operations provide full ordering. These
+operations include value-returning RMW atomic operations (that is, those
+with non-void return types) whose names do not end in _acquire, _release,
+or _relaxed. Examples include atomic_add_return(), atomic_dec_and_test(),
+cmpxchg(), and xchg(). Note that conditional RMW atomic operations such
+as cmpxchg() are only guaranteed to provide ordering when they succeed.
+When RMW atomic operations provide full ordering, they partition the
+CPU's accesses into three groups:
+
+1. All code that executed prior to the RMW atomic operation.
+
+2. The RMW atomic operation itself.
+
+3. All code that executed after the RMW atomic operation.
+
+All CPUs will agree that any operation in a given partition happened
+before any operation in a higher-numbered partition.
+
+In contrast, non-value-returning RMW atomic operations (that is, those
+with void return types) do not guarantee any ordering whatsoever. Nor do
+value-returning RMW atomic operations whose names end in _relaxed.
+Examples of the former include atomic_inc() and atomic_dec(),
+while examples of the latter include atomic_cmpxchg_relaxed() and
+atomic_xchg_relaxed(). Similarly, value-returning non-RMW atomic
+operations such as atomic_read() do not guarantee full ordering, and
+are covered in the later section on unordered operations.
+
+Value-returning RMW atomic operations whose names end in _acquire or
+_release provide limited ordering, and will be described later in this
+document.
+
+Finally, RCU's grace-period primitives provide full ordering. These
+primitives include synchronize_rcu(), synchronize_rcu_expedited(),
+synchronize_srcu() and so on. However, these primitives have orders
+of magnitude greater overhead than smp_mb(), atomic_xchg(), and so on.
+Furthermore, RCU's grace-period primitives can only be invoked in
+sleepable contexts. Therefore, RCU's grace-period primitives are
+typically instead used to provide ordering against RCU read-side critical
+sections, as documented in their comment headers. But of course if you
+need a synchronize_rcu() to interact with readers, it costs you nothing
+to also rely on its additional full-memory-barrier semantics. Just please
+carefully comment this, otherwise your future self will hate you.
+
+
+RMW Ordering Augmentation Barriers
+----------------------------------
+
+As noted in the previous section, non-value-returning RMW operations
+such as atomic_inc() and atomic_dec() guarantee no ordering whatsoever.
+Nevertheless, a number of popular CPU families, including x86, provide
+full ordering for these primitives. One way to obtain full ordering on
+all architectures is to add a call to smp_mb():
+
+ WRITE_ONCE(x, 1);
+ atomic_inc(&my_counter);
+ smp_mb(); // Inefficient on x86!!!
+ r1 = READ_ONCE(y);
+
+This works, but the added smp_mb() adds needless overhead for
+x86, on which atomic_inc() provides full ordering all by itself.
+The smp_mb__after_atomic() primitive can be used instead:
+
+ WRITE_ONCE(x, 1);
+ atomic_inc(&my_counter);
+ smp_mb__after_atomic(); // Order store to x before load from y.
+ r1 = READ_ONCE(y);
+
+The smp_mb__after_atomic() primitive emits code only on CPUs whose
+atomic_inc() implementations do not guarantee full ordering, thus
+incurring no unnecessary overhead on x86. There are a number of
+variations on the smp_mb__*() theme:
+
+o smp_mb__before_atomic(), which provides full ordering prior
+ to an unordered RMW atomic operation.
+
+o smp_mb__after_atomic(), which, as shown above, provides full
+ ordering subsequent to an unordered RMW atomic operation.
+
+o smp_mb__after_spinlock(), which provides full ordering subsequent
+ to a successful spinlock acquisition. Note that spin_lock() is
+ always successful but spin_trylock() might not be.
+
+o smp_mb__after_srcu_read_unlock(), which provides full ordering
+ subsequent to an srcu_read_unlock().
+
+It is bad practice to place code between the smp__*() primitive and the
+operation whose ordering that it is augmenting. The reason is that the
+ordering of this intervening code will differ from one CPU architecture
+to another.
+
+
+Write Memory Barrier
+--------------------
+
+The Linux kernel's write memory barrier is smp_wmb(). If a CPU executes
+the following code:
+
+ WRITE_ONCE(x, 1);
+ smp_wmb();
+ WRITE_ONCE(y, 1);
+
+Then any given CPU will see the write to "x" has having happened before
+the write to "y". However, you are usually better off using a release
+store, as described in the "Release Operations" section below.
+
+Note that smp_wmb() might fail to provide ordering for unmarked C-language
+stores because profile-driven optimization could determine that the
+value being overwritten is almost always equal to the new value. Such a
+compiler might then reasonably decide to transform "x = 1" and "y = 1"
+as follows:
+
+ if (x != 1)
+ x = 1;
+ smp_wmb(); // BUG: does not order the reads!!!
+ if (y != 1)
+ y = 1;
+
+Therefore, if you need to use smp_wmb() with unmarked C-language writes,
+you will need to make sure that none of the compilers used to build
+the Linux kernel carry out this sort of transformation, both now and in
+the future.
+
+
+Read Memory Barrier
+-------------------
+
+The Linux kernel's read memory barrier is smp_rmb(). If a CPU executes
+the following code:
+
+ r0 = READ_ONCE(y);
+ smp_rmb();
+ r1 = READ_ONCE(x);
+
+Then any given CPU will see the read from "y" as having preceded the read from
+"x". However, you are usually better off using an acquire load, as described
+in the "Acquire Operations" section below.
+
+Compiler Barrier
+----------------
+
+The Linux kernel's compiler barrier is barrier(). This primitive
+prohibits compiler code-motion optimizations that might move memory
+references across the point in the code containing the barrier(), but
+does not constrain hardware memory ordering. For example, this can be
+used to prevent to compiler from moving code across an infinite loop:
+
+ WRITE_ONCE(x, 1);
+ while (dontstop)
+ barrier();
+ r1 = READ_ONCE(y);
+
+Without the barrier(), the compiler would be within its rights to move the
+WRITE_ONCE() to follow the loop. This code motion could be problematic
+in the case where an interrupt handler terminates the loop. Another way
+to handle this is to use READ_ONCE() for the load of "dontstop".
+
+Note that the barriers discussed previously use barrier() or its low-level
+equivalent in their implementations.
+
+
+Ordered Memory Accesses
+=======================
+
+The Linux kernel provides a wide variety of ordered memory accesses:
+
+a. Release operations.
+
+b. Acquire operations.
+
+c. RCU read-side ordering.
+
+d. Control dependencies.
+
+Each of the above categories has its own section below.
+
+
+Release Operations
+------------------
+
+Release operations include smp_store_release(), atomic_set_release(),
+rcu_assign_pointer(), and value-returning RMW operations whose names
+end in _release. These operations order their own store against all
+of the CPU's prior memory accesses. Release operations often provide
+improved readability and performance compared to explicit barriers.
+For example, use of smp_store_release() saves a line compared to the
+smp_wmb() example above:
+
+ WRITE_ONCE(x, 1);
+ smp_store_release(&y, 1);
+
+More important, smp_store_release() makes it easier to connect up the
+different pieces of the concurrent algorithm. The variable stored to
+by the smp_store_release(), in this case "y", will normally be used in
+an acquire operation in other parts of the concurrent algorithm.
+
+To see the performance advantages, suppose that the above example read
+from "x" instead of writing to it. Then an smp_wmb() could not guarantee
+ordering, and an smp_mb() would be needed instead:
+
+ r1 = READ_ONCE(x);
+ smp_mb();
+ WRITE_ONCE(y, 1);
+
+But smp_mb() often incurs much higher overhead than does
+smp_store_release(), which still provides the needed ordering of "x"
+against "y". On x86, the version using smp_store_release() might compile
+to a simple load instruction followed by a simple store instruction.
+In contrast, the smp_mb() compiles to an expensive instruction that
+provides the needed ordering.
+
+There is a wide variety of release operations:
+
+o Store operations, including not only the aforementioned
+ smp_store_release(), but also atomic_set_release(), and
+ atomic_long_set_release().
+
+o RCU's rcu_assign_pointer() operation. This is the same as
+ smp_store_release() except that: (1) It takes the pointer to
+ be assigned to instead of a pointer to that pointer, (2) It
+ is intended to be used in conjunction with rcu_dereference()
+ and similar rather than smp_load_acquire(), and (3) It checks
+ for an RCU-protected pointer in "sparse" runs.
+
+o Value-returning RMW operations whose names end in _release,
+ such as atomic_fetch_add_release() and cmpxchg_release().
+ Note that release ordering is guaranteed only against the
+ memory-store portion of the RMW operation, and not against the
+ memory-load portion. Note also that conditional operations such
+ as cmpxchg_release() are only guaranteed to provide ordering
+ when they succeed.
+
+As mentioned earlier, release operations are often paired with acquire
+operations, which are the subject of the next section.
+
+
+Acquire Operations
+------------------
+
+Acquire operations include smp_load_acquire(), atomic_read_acquire(),
+and value-returning RMW operations whose names end in _acquire. These
+operations order their own load against all of the CPU's subsequent
+memory accesses. Acquire operations often provide improved performance
+and readability compared to explicit barriers. For example, use of
+smp_load_acquire() saves a line compared to the smp_rmb() example above:
+
+ r0 = smp_load_acquire(&y);
+ r1 = READ_ONCE(x);
+
+As with smp_store_release(), this also makes it easier to connect
+the different pieces of the concurrent algorithm by looking for the
+smp_store_release() that stores to "y". In addition, smp_load_acquire()
+improves upon smp_rmb() by ordering against subsequent stores as well
+as against subsequent loads.
+
+There are a couple of categories of acquire operations:
+
+o Load operations, including not only the aforementioned
+ smp_load_acquire(), but also atomic_read_acquire(), and
+ atomic64_read_acquire().
+
+o Value-returning RMW operations whose names end in _acquire,
+ such as atomic_xchg_acquire() and atomic_cmpxchg_acquire().
+ Note that acquire ordering is guaranteed only against the
+ memory-load portion of the RMW operation, and not against the
+ memory-store portion. Note also that conditional operations
+ such as atomic_cmpxchg_acquire() are only guaranteed to provide
+ ordering when they succeed.
+
+Symmetry being what it is, acquire operations are often paired with the
+release operations covered earlier. For example, consider the following
+example, where task0() and task1() execute concurrently:
+
+ void task0(void)
+ {
+ WRITE_ONCE(x, 1);
+ smp_store_release(&y, 1);
+ }
+
+ void task1(void)
+ {
+ r0 = smp_load_acquire(&y);
+ r1 = READ_ONCE(x);
+ }
+
+If "x" and "y" are both initially zero, then either r0's final value
+will be zero or r1's final value will be one, thus providing the required
+ordering.
+
+
+RCU Read-Side Ordering
+----------------------
+
+This category includes read-side markers such as rcu_read_lock()
+and rcu_read_unlock() as well as pointer-traversal primitives such as
+rcu_dereference() and srcu_dereference().
+
+Compared to locking primitives and RMW atomic operations, markers
+for RCU read-side critical sections incur very low overhead because
+they interact only with the corresponding grace-period primitives.
+For example, the rcu_read_lock() and rcu_read_unlock() markers interact
+with synchronize_rcu(), synchronize_rcu_expedited(), and call_rcu().
+The way this works is that if a given call to synchronize_rcu() cannot
+prove that it started before a given call to rcu_read_lock(), then
+that synchronize_rcu() must block until the matching rcu_read_unlock()
+is reached. For more information, please see the synchronize_rcu()
+docbook header comment and the material in Documentation/RCU.
+
+RCU's pointer-traversal primitives, including rcu_dereference() and
+srcu_dereference(), order their load (which must be a pointer) against any
+of the CPU's subsequent memory accesses whose address has been calculated
+from the value loaded. There is said to be an *address dependency*
+from the value returned by the rcu_dereference() or srcu_dereference()
+to that subsequent memory access.
+
+A call to rcu_dereference() for a given RCU-protected pointer is
+usually paired with a call to a call to rcu_assign_pointer() for that
+same pointer in much the same way that a call to smp_load_acquire() is
+paired with a call to smp_store_release(). Calls to rcu_dereference()
+and rcu_assign_pointer are often buried in other APIs, for example,
+the RCU list API members defined in include/linux/rculist.h. For more
+information, please see the docbook headers in that file, the most
+recent LWN article on the RCU API (https://lwn.net/Articles/777036/),
+and of course the material in Documentation/RCU.
+
+If the pointer value is manipulated between the rcu_dereference()
+that returned it and a later dereference(), please read
+Documentation/RCU/rcu_dereference.rst. It can also be quite helpful to
+review uses in the Linux kernel.
+
+
+Control Dependencies
+--------------------
+
+A control dependency extends from a marked load (READ_ONCE() or stronger)
+through an "if" condition to a marked store (WRITE_ONCE() or stronger)
+that is executed only by one of the legs of that "if" statement.
+Control dependencies are so named because they are mediated by
+control-flow instructions such as comparisons and conditional branches.
+
+In short, you can use a control dependency to enforce ordering between
+an READ_ONCE() and a WRITE_ONCE() when there is an "if" condition
+between them. The canonical example is as follows:
+
+ q = READ_ONCE(a);
+ if (q)
+ WRITE_ONCE(b, 1);
+
+In this case, all CPUs would see the read from "a" as happening before
+the write to "b".
+
+However, control dependencies are easily destroyed by compiler
+optimizations, so any use of control dependencies must take into account
+all of the compilers used to build the Linux kernel. Please see the
+"control-dependencies.txt" file for more information.
+
+
+Unordered Accesses
+==================
+
+Each of these two categories of unordered accesses has a section below:
+
+a. Unordered marked operations.
+
+b. Unmarked C-language accesses.
+
+
+Unordered Marked Operations
+---------------------------
+
+Unordered operations to different variables are just that, unordered.
+However, if a group of CPUs apply these operations to a single variable,
+all the CPUs will agree on the operation order. Of course, the ordering
+of unordered marked accesses can also be constrained using the mechanisms
+described earlier in this document.
+
+These operations come in three categories:
+
+o Marked writes, such as WRITE_ONCE() and atomic_set(). These
+ primitives required the compiler to emit the corresponding store
+ instructions in the expected execution order, thus suppressing
+ a number of destructive optimizations. However, they provide no
+ hardware ordering guarantees, and in fact many CPUs will happily
+ reorder marked writes with each other or with other unordered
+ operations, unless these operations are to the same variable.
+
+o Marked reads, such as READ_ONCE() and atomic_read(). These
+ primitives required the compiler to emit the corresponding load
+ instructions in the expected execution order, thus suppressing
+ a number of destructive optimizations. However, they provide no
+ hardware ordering guarantees, and in fact many CPUs will happily
+ reorder marked reads with each other or with other unordered
+ operations, unless these operations are to the same variable.
+
+o Unordered RMW atomic operations. These are non-value-returning
+ RMW atomic operations whose names do not end in _acquire or
+ _release, and also value-returning RMW operations whose names
+ end in _relaxed. Examples include atomic_add(), atomic_or(),
+ and atomic64_fetch_xor_relaxed(). These operations do carry
+ out the specified RMW operation atomically, for example, five
+ concurrent atomic_inc() operations applied to a given variable
+ will reliably increase the value of that variable by five.
+ However, many CPUs will happily reorder these operations with
+ each other or with other unordered operations.
+
+ This category of operations can be efficiently ordered using
+ smp_mb__before_atomic() and smp_mb__after_atomic(), as was
+ discussed in the "RMW Ordering Augmentation Barriers" section.
+
+In short, these operations can be freely reordered unless they are all
+operating on a single variable or unless they are constrained by one of
+the operations called out earlier in this document.
+
+
+Unmarked C-Language Accesses
+----------------------------
+
+Unmarked C-language accesses are normal variable accesses to to normal
+variables, that is, to variables that are not "volatile" and are not
+C11 atomic variables. These operations provide no ordering guarantees,
+and further do not guarantee "atomic" access. For example, the compiler
+might (and sometimes does) split a plain C-language store into multiple
+smaller stores. A load from that same variable running on some other
+CPU while such a store is executing might see a value that is a mashup
+of the old value and the new value.
+
+Unmarked C-language accesses are unordered, and are also subject to
+any number of compiler optimizations, many of which can break your
+concurrent code. It is possible to used unmarked C-language accesses for
+shared variables that are subject to concurrent access, but great care
+is required on an ongoing basis. The compiler-constraining barrier()
+primitive can be helpful, as can the various ordering primitives discussed
+in this document. It nevertheless bears repeating that use of unmarked
+C-language accesses requires careful attention to not just your code,
+but to all the compilers that might be used to build it. Such compilers
+might replace a series of loads with a single load, and might replace
+a series of stores with a single store. Some compilers will even split
+a single store into multiple smaller stores.
+
+But there are some ways of using unmarked C-language accesses for shared
+variables without such worries:
+
+o
+ Guard all accesses to a given variable by a particular lock,
+ so that there are never concurrent conflicting accesses to
+ that variable. (There are "conflicting accesses" when
+ (1) at least one of the concurrent accesses to a variable is an
+ unmarked C-language access and (2) when at least one of those
+ accesses is a write, whether marked or not.)
+
+o As above, but using other synchronization primitives such
+ as reader-writer locks or sequence locks.
+
+o Use locking or other means to ensure that all concurrent accesses
+ to a given variable are reads.
+
+o Restrict use of a given variable to statistics or heuristics
+ where the occasional bogus value can be tolerated.
+
+o Declare the accessed variables as C11 atomics.
+ https://lwn.net/Articles/691128/
+
+o Declare the accessed variables as "volatile".
+
+If you need to live more dangerously, please do take the time to
+understand the compilers. One place to start is these two LWN
+articles:
+
+Who's afraid of a big bad optimizing compiler?
+ https://lwn.net/Articles/793253
+Calibrating your fear of big bad optimizing compilers
+ https://lwn.net/Articles/799218
+
+Used properly, unmarked C-language accesses can reduce overhead on
+fastpaths. However, the price is great care and continual attention
+to your compiler as new versions come out and as new optimizations
+are enabled.
--
2.9.5
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 3/8] tools/memory-model: Document categories of ordering primitives
2020-11-05 22:00 ` [PATCH memory-model 3/8] tools/memory-model: Document categories of ordering primitives paulmck
@ 2020-11-06 16:56 ` Alan Stern
2020-11-06 19:11 ` Paul E. McKenney
0 siblings, 1 reply; 29+ messages in thread
From: Alan Stern @ 2020-11-06 16:56 UTC (permalink / raw)
To: paulmck
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
On Thu, Nov 05, 2020 at 02:00:12PM -0800, paulmck@kernel.org wrote:
> From: "Paul E. McKenney" <paulmck@kernel.org>
>
> The Linux kernel has a number of categories of ordering primitives, which
> are recorded in the LKMM implementation and hinted at by cheatsheet.txt.
> But there is no overview of these categories, and such an overview
> is needed in order to understand multithreaded LKMM litmus tests.
> This commit therefore adds an ordering.txt as well as extracting a
> control-dependencies.txt from memory-barriers.txt. It also updates the
> README file.
>
> [ paulmck: Apply Akira Yokosawa file-placement feedback. ]
> [ paulmck: Apply Alan Stern feedback. ]
> [ paulmck: Apply self-review feedback. ]
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> ---
> diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
> index 2d9539f..a50ea81 100644
> --- a/tools/memory-model/Documentation/README
> +++ b/tools/memory-model/Documentation/README
> @@ -41,13 +50,21 @@ README
> cheatsheet.txt
> Quick-reference guide to the Linux-kernel memory model.
>
> +control-dependencies.txt
> + Guide to preventing compiler optimizations from destroying
> + your control dependencies.
> +
> explanation.txt
> - Detailed description of the memory model.
> + Detailed description of the memory model in detail.
A redundantly redundant change.
Alan
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 3/8] tools/memory-model: Document categories of ordering primitives
2020-11-06 16:56 ` Alan Stern
@ 2020-11-06 19:11 ` Paul E. McKenney
0 siblings, 0 replies; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-06 19:11 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
On Fri, Nov 06, 2020 at 11:56:54AM -0500, Alan Stern wrote:
> On Thu, Nov 05, 2020 at 02:00:12PM -0800, paulmck@kernel.org wrote:
> > From: "Paul E. McKenney" <paulmck@kernel.org>
> >
> > The Linux kernel has a number of categories of ordering primitives, which
> > are recorded in the LKMM implementation and hinted at by cheatsheet.txt.
> > But there is no overview of these categories, and such an overview
> > is needed in order to understand multithreaded LKMM litmus tests.
> > This commit therefore adds an ordering.txt as well as extracting a
> > control-dependencies.txt from memory-barriers.txt. It also updates the
> > README file.
> >
> > [ paulmck: Apply Akira Yokosawa file-placement feedback. ]
> > [ paulmck: Apply Alan Stern feedback. ]
> > [ paulmck: Apply self-review feedback. ]
> > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > ---
> > diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
> > index 2d9539f..a50ea81 100644
> > --- a/tools/memory-model/Documentation/README
> > +++ b/tools/memory-model/Documentation/README
>
> > @@ -41,13 +50,21 @@ README
> > cheatsheet.txt
> > Quick-reference guide to the Linux-kernel memory model.
> >
> > +control-dependencies.txt
> > + Guide to preventing compiler optimizations from destroying
> > + your control dependencies.
> > +
> > explanation.txt
> > - Detailed description of the memory model.
> > + Detailed description of the memory model in detail.
>
> A redundantly redundant change.
I will revert the reversion of the removal of the added detail "in
detail". ;-)
Good catch, thank you!
Thanx, Paul
^ permalink raw reply [flat|nested] 29+ messages in thread
* [PATCH memory-model 4/8] docs/memory-barriers.txt: Fix a typo in CPU MEMORY BARRIERS section
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
` (2 preceding siblings ...)
2020-11-05 22:00 ` [PATCH memory-model 3/8] tools/memory-model: Document categories of ordering primitives paulmck
@ 2020-11-05 22:00 ` paulmck
2020-11-05 22:00 ` [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms paulmck
` (3 subsequent siblings)
7 siblings, 0 replies; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Fox Chen, Paul E . McKenney
From: Fox Chen <foxhlchen@gmail.com>
Commit 39323c6 ("smp_mb__{before,after}_atomic(): update Documentation")
has a typo in CPU MEORY BARRIERS section:
"RMW functions that do not imply are memory barrier are ..." should be
"RMW functions that do not imply a memory barrier are ...".
This patch fixes this typo.
Signed-off-by: Fox Chen <foxhlchen@gmail.com>
Acked-by: Will Deacon <will@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
Documentation/memory-barriers.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 17c8e0c..7367ada 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -1870,7 +1870,7 @@ There are some more advanced barrier functions:
These are for use with atomic RMW functions that do not imply memory
barriers, but where the code needs a memory barrier. Examples for atomic
- RMW functions that do not imply are memory barrier are e.g. add,
+ RMW functions that do not imply a memory barrier are e.g. add,
subtract, (failed) conditional operations, _relaxed functions,
but not atomic_read or atomic_set. A common example where a memory
barrier may be required is when atomic ops are used for reference
--
2.9.5
^ permalink raw reply related [flat|nested] 29+ messages in thread* [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
` (3 preceding siblings ...)
2020-11-05 22:00 ` [PATCH memory-model 4/8] docs/memory-barriers.txt: Fix a typo in CPU MEMORY BARRIERS section paulmck
@ 2020-11-05 22:00 ` paulmck
2020-11-06 1:47 ` Boqun Feng
2020-11-06 16:59 ` Alan Stern
2020-11-05 22:00 ` [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests paulmck
` (2 subsequent siblings)
7 siblings, 2 replies; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E. McKenney
From: "Paul E. McKenney" <paulmck@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
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
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-05 22:00 ` [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms paulmck
@ 2020-11-06 1:47 ` Boqun Feng
2020-11-06 18:01 ` Paul E. McKenney
2020-11-06 16:59 ` Alan Stern
1 sibling, 1 reply; 29+ messages in thread
From: Boqun Feng @ 2020-11-06 1:47 UTC (permalink / raw)
To: paulmck
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, npiggin, dhowells, j.alglave,
luc.maranget, akiyks
On Thu, Nov 05, 2020 at 02:00:14PM -0800, paulmck@kernel.org wrote:
> From: "Paul E. McKenney" <paulmck@kernel.org>
>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> ---
> 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".
> +
[...]
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 1:47 ` Boqun Feng
@ 2020-11-06 18:01 ` Paul E. McKenney
2020-11-07 3:07 ` Boqun Feng
0 siblings, 1 reply; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-06 18:01 UTC (permalink / raw)
To: Boqun Feng
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, npiggin, dhowells, j.alglave,
luc.maranget, akiyks
On Fri, Nov 06, 2020 at 09:47:22AM +0800, Boqun Feng wrote:
> On Thu, Nov 05, 2020 at 02:00:14PM -0800, paulmck@kernel.org wrote:
> > From: "Paul E. McKenney" <paulmck@kernel.org>
> >
> > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > ---
> > 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 <paulmck@kernel.org>
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 <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
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)".
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 18:01 ` Paul E. McKenney
@ 2020-11-07 3:07 ` Boqun Feng
0 siblings, 0 replies; 29+ messages in thread
From: Boqun Feng @ 2020-11-07 3:07 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, npiggin, dhowells, j.alglave,
luc.maranget, akiyks
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, paulmck@kernel.org wrote:
> > > From: "Paul E. McKenney" <paulmck@kernel.org>
> > >
> > > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > > ---
> > > 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 <paulmck@kernel.org>
> 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 <boqun.feng@gmail.com>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
>
> 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)".
>
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-05 22:00 ` [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms paulmck
2020-11-06 1:47 ` Boqun Feng
@ 2020-11-06 16:59 ` Alan Stern
2020-11-06 18:04 ` Paul E. McKenney
1 sibling, 1 reply; 29+ messages in thread
From: Alan Stern @ 2020-11-06 16:59 UTC (permalink / raw)
To: paulmck
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
On Thu, Nov 05, 2020 at 02:00:14PM -0800, paulmck@kernel.org wrote:
> From: "Paul E. McKenney" <paulmck@kernel.org>
>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> ---
> 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
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 16:59 ` Alan Stern
@ 2020-11-06 18:04 ` Paul E. McKenney
2020-11-06 19:23 ` Alan Stern
0 siblings, 1 reply; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-06 18:04 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> On Thu, Nov 05, 2020 at 02:00:14PM -0800, paulmck@kernel.org wrote:
> > From: "Paul E. McKenney" <paulmck@kernel.org>
> >
> > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > ---
> > 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 <paulmck@kernel.org>
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 <paulmck@kernel.org>
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".
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 18:04 ` Paul E. McKenney
@ 2020-11-06 19:23 ` Alan Stern
2020-11-06 19:59 ` Paul E. McKenney
0 siblings, 1 reply; 29+ messages in thread
From: Alan Stern @ 2020-11-06 19:23 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
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 <paulmck@kernel.org>
> 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 <paulmck@kernel.org>
>
> 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".
>
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 19:23 ` Alan Stern
@ 2020-11-06 19:59 ` Paul E. McKenney
2020-11-06 20:40 ` Alan Stern
0 siblings, 1 reply; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-06 19:59 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
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 <paulmck@kernel.org>
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 <paulmck@kernel.org>
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
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 19:59 ` Paul E. McKenney
@ 2020-11-06 20:40 ` Alan Stern
2020-11-06 21:04 ` Paul E. McKenney
0 siblings, 1 reply; 29+ messages in thread
From: Alan Stern @ 2020-11-06 20:40 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
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 <paulmck@kernel.org>
> 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 <paulmck@kernel.org>
>
> 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
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 20:40 ` Alan Stern
@ 2020-11-06 21:04 ` Paul E. McKenney
2020-11-07 2:32 ` Alan Stern
0 siblings, 1 reply; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-06 21:04 UTC (permalink / raw)
To: Alan Stern
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
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 <paulmck@kernel.org>
> > 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 <paulmck@kernel.org>
> >
> > 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
^ permalink raw reply [flat|nested] 29+ messages in thread
* Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms
2020-11-06 21:04 ` Paul E. McKenney
@ 2020-11-07 2:32 ` Alan Stern
0 siblings, 0 replies; 29+ messages in thread
From: Alan Stern @ 2020-11-07 2:32 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, parri.andrea, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
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
^ permalink raw reply [flat|nested] 29+ messages in thread
* [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
` (4 preceding siblings ...)
2020-11-05 22:00 ` [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms paulmck
@ 2020-11-05 22:00 ` paulmck
2020-11-05 22:41 ` Akira Yokosawa
2020-11-05 22:00 ` [PATCH memory-model 7/8] tools/memory-model: Use "buf" and "flag" for message-passing tests paulmck
2020-11-05 22:00 ` [PATCH memory-model 8/8] tools/memory-model: Label MP tests' producers and consumers paulmck
7 siblings, 1 reply; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E. McKenney
From: "Paul E. McKenney" <paulmck@kernel.org>
This commit adds type information for global variables in the litmus
tests in order to allow easier use with klitmus7.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
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
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests
2020-11-05 22:00 ` [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests paulmck
@ 2020-11-05 22:41 ` Akira Yokosawa
2020-11-05 22:56 ` Paul E. McKenney
0 siblings, 1 reply; 29+ messages in thread
From: Akira Yokosawa @ 2020-11-05 22:41 UTC (permalink / raw)
To: paulmck, linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, Akira Yokosawa
Hi Paul,
On 2020/11/06 7:00, paulmck@kernel.org wrote:
> From: "Paul E. McKenney" <paulmck@kernel.org>
>
> 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 <paulmck@kernel.org>
> ---
> 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)
> {
>
^ permalink raw reply [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests
2020-11-05 22:41 ` Akira Yokosawa
@ 2020-11-05 22:56 ` Paul E. McKenney
2020-11-25 11:34 ` Akira Yokosawa
0 siblings, 1 reply; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-05 22:56 UTC (permalink / raw)
To: Akira Yokosawa
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget
On Fri, Nov 06, 2020 at 07:41:48AM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> On 2020/11/06 7:00, paulmck@kernel.org wrote:
> > From: "Paul E. McKenney" <paulmck@kernel.org>
> >
> > 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 <paulmck@kernel.org>
> > ---
> > 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)
> > {
> >
^ permalink raw reply [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests
2020-11-05 22:56 ` Paul E. McKenney
@ 2020-11-25 11:34 ` Akira Yokosawa
2020-11-27 15:46 ` Paul E. McKenney
0 siblings, 1 reply; 29+ messages in thread
From: Akira Yokosawa @ 2020-11-25 11:34 UTC (permalink / raw)
To: paulmck
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, Akira Yokosawa
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, paulmck@kernel.org wrote:
>>> From: "Paul E. McKenney" <paulmck@kernel.org>
>>>
>>> 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 <paulmck@kernel.org>
>>> ---
>>> 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)
>>> {
>>>
^ permalink raw reply [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests
2020-11-25 11:34 ` Akira Yokosawa
@ 2020-11-27 15:46 ` Paul E. McKenney
2020-11-28 5:56 ` Akira Yokosawa
0 siblings, 1 reply; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-27 15:46 UTC (permalink / raw)
To: Akira Yokosawa
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget
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, paulmck@kernel.org wrote:
> >>> From: "Paul E. McKenney" <paulmck@kernel.org>
> >>>
> >>> 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 <paulmck@kernel.org>
> >>> ---
> >>> 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)
> >>> {
> >>>
^ permalink raw reply [flat|nested] 29+ messages in thread* Re: [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests
2020-11-27 15:46 ` Paul E. McKenney
@ 2020-11-28 5:56 ` Akira Yokosawa
2020-11-28 6:00 ` [PATCH 1/2] tools/memory-model: Remove redundant initialization in " Akira Yokosawa
2020-11-28 6:01 ` [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table Akira Yokosawa
0 siblings, 2 replies; 29+ messages in thread
From: Akira Yokosawa @ 2020-11-28 5:56 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, Akira Yokosawa
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
>>
^ permalink raw reply [flat|nested] 29+ messages in thread* [PATCH 1/2] tools/memory-model: Remove redundant initialization in litmus tests
2020-11-28 5:56 ` Akira Yokosawa
@ 2020-11-28 6:00 ` Akira Yokosawa
2020-11-28 6:01 ` [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table Akira Yokosawa
1 sibling, 0 replies; 29+ messages in thread
From: Akira Yokosawa @ 2020-11-28 6:00 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, Akira Yokosawa
From 3a871845825d96a23d64be05b6cf6d4af2bae167 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 28 Nov 2020 08:43:45 +0900
Subject: [PATCH 1/2] tools/memory-model: Remove redundant initialization in litmus tests
This is a revert of commit 1947bfcf81a9 ("tools/memory-model: Add types
to litmus tests") with conflict resolutions.
klitmus7 [1] is aware of default types of "int" and "int*".
It accepts litmus tests for herd7 without extra type info unless
non-"int" variables are referenced by an "exists", "locations",
or "filter" directive.
[1]: Tested with klitmus7 versions 7.49 or later.
Suggested-by: Paul E. McKenney <paulmck@kernel.org>
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
.../memory-model/litmus-tests/CoRR+poonceonce+Once.litmus | 4 +---
.../memory-model/litmus-tests/CoRW+poonceonce+Once.litmus | 4 +---
.../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 +----
.../litmus-tests/IRIW+poonceonces+OnceOnce.litmus | 5 +----
.../ISA2+pooncelock+pooncelock+pombonce.litmus | 7 +------
tools/memory-model/litmus-tests/ISA2+poonceonces.litmus | 6 +-----
...SA2+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 +----
.../MP+fencewmbonceonce+fencermbonceonce.litmus | 5 +----
.../litmus-tests/MP+onceassign+derefonce.litmus | 4 +---
.../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 5 +----
.../litmus-tests/MP+polockonce+poacquiresilsil.litmus | 5 +----
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 +----
.../litmus-tests/SB+rfionceonce-poonceonces.litmus | 5 +----
.../memory-model/litmus-tests/WRC+poonceonces+Once.litmus | 5 +----
.../WRC+pooncerelease+fencermbonceonce+Once.litmus | 5 +----
.../Z6.0+pooncelock+poonceLock+pombonce.litmus | 7 +------
.../Z6.0+pooncelock+pooncelock+pombonce.litmus | 7 +------
...0+pooncerelease+poacquirerelease+fencembonceonce.litmus | 6 +-----
32 files changed, 32 insertions(+), 134 deletions(-)
diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
index 772544f03fb5..967f9f2a6226 100644
--- a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
@@ -7,9 +7,7 @@ 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 5faae98f7ffb..4635739f3974 100644
--- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
@@ -7,9 +7,7 @@ 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 77c9cc9f8dc6..bb068c92d8da 100644
--- a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
@@ -7,9 +7,7 @@ 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 85ef746f511a..0d9f0a958799 100644
--- a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
+++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
@@ -7,9 +7,7 @@ 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 87aa900125ab..e729d2776e89 100644
--- a/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
@@ -10,10 +10,7 @@ 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 f84022dca555..4b54dd6a6cd9 100644
--- a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
@@ -10,10 +10,7 @@ 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 398f624daa77..094d58df7789 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -7,12 +7,7 @@ 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 212a432ba16b..b321aa6f4ea5 100644
--- a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
@@ -9,11 +9,7 @@ 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 7afd85672ccd..025b0462ec9b 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
@@ -11,11 +11,7 @@ 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 c8a93c7ee556..4727f5aaf03b 100644
--- a/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
+++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
@@ -11,10 +11,7 @@ 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 2fa029568fa1..07b9904b0e49 100644
--- a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
+++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus
@@ -8,10 +8,7 @@ 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 2107306e8625..74c49cb3c37b 100644
--- a/tools/memory-model/litmus-tests/LB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus
@@ -7,10 +7,7 @@ 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 c5c168d92973..f8ca1229857a 100644
--- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
@@ -8,10 +8,7 @@ C MP+fencewmbonceonce+fencermbonceonce
* is usually better to use smp_store_release() and smp_load_acquire().
*)
-{
- int buf;
- int flag;
-}
+{}
P0(int *buf, int *flag) // Producer
{
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index 20ff62649f1e..d84160b9c1ae 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -10,9 +10,7 @@ C MP+onceassign+derefonce
*)
{
- int *p=y;
- int x;
- int y=0;
+p=y;
}
P0(int *x, int **p) // Producer
diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
index 153917ad5dc9..ba91cc63e148 100644
--- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
+++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
@@ -10,10 +10,7 @@ C MP+polockmbonce+poacquiresilsil
* executed before the lock was acquired (loosely speaking).
*)
-{
- spinlock_t lo;
- int x;
-}
+{}
P0(spinlock_t *lo, int *x) // Producer
{
diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
index aad64397bb8c..a5ea3ed8f52e 100644
--- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
+++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
@@ -10,10 +10,7 @@ C MP+polockonce+poacquiresilsil
* speaking).
*)
-{
- spinlock_t lo;
- int x;
-}
+{}
P0(spinlock_t *lo, int *x) // Producer
{
diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
index 21cbca6f3be4..e6af05f70069 100644
--- a/tools/memory-model/litmus-tests/MP+polocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
@@ -11,11 +11,7 @@ C MP+polocks
* to see all prior accesses by those other CPUs.
*)
-{
- spinlock_t mylock;
- int buf;
- int flag;
-}
+{}
P0(int *buf, int *flag, spinlock_t *mylock) // Producer
{
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 9f9769d647c7..ba9c99c6cf65 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -7,10 +7,7 @@ C MP+poonceonces
* no ordering at all?
*)
-{
- int buf;
- int flag;
-}
+{}
P0(int *buf, int *flag) // Producer
{
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index cbe28e733443..f174bfe61702 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -8,10 +8,7 @@ C MP+pooncerelease+poacquireonce
* pattern.
*)
-{
- int buf;
- int flag;
-}
+{}
P0(int *buf, int *flag) // Producer
{
diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
index 012041bd4feb..b9599141160e 100644
--- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
@@ -11,11 +11,7 @@ C MP+porevlocks
* see all prior accesses by those other CPUs.
*)
-{
- spinlock_t mylock;
- int buf;
- int flag;
-}
+{}
P0(int *buf, int *flag, spinlock_t *mylock) // Consumer
{
diff --git a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
index af9463b39b4a..222a0b850b4a 100644
--- a/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
@@ -9,10 +9,7 @@ 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 bcd5574e304a..5386f128a131 100644
--- a/tools/memory-model/litmus-tests/R+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus
@@ -8,10 +8,7 @@ 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 c36341d1aed6..18479823cd6c 100644
--- a/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
@@ -7,10 +7,7 @@ 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 7775c23143a0..8c9c2f81a580 100644
--- a/tools/memory-model/litmus-tests/S+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus
@@ -9,10 +9,7 @@ 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 833cdfeb7c09..ed5fff18d223 100644
--- a/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
@@ -9,10 +9,7 @@ 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 c92211ecbfdf..10d550730b25 100644
--- a/tools/memory-model/litmus-tests/SB+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus
@@ -8,10 +8,7 @@ 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 84344b455eb7..04a16603660b 100644
--- a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
@@ -6,10 +6,7 @@ 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 431494708611..6a2bc12a1af1 100644
--- a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
@@ -8,10 +8,7 @@ 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 554999c64db5..e9947250d7de 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
@@ -10,10 +10,7 @@ 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 265a95ffef13..415248fb6699 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,12 +9,7 @@ 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 0c9aea8e80df..10a2aa04cd07 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,12 +8,7 @@ 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 661f9aaa5791..88e70b87a683 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,11 +14,7 @@ C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
* involving locking.)
*)
-{
- int x;
- int y;
- int z;
-}
+{}
P0(int *x, int *y)
{
--
2.17.1
^ permalink raw reply related [flat|nested] 29+ messages in thread* [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table
2020-11-28 5:56 ` Akira Yokosawa
2020-11-28 6:00 ` [PATCH 1/2] tools/memory-model: Remove redundant initialization in " Akira Yokosawa
@ 2020-11-28 6:01 ` Akira Yokosawa
2020-11-29 3:33 ` Paul E. McKenney
1 sibling, 1 reply; 29+ messages in thread
From: Akira Yokosawa @ 2020-11-28 6:01 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, Akira Yokosawa
From 4f577823fa60e14ae58caa2d3c0b2ced64e6eb43 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 28 Nov 2020 14:32:15 +0900
Subject: [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table
klitmus7 of herdtools7 7.48 or earlier depends on ACCESS_ONCE(),
which was removed in Linux v4.15.
Fix the obvious typo in the table.
Fixes: d075a78a5ab1 ("tools/memory-model/README: Expand dependency of klitmus7")
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
tools/memory-model/README | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/README b/tools/memory-model/README
index 39d08d1f0443..9a84c45504ab 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -51,7 +51,7 @@ klitmus7 Compatibility Table
============ ==========
target Linux herdtools7
------------ ----------
- -- 4.18 7.48 --
+ -- 4.14 7.48 --
4.15 -- 4.19 7.49 --
4.20 -- 5.5 7.54 --
5.6 -- 7.56 --
--
2.17.1
^ permalink raw reply related [flat|nested] 29+ messages in thread* Re: [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table
2020-11-28 6:01 ` [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table Akira Yokosawa
@ 2020-11-29 3:33 ` Paul E. McKenney
0 siblings, 0 replies; 29+ messages in thread
From: Paul E. McKenney @ 2020-11-29 3:33 UTC (permalink / raw)
To: Akira Yokosawa
Cc: linux-kernel, linux-arch, kernel-team, mingo, stern,
parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget
On Sat, Nov 28, 2020 at 03:01:49PM +0900, Akira Yokosawa wrote:
> >From 4f577823fa60e14ae58caa2d3c0b2ced64e6eb43 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sat, 28 Nov 2020 14:32:15 +0900
> Subject: [PATCH 2/2] tools/memory-model: Fix typo in klitmus7 compatibility table
>
> klitmus7 of herdtools7 7.48 or earlier depends on ACCESS_ONCE(),
> which was removed in Linux v4.15.
> Fix the obvious typo in the table.
>
> Fixes: d075a78a5ab1 ("tools/memory-model/README: Expand dependency of klitmus7")
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Both queued for review and further testing, thank you!
Thanx, Paul
> ---
> tools/memory-model/README | 2 +-
> 1 file changed, 1 insertion(+), 1 deletion(-)
>
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index 39d08d1f0443..9a84c45504ab 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -51,7 +51,7 @@ klitmus7 Compatibility Table
> ============ ==========
> target Linux herdtools7
> ------------ ----------
> - -- 4.18 7.48 --
> + -- 4.14 7.48 --
> 4.15 -- 4.19 7.49 --
> 4.20 -- 5.5 7.54 --
> 5.6 -- 7.56 --
> --
> 2.17.1
>
>
^ permalink raw reply [flat|nested] 29+ messages in thread
* [PATCH memory-model 7/8] tools/memory-model: Use "buf" and "flag" for message-passing tests
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
` (5 preceding siblings ...)
2020-11-05 22:00 ` [PATCH memory-model 6/8] tools/memory-model: Add types to litmus tests paulmck
@ 2020-11-05 22:00 ` paulmck
2020-11-05 22:00 ` [PATCH memory-model 8/8] tools/memory-model: Label MP tests' producers and consumers paulmck
7 siblings, 0 replies; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E. McKenney
From: "Paul E. McKenney" <paulmck@kernel.org>
The use of "x" and "y" for message-passing tests is fine for people
familiar with memory models and litmus-test nomenclature, but is a bit
obtuse for others. This commit therefore substitutes "buf" for "x" and
"flag" for "y" for the MP tests. There are a few special-case MP tests
that use locks and these are unchanged. There is another MP test that
uses pointers, and this is changed to name the pointer "p".
Reported-by: Johannes Weiner <hannes@cmpxchg.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
.../MP+fencewmbonceonce+fencermbonceonce.litmus | 16 ++++++++--------
.../litmus-tests/MP+onceassign+derefonce.litmus | 12 ++++++------
tools/memory-model/litmus-tests/MP+polocks.litmus | 16 ++++++++--------
tools/memory-model/litmus-tests/MP+poonceonces.litmus | 16 ++++++++--------
.../litmus-tests/MP+pooncerelease+poacquireonce.litmus | 16 ++++++++--------
tools/memory-model/litmus-tests/MP+porevlocks.litmus | 16 ++++++++--------
6 files changed, 46 insertions(+), 46 deletions(-)
diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
index e04b71b..f15e501 100644
--- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
@@ -9,25 +9,25 @@ C MP+fencewmbonceonce+fencermbonceonce
*)
{
- int x;
- int y;
+ int buf;
+ int flag;
}
-P0(int *x, int *y)
+P0(int *buf, int *flag)
{
- WRITE_ONCE(*x, 1);
+ WRITE_ONCE(*buf, 1);
smp_wmb();
- WRITE_ONCE(*y, 1);
+ WRITE_ONCE(*flag, 1);
}
-P1(int *x, int *y)
+P1(int *buf, int *flag)
{
int r0;
int r1;
- r0 = READ_ONCE(*y);
+ r0 = READ_ONCE(*flag);
smp_rmb();
- r1 = READ_ONCE(*x);
+ r1 = READ_ONCE(*buf);
}
exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
index 18df682..ed8ee9b 100644
--- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus
@@ -10,24 +10,24 @@ C MP+onceassign+derefonce
*)
{
+ int *p=y;
int x;
- int *y=z;
- int z=0;
+ int y=0;
}
-P0(int *x, int **y)
+P0(int *x, int **p)
{
WRITE_ONCE(*x, 1);
- rcu_assign_pointer(*y, x);
+ rcu_assign_pointer(*p, x);
}
-P1(int *x, int **y)
+P1(int *x, int **p)
{
int *r0;
int r1;
rcu_read_lock();
- r0 = rcu_dereference(*y);
+ r0 = rcu_dereference(*p);
r1 = READ_ONCE(*r0);
rcu_read_unlock();
}
diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus
index 63e0f67..4b0c2ed 100644
--- a/tools/memory-model/litmus-tests/MP+polocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+polocks.litmus
@@ -13,27 +13,27 @@ C MP+polocks
{
spinlock_t mylock;
- int x;
- int y;
+ int buf;
+ int flag;
}
-P0(int *x, int *y, spinlock_t *mylock)
+P0(int *buf, int *flag, spinlock_t *mylock)
{
- WRITE_ONCE(*x, 1);
+ WRITE_ONCE(*buf, 1);
spin_lock(mylock);
- WRITE_ONCE(*y, 1);
+ WRITE_ONCE(*flag, 1);
spin_unlock(mylock);
}
-P1(int *x, int *y, spinlock_t *mylock)
+P1(int *buf, int *flag, spinlock_t *mylock)
{
int r0;
int r1;
spin_lock(mylock);
- r0 = READ_ONCE(*y);
+ r0 = READ_ONCE(*flag);
spin_unlock(mylock);
- r1 = READ_ONCE(*x);
+ r1 = READ_ONCE(*buf);
}
exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
index 68180a4..3010bba 100644
--- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus
+++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus
@@ -8,23 +8,23 @@ C MP+poonceonces
*)
{
- int x;
- int y;
+ int buf;
+ int flag;
}
-P0(int *x, int *y)
+P0(int *buf, int *flag)
{
- WRITE_ONCE(*x, 1);
- WRITE_ONCE(*y, 1);
+ WRITE_ONCE(*buf, 1);
+ WRITE_ONCE(*flag, 1);
}
-P1(int *x, int *y)
+P1(int *buf, int *flag)
{
int r0;
int r1;
- r0 = READ_ONCE(*y);
- r1 = READ_ONCE(*x);
+ r0 = READ_ONCE(*flag);
+ r1 = READ_ONCE(*buf);
}
exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
index 19f3e68..21e825d 100644
--- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus
@@ -9,23 +9,23 @@ C MP+pooncerelease+poacquireonce
*)
{
- int x;
- int y;
+ int buf;
+ int flag;
}
-P0(int *x, int *y)
+P0(int *buf, int *flag)
{
- WRITE_ONCE(*x, 1);
- smp_store_release(y, 1);
+ WRITE_ONCE(*buf, 1);
+ smp_store_release(flag, 1);
}
-P1(int *x, int *y)
+P1(int *buf, int *flag)
{
int r0;
int r1;
- r0 = smp_load_acquire(y);
- r1 = READ_ONCE(*x);
+ r0 = smp_load_acquire(flag);
+ r1 = READ_ONCE(*buf);
}
exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
index 4ac189a..9691d55 100644
--- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus
+++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus
@@ -13,27 +13,27 @@ C MP+porevlocks
{
spinlock_t mylock;
- int x;
- int y;
+ int buf;
+ int flag;
}
-P0(int *x, int *y, spinlock_t *mylock)
+P0(int *buf, int *flag, spinlock_t *mylock)
{
int r0;
int r1;
- r0 = READ_ONCE(*y);
+ r0 = READ_ONCE(*flag);
spin_lock(mylock);
- r1 = READ_ONCE(*x);
+ r1 = READ_ONCE(*buf);
spin_unlock(mylock);
}
-P1(int *x, int *y, spinlock_t *mylock)
+P1(int *buf, int *flag, spinlock_t *mylock)
{
spin_lock(mylock);
- WRITE_ONCE(*x, 1);
+ WRITE_ONCE(*buf, 1);
spin_unlock(mylock);
- WRITE_ONCE(*y, 1);
+ WRITE_ONCE(*flag, 1);
}
exists (0:r0=1 /\ 0:r1=0)
--
2.9.5
^ permalink raw reply related [flat|nested] 29+ messages in thread* [PATCH memory-model 8/8] tools/memory-model: Label MP tests' producers and consumers
2020-11-05 21:59 [PATCH memory-model 0/8] LKMM updates for v5.11 Paul E. McKenney
` (6 preceding siblings ...)
2020-11-05 22:00 ` [PATCH memory-model 7/8] tools/memory-model: Use "buf" and "flag" for message-passing tests paulmck
@ 2020-11-05 22:00 ` paulmck
7 siblings, 0 replies; 29+ messages in thread
From: paulmck @ 2020-11-05 22:00 UTC (permalink / raw)
To: linux-kernel, linux-arch, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E. McKenney
From: "Paul E. McKenney" <paulmck@kernel.org>
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 <hannes@cmpxchg.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
.../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
^ permalink raw reply related [flat|nested] 29+ messages in thread