summaryrefslogtreecommitdiff
path: root/tools/memory-model
AgeCommit message (Collapse)AuthorFilesLines
2019-04-04tools/memory-model: Add support for synchronize_srcu_expedited()Paul E. McKenney1-0/+1
Given that synchronize_rcu_expedited() is supported, this commit adds support for synchronize_srcu_expedited(). Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
2019-03-18tools/memory-model: Avoid duplicating herdtools versionsAndrea Parri3-7/+6
Currently, herdtools version information appears no fewer than three times in the LKMM source, which is difficult to maintain. This commit therefore places the required version in one place, namely the tools/memory-model/README file. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu>
2019-03-18tools/memory-model: Dynamically check SRCU lock-to-unlock matchingLuc Maranget3-1/+6
This commit checks that the return value of srcu_read_lock() is passed to the matching srcu_read_unlock(), where "matching" is determined by nesting. This check operates as follows: 1. srcu_read_lock() creates an integer token, which is stored into the generated events. 2. srcu_read_unlock() records its second (token) argument into the generated event. 3. A new herd primitive 'different-values' filters out pairs of events with identical values from the relation passed as its argument. 4. The bell file applies the above primitive to the (srcu) read-side-critical-section relation 'srcu-rscs' and flags non-empty results. BEWARE: Works only with herd version 7.51+6 and onwards. Signed-off-by: Luc Maranget <Luc.Maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> [ paulmck: Apply Andrea Parri's off-list feedback. ] Acked-by: Alan Stern <stern@rowland.harvard.edu>
2019-03-18tools/memory-model: Update Documentation/explanation.txt to include SRCU supportAlan Stern1-137/+152
The recent commit adding support for SRCU to the Linux Kernel Memory Model ended up changing the names and meanings of several relations. This patch updates the explanation.txt documentation file to reflect those changes. It also revises the statement of the RCU Guarantee to a more accurate form, and it adds a short paragraph mentioning the new support for SRCU. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: Daniel Lustig <dlustig@nvidia.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will.deacon@arm.com> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
2019-03-18tools/memory-model: Update README for addition of SRCUPaul E. McKenney1-2/+23
This commit updates the section on LKMM limitations to no longer say that SRCU is not modeled, but instead describe how LKMM's modeling of SRCU departs from the Linux-kernel implementation. TL;DR: There is no known valid use case that cares about the Linux kernel's ability to have partially overlapping SRCU read-side critical sections. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
2019-03-18tools/memory-model: Add SRCU supportAlan Stern3-4/+44
Add support for SRCU. Herd creates srcu events and linux-kernel.def associates them with three possible annotations (srcu-lock, srcu-unlock, and sync-srcu) corresponding to the API routines srcu_read_lock(), srcu_read_unlock(), and synchronize_srcu(). The linux-kernel.bell file now declares the annotations and determines matching lock/unlock pairs delimiting SRCU read-side critical sections, and it also checks for synchronize_srcu() calls inside an RCU critical section (which would generate a "sleeping in atomic context" error in real kernel code). The linux-kernel.cat file now adds SRCU-induced ordering, analogous to the existing RCU-induced ordering, to the gp and rcu-fence relations. Curiously enough, these small changes to the model's .cat code are all that is needed to describe SRCU. Portions of this patch (linux-kernel.def and the first hunk in linux-kernel.bell) were written by Luc Maranget. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> CC: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
2019-03-18tools/memory-model: Refactor some RCU relationsAlan Stern1-10/+15
In preparation for adding support for SRCU, refactor the definitions of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po? terms from the first two to the second two. An rcu-gp relation is added; it is equivalent to gp with the po and po? terms removed. This is necessary because for SRCU, we will have to use the loc relation to check that the terms at the start and end of each disjunct in the definition of rcu-fence refer to the same srcu_struct location. If these terms are hidden behind po and po?, there's no way to carry out this check. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
2019-03-18tools/memory-model: Rename some RCU relationsAlan Stern2-11/+8
In preparation for adding support for SRCU, rename "crit" to "rcu-rscs", rename "rscs" to "rcu-rscsi", and remove the restriction to only the outermost level of nesting. The name change is needed for disambiguating RCU read-side critical sections from SRCU read-side critical sections. Adding the "i" at the end of "rcu-rscsi" emphasizes that the relation is inverted; it links rcu_read_unlock() events to their corresponding preceding rcu_read_lock() events. The restriction to outermost nesting levels was never essential; it was included mostly to show that it could be done. Rather than add equivalent unnecessary code for SRCU lock nesting, it seemed better to remove the existing code. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
2019-01-21tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"Paul E. McKenney1-2/+12
The "--jobs" argument to the litmus-test scripts is similar to the "-jN" argument to "make", so this commit allows the "-jN" form as well. While in the area, it also prohibits the various forms of "-j0". Suggested-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20181203230451.28921-3-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2019-01-21tools/memory-model: Add scripts to check github litmus testsPaul E. McKenney13-93/+739
The https://github.com/paulmckrcu/litmus repository contains a large number of C-language litmus tests that include "Result:" comments predicting the verification result. This commit adds a number of scripts that run tests on these litmus tests: checkghlitmus.sh: Runs all litmus tests in the https://github.com/paulmckrcu/litmus archive that are C-language and that have "Result:" comment lines documenting expected results, comparing the actual results to those expected. Clones the repository if it has not already been cloned into the "tools/memory-model/litmus" directory. initlitmushist.sh Run all litmus tests having no more than the specified number of processes given a specified timeout, recording the results in .litmus.out files. Clones the repository if it has not already been cloned into the "tools/memory-model/litmus" directory. newlitmushist.sh For all new or updated litmus tests having no more than the specified number of processes given a specified timeout, run and record the results in .litmus.out files. checklitmushist.sh Run all litmus tests having .litmus.out files from previous initlitmushist.sh or newlitmushist.sh runs, comparing the herd output to that of the original runs. The above scripts will run litmus tests concurrently, by default with one job per available CPU. Giving any of these scripts the --help argument will cause them to print usage information. This commit also adds a number of helper scripts that are not intended to be invoked from the command line: cmplitmushist.sh: Compare the output of two different runs of the same litmus test. judgelitmus.sh: Compare the output of a litmus test to its "Result:" comment line. parseargs.sh: Parse command-line arguments. runlitmushist.sh: Run the litmus tests whose pathnames are provided one per line on standard input. While in the area, this commit also makes the existing checklitmus.sh and checkalllitmus.sh scripts use parseargs.sh in order to provide a bit of uniformity. In addition, per-litmus-test status output is directed to stdout, while end-of-test summary information is directed to stderr. Finally, the error flag standardizes on "!!!" to assist those familiar with rcutorture output. The defaults for the parseargs.sh arguments may be overridden by using environment variables: LKMM_DESTDIR for --destdir, LKMM_HERD_OPTIONS for --herdoptions, LKMM_JOBS for --jobs, LKMM_PROCS for --procs, and LKMM_TIMEOUT for --timeout. [ paulmck: History-check summary-line changes per Alan Stern feedback. ] Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20181203230451.28921-2-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2019-01-21tools/memory-model: Model smp_mb__after_unlock_lock()Andrea Parri3-2/+6
The kernel documents smp_mb__after_unlock_lock() the following way: "Place this after a lock-acquisition primitive to guarantee that an UNLOCK+LOCK pair acts as a full barrier. This guarantee applies if the UNLOCK and LOCK are executed by the same CPU or if the UNLOCK and LOCK operate on the same lock variable." Formalize in LKMM the above guarantee by defining (new) mb-links according to the law: ([M] ; po ; [UL] ; (co | po) ; [LKW] ; fencerel(After-unlock-lock) ; [M]) where the component ([UL] ; co ; [LKW]) identifies "UNLOCK+LOCK pairs on the same lock variable" and the component ([UL] ; po ; [LKW]) identifies "UNLOCK+LOCK pairs executed by the same CPU". In particular, the LKMM forbids the following two behaviors (the second litmus test below is based on: Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html c.f., Section "Tree RCU Grace Period Memory Ordering Building Blocks"): C after-unlock-lock-same-cpu (* * Result: Never *) {} P0(spinlock_t *s, spinlock_t *t, int *x, int *y) { int r0; spin_lock(s); WRITE_ONCE(*x, 1); spin_unlock(s); spin_lock(t); smp_mb__after_unlock_lock(); r0 = READ_ONCE(*y); spin_unlock(t); } P1(int *x, int *y) { int r0; WRITE_ONCE(*y, 1); smp_mb(); r0 = READ_ONCE(*x); } exists (0:r0=0 /\ 1:r0=0) C after-unlock-lock-same-lock-variable (* * Result: Never *) {} P0(spinlock_t *s, int *x, int *y) { int r0; spin_lock(s); WRITE_ONCE(*x, 1); r0 = READ_ONCE(*y); spin_unlock(s); } P1(spinlock_t *s, int *y, int *z) { int r0; spin_lock(s); smp_mb__after_unlock_lock(); WRITE_ONCE(*y, 1); r0 = READ_ONCE(*z); spin_unlock(s); } P2(int *z, int *x) { int r0; WRITE_ONCE(*z, 1); smp_mb(); r0 = READ_ONCE(*x); } exists (0:r0=0 /\ 1:r0=0 /\ 2:r0=0) Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Alan Stern <stern@rowland.harvard.edu> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: Daniel Lustig <dlustig@nvidia.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20181203230451.28921-1-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-10-02tools/memory-model: Add more LKMM limitationsPaul E. McKenney1-0/+39
This commit adds more detail about compiler optimizations and not-yet-modeled Linux-kernel APIs. Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Reviewed-by: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Alexander Shishkin <alexander.shishkin@linux.intel.com> Cc: Arnaldo Carvalho de Melo <acme@redhat.com> Cc: Jiri Olsa <jolsa@redhat.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Stephane Eranian <eranian@google.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Vince Weaver <vincent.weaver@maine.edu> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180926182920.27644-4-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-10-02tools/memory-model: Fix a README typoSeongJae Park1-1/+1
This commit fixes a duplicate-"the" typo in README. Signed-off-by: SeongJae Park <sj38.park@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Alexander Shishkin <alexander.shishkin@linux.intel.com> Cc: Arnaldo Carvalho de Melo <acme@redhat.com> Cc: Jiri Olsa <jolsa@redhat.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Stephane Eranian <eranian@google.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Vince Weaver <vincent.weaver@maine.edu> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180926182920.27644-3-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-10-02tools/memory-model: Add extra ordering for locks and remove it for ordinary ↵Alan Stern3-51/+150
release/acquire More than one kernel developer has expressed the opinion that the LKMM should enforce ordering of writes by locking. In other words, given the following code: WRITE_ONCE(x, 1); spin_unlock(&s): spin_lock(&s); WRITE_ONCE(y, 1); the stores to x and y should be propagated in order to all other CPUs, even though those other CPUs might not access the lock s. In terms of the memory model, this means expanding the cumul-fence relation. Locks should also provide read-read (and read-write) ordering in a similar way. Given: READ_ONCE(x); spin_unlock(&s); spin_lock(&s); READ_ONCE(y); // or WRITE_ONCE(y, 1); the load of x should be executed before the load of (or store to) y. The LKMM already provides this ordering, but it provides it even in the case where the two accesses are separated by a release/acquire pair of fences rather than unlock/lock. This would prevent architectures from using weakly ordered implementations of release and acquire, which seems like an unnecessary restriction. The patch therefore removes the ordering requirement from the LKMM for that case. There are several arguments both for and against this change. Let us refer to these enhanced ordering properties by saying that the LKMM would require locks to be RCtso (a bit of a misnomer, but analogous to RCpc and RCsc) and it would require ordinary acquire/release only to be RCpc. (Note: In the following, the phrase "all supported architectures" is meant not to include RISC-V. Although RISC-V is indeed supported by the kernel, the implementation is still somewhat in a state of flux and therefore statements about it would be premature.) Pros: The kernel already provides RCtso ordering for locks on all supported architectures, even though this is not stated explicitly anywhere. Therefore the LKMM should formalize it. In theory, guaranteeing RCtso ordering would reduce the need for additional barrier-like constructs meant to increase the ordering strength of locks. Will Deacon and Peter Zijlstra are strongly in favor of formalizing the RCtso requirement. Linus Torvalds and Will would like to go even further, requiring locks to have RCsc behavior (ordering preceding writes against later reads), but they recognize that this would incur a noticeable performance degradation on the POWER architecture. Linus also points out that people have made the mistake, in the past, of assuming that locking has stronger ordering properties than is currently guaranteed, and this change would reduce the likelihood of such mistakes. Not requiring ordinary acquire/release to be any stronger than RCpc may prove advantageous for future architectures, allowing them to implement smp_load_acquire() and smp_store_release() with more efficient machine instructions than would be possible if the operations had to be RCtso. Will and Linus approve this rationale, hypothetical though it is at the moment (it may end up affecting the RISC-V implementation). The same argument may or may not apply to RMW-acquire/release; see also the second Con entry below. Linus feels that locks should be easy for people to use without worrying about memory consistency issues, since they are so pervasive in the kernel, whereas acquire/release is much more of an "experts only" tool. Requiring locks to be RCtso is a step in this direction. Cons: Andrea Parri and Luc Maranget think that locks should have the same ordering properties as ordinary acquire/release (indeed, Luc points out that the names "acquire" and "release" derive from the usage of locks). Andrea points out that having different ordering properties for different forms of acquires and releases is not only unnecessary, it would also be confusing and unmaintainable. Locks are constructed from lower-level primitives, typically RMW-acquire (for locking) and ordinary release (for unlock). It is illogical to require stronger ordering properties from the high-level operations than from the low-level operations they comprise. Thus, this change would make while (cmpxchg_acquire(&s, 0, 1) != 0) cpu_relax(); an incorrect implementation of spin_lock(&s) as far as the LKMM is concerned. In theory this weakness can be ameliorated by changing the LKMM even further, requiring RMW-acquire/release also to be RCtso (which it already is on all supported architectures). As far as I know, nobody has singled out any examples of code in the kernel that actually relies on locks being RCtso. (People mumble about RCU and the scheduler, but nobody has pointed to any actual code. If there are any real cases, their number is likely quite small.) If RCtso ordering is not needed, why require it? A handful of locking constructs (qspinlocks, qrwlocks, and mcs_spinlocks) are built on top of smp_cond_load_acquire() instead of an RMW-acquire instruction. It currently provides only the ordinary acquire semantics, not the stronger ordering this patch would require of locks. In theory this could be ameliorated by requiring smp_cond_load_acquire() in combination with ordinary release also to be RCtso (which is currently true on all supported architectures). On future weakly ordered architectures, people may be able to implement locks in a non-RCtso fashion with significant performance improvement. Meeting the RCtso requirement would necessarily add run-time overhead. Overall, the technical aspects of these arguments seem relatively minor, and it appears mostly to boil down to a matter of opinion. Since the opinions of senior kernel maintainers such as Linus, Peter, and Will carry more weight than those of Luc and Andrea, this patch changes the model in accordance with the maintainers' wishes. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Reviewed-by: Will Deacon <will.deacon@arm.com> Reviewed-by: Andrea Parri <andrea.parri@amarulasolutions.com> Acked-by: Peter Zijlstra (Intel) <peterz@infradead.org> Cc: Alexander Shishkin <alexander.shishkin@linux.intel.com> Cc: Arnaldo Carvalho de Melo <acme@redhat.com> Cc: Jiri Olsa <jolsa@redhat.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Stephane Eranian <eranian@google.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Vince Weaver <vincent.weaver@maine.edu> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180926182920.27644-2-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-10-02tools/memory-model: Add litmus-test naming schemePaul E. McKenney1-2/+102
This commit documents the scheme used to generate the names for the litmus tests. [ paulmck: Apply feedback from Andrea Parri and Will Deacon. ] Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Will Deacon <will.deacon@arm.com> Cc: Alexander Shishkin <alexander.shishkin@linux.intel.com> Cc: Arnaldo Carvalho de Melo <acme@redhat.com> Cc: Jiri Olsa <jolsa@redhat.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Stephane Eranian <eranian@google.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Vince Weaver <vincent.weaver@maine.edu> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/20180926182920.27644-1-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model: Rename litmus tests to comply to norm7Andrea Parri11-30/+30
norm7 produces the 'normalized' name of a litmus test, when the test can be generated from a single cycle that passes through each process exactly once. The commit renames such tests in order to comply to the naming scheme implemented by this tool. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180716180605.16115-14-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model/Documentation: Fix typo, smb->smpYauheni Kaliuta1-1/+1
The tools/memory-model/Documentation/explanation.txt file says "For each other CPU C', smb_wmb() forces all po-earlier stores" This commit therefore replaces the "smb_wmb()" with "smp_wmb()". Signed-off-by: Yauheni Kaliuta <yauheni.kaliuta@redhat.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-13-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model: Make scripts executablePaul E. McKenney2-2/+2
This commit makes the scripts executable to avoid the need for everyone to do so manually in their archive. Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Akira Yokosawa <akiyks@gmail.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-7-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model: Remove ACCESS_ONCE() from modelMark Rutland1-1/+1
Since commit: b899a850431e2dd0 ("compiler.h: Remove ACCESS_ONCE()") ... there has been no definition of ACCESS_ONCE() in the kernel tree, and it has been necessary to use READ_ONCE() or WRITE_ONCE() instead. Correspondingly, let's remove ACCESS_ONCE() from the kernel memory model. Signed-off-by: Mark Rutland <mark.rutland@arm.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Alan Stern <stern@rowland.harvard.edu> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180716180605.16115-6-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model: Remove ACCESS_ONCE() from recipesMark Rutland1-2/+2
Since commit: b899a850431e2dd0 ("compiler.h: Remove ACCESS_ONCE()") ... there has been no definition of ACCESS_ONCE() in the kernel tree, and it has been necessary to use READ_ONCE() or WRITE_ONCE() instead. Let's update the exmaples in recipes.txt likewise for consistency, using READ_ONCE() for reads. Signed-off-by: Mark Rutland <mark.rutland@arm.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Alan Stern <stern@rowland.harvard.edu> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180716180605.16115-5-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model: Fix ISA2+pooncelock+pooncelock+pombonce namePaul E. McKenney1-1/+1
The names on the first line of the litmus tests are arbitrary, but the convention is that they be the filename without the trailing ".litmus". This commit therefore removes the stray trailing ".litmus" from ISA2+pooncelock+pooncelock+pombonce.litmus's name. Reported-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-2-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-07-17tools/memory-model: Add litmus test for full multicopy atomicityPaul E. McKenney2-0/+41
This commit adds a litmus test suggested by Alan Stern that is forbidden on fully multicopy atomic systems, but allowed on other-multicopy and on non-multicopy atomic systems. For reference, s390 is fully multicopy atomic, x86 and ARMv8 are other-multicopy atomic, and ARMv7 and powerpc are non-multicopy atomic. Suggested-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-1-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Add reference for 'Simplifying ARM concurrency'Andrea Parri1-0/+6
The paper discusses the revised ARMv8 memory model; such revision had an important impact on the design of the LKMM. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-19-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Update ASPLOS informationAndrea Parri4-11/+12
ASPLOS 2018 was held in March: make sure this is reflected in header comments and references. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-18-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Fix coding style in 'lock.cat'Andrea Parri1-14/+14
This commit uses tabs for indentation and adds spaces around binary operator. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-16-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Remove out-of-date comments and code from lock.catAlan Stern1-9/+6
lock.cat contains old comments and code referring to the possibility of LKR events that are not part of an RMW pair. This is a holdover from when I though we might end up using LKR events to implement spin_is_locked(). Reword the comments to remove this assumption and replace domain(lk-rmw) in the code with LKR. Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com> [ paulmck: Pulled as lock-nest into previous line as discussed. ] Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-15-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Improve mixed-access checking in lock.catAlan Stern1-11/+11
The code in lock.cat which checks for normal read/write accesses to spinlock variables doesn't take into account the newly added RL and RU events. Add them into the test, and move the resulting code up near the start of the file, since a violation would indicate a pretty severe conceptual error in a litmus test. Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-14-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Improve comments in lock.catAlan Stern1-15/+36
This patch improves the comments in tools/memory-model/lock.cat. In addition to making the text more uniform and removing redundant comments, it adds a description of all the possible locking events that herd can generate. Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-13-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Remove duplicated code from lock.catAlan Stern1-22/+6
This patch simplifies the implementation of spin_is_locked in the LKMM. It capitalizes on the fact that a failed spin_trylock() and a spin_is_locked() which returns True have exactly the same semantics (those of READ_ONCE) and ordering properties (none). Therefore the two kinds of events can be combined and handled by the same code, instead of treated separately as they are currently. Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-12-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Flag "cumulativity" and "propagation" testsPaul E. McKenney3-5/+10
This commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being forbidden by smp_store_release() A-cumulativity and IRIW+mbonceonces+OnceOnce.litmus as being forbidden by the LKMM propagation rule. Suggested-by: Andrea Parri <andrea.parri@amarulasolutions.com> Reported-by: Paolo Bonzini <pbonzini@redhat.com> [ paulmck: Updated wording as suggested by Alan Stern. ] Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-11-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Add model support for spin_is_locked()Luc Maranget5-4/+129
This commit first adds a trivial macro for spin_is_locked() to linux-kernel.def. It also adds cat code for enumerating all possible matches of lock write events (set LKW) with islocked events returning true (set RL, for Read from Lock), and unlock write events (set UL) with islocked events returning false (set RU, for Read from Unlock). Note that this intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally returns zero. It also adds a pair of litmus tests demonstrating the minimal ordering provided by spin_is_locked() in conjunction with spin_lock(). Will Deacon noted that this minimal ordering happens on ARMv8: https://lkml.kernel.org/r/20180226162426.GB17158@arm.com Notice that herd7 installations strictly older than version 7.49 do not handle the new constructs. Signed-off-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Reviewed-by: Alan Stern <stern@rowland.harvard.edu> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Andrea Parri <parri.andrea@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <Luc.Maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Link: http://lkml.kernel.org/r/1526340837-12222-10-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Add scripts to test memory modelPaul E. McKenney3-0/+160
This commit adds a pair of scripts that run the memory model on litmus tests, checking that the verification result of each litmus test matches the result flagged in the litmus test itself. These scripts permit easier checking of changes to the memory model against preconceived notions. To run the scripts, go to the tools/memory-model directory and type "scripts/checkalllitmus.sh". If all is well, the last line printed will be "All litmus tests verified as was expected." Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-9-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Fix coding style in 'linux-kernel.def'Andrea Parri1-14/+14
This commit fixes white spaces around semicolons. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-8-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Model 'smp_store_mb()'Andrea Parri1-0/+1
This commit models 'smp_store_mb(x, val);' to be semantically equivalent to 'WRITE_ONCE(x, val); smp_mb();'. Suggested-by: Paolo Bonzini <pbonzini@redhat.com> Suggested-by: Peter Zijlstra <peterz@infradead.org> Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-7-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-order: Update the cheat-sheet to show that ↵Paul E. McKenney1-1/+1
smp_mb__after_atomic() orders later RMW operations The current cheat sheet does not claim that smp_mb__after_atomic() orders later RMW atomic operations, which it must, at least against earlier RMW atomic operations and whatever precedes them. This commit therefore adds the needed "Y". Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-6-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-order: Improve key for SELF and SVPaul E. McKenney1-1/+2
The key for "SELF" was missing completely and the key for "SV" was a bit obtuse. This commit therefore adds a key for "SELF" and improves the one for "SV". Reported-by: Paolo Bonzini <pbonzini@redhat.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-5-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Fix cheat sheet typoPaolo Bonzini1-1/+1
"RWM" should be "RMW". Signed-off-by: Paolo Bonzini <pbonzini@redhat.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-4-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Update required version of herdtools7Akira Yokosawa1-1/+1
Code generated by klitmus7 version 7.48 doesn't compile with kernel header of 4.15 and later due to the absence of ACCESS_ONCE(). As the issue has been resolved in herdtools7 7.49, bump the required version number in README. Signed-off-by: Akira Yokosawa <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Alan Stern <stern@rowland.harvard.edu> Cc: Andrea Parri <parri.andrea@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Link: http://lkml.kernel.org/r/1526340837-12222-3-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Redefine rb in terms of rcu-fenceAlan Stern2-72/+129
This patch reorganizes the definition of rb in the Linux Kernel Memory Consistency Model. The relation is now expressed in terms of rcu-fence, which consists of a sequence of gp and rscs links separated by rcu-link links, in which the number of occurrences of gp is >= the number of occurrences of rscs. Arguments similar to those published in http://diy.inria.fr/linux/long.pdf show that rcu-fence behaves like an inter-CPU strong fence. Furthermore, the definition of rb in terms of rcu-fence is highly analogous to the definition of pb in terms of strong-fence, which can help explain why rcu-path expresses a form of temporal ordering. This change should not affect the semantics of the memory model, just its internal organization. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> Reviewed-by: Andrea Parri <parri.andrea@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-2-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15tools/memory-model: Rename link and rcu-path to rcu-link and rbAlan Stern2-54/+55
This patch makes a simple non-functional change to the RCU portion of the Linux Kernel Memory Consistency Model by renaming the "link" and "rcu-path" relations to "rcu-link" and "rb", respectively. The name "link" was an unfortunate choice, because it was too generic and subject to confusion with other meanings of the same word, which occur quite often in LKMM documentation. The name "rcu-path" is not very appropriate, because the relation is analogous to the happens-before (hb) and propagates-before (pb) relations -- although that fact won't become apparent until the second patch in this series. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-1-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-03-10tools/memory-model: Finish the removal of rb-dep, ↵Alan Stern3-6/+6
smp_read_barrier_depends(), and lockless_dereference() Commit: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference") was merged too early, while it was still in RFC form. This patch adds in the missing pieces. Akira pointed out some typos in the original patch, and he noted that cheatsheet.txt should indicate that READ_ONCE() now implies an address dependency. Andrea suggested documenting the relationship betwwen unsuccessful RMW operations and address dependencies. Andrea pointed out that the macro for rcu_dereference() in linux.def should now use the "once" annotation instead of "deref". He also suggested that the comments should mention commit: 5a8897cc7631 ("locking/atomics/alpha: Add smp_read_barrier_depends() to _release()/_relaxed() atomics") ... as an important precursor, and he contributed commit: cb13b424e986 ("locking/xchg/alpha: Add unconditional memory barrier to cmpxchg()") which is another prerequisite. Suggested-by: Akira Yokosawa <akiyks@gmail.com> Suggested-by: Andrea Parri <parri.andrea@gmail.com> Signed-off-by: Alan Stern <stern@rowland.harvard.edu> [ Fixed read_read_lock() typo reported by Akira. ] Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Acked-by: Akira Yokosawa <akiyks@gmail.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: will.deacon@arm.com Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference") Link: http://lkml.kernel.org/r/1520443660-16858-4-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-03-10tools/memory-model: Add documentation of new litmus testPaul E. McKenney1-0/+6
The litmus-tests/README file lacks any mention of the new litmus test ISA2+pooncelock+pooncelock+pombonce.litmus. This commit therefore adds a description of this test. Reported-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1520443660-16858-3-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-03-10tools/memory-model: Remove mention of docker/gentoo imagePaul E. McKenney1-15/+0
Because the docker and gentoo images haven't been updated in quite some time, they are likely to provide more confusion than help. This commit therefore removes mention of them from the README file. Reported-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1520443660-16858-2-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and ↵Alan Stern5-48/+46
lockless_dereference Since commit 76ebbe78f739 ("locking/barriers: Add implicit smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15 kernel, it has not been necessary to use smp_read_barrier_depends(). Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill lockless_dereference()") removed lockless_dereference() from the kernel. Since these primitives are no longer part of the kernel, they do not belong in the Linux Kernel Memory Consistency Model. This patch removes them, along with the internal rb-dep relation, and updates the revelant documentation. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-12-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21tools/memory-model: Convert underscores to hyphensPaul E. McKenney3-9/+9
Typical cat-language code uses hyphens for word separators in identifiers, but several LKMM identifiers use underscores instead. This commit therefore converts underscores to hyphens in the .bell- and .cat-file identifiers corresponding to smp_mb__before_atomic(), smp_mb__after_atomic(), and smp_mb__after_spinlock(). Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-11-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21tools/memory-model: Add a S lock-based external-view litmus testAlan Stern1-0/+41
This commit adds a litmus test in which P0() and P1() form a lock-based S litmus test, with the addition of P2(), which observes P0()'s and P1()'s accesses with a full memory barrier but without the lock. This litmus test asks whether writes carried out by two different processes under the same lock will be seen in order by a third process not holding that lock. The answer to this question is "yes" for all architectures supporting the Linux kernel, but is "no" according to the current version of LKMM. A patch to LKMM is under development. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-10-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21tools/memory-model: Add required herd7 version to README filePaul E. McKenney1-1/+2
LKMM and the herd7 tool are co-evolving, and out-of-date herd7 tools produce inaccurate results, often with no obvious error messages. This commit therefore adds the required herd7 version to the LKMM README file. Longer term, it would be good if .cat files could specify the required version in a manner allowing herd7 to produce clear diagnostics. Suggested-by: Akira Yokosawa <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-9-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21README: Fix a couple of punctuation errorsPaul E. McKenney1-2/+2
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-5-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21EXP litmus_tests: Add comments explaining tests' purposesPaul E. McKenney28-1/+246
This commit adds comments to the litmus tests summarizing what these tests are intended to demonstrate. [ paulmck: Apply Andrea's and Alan's feedback. ] Suggested-by: Ingo Molnar <mingo@kernel.org> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-4-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-02-21MAINTAINERS: Add the Memory Consistency Model subsystemAndrea Parri1-15/+0
Move the contents of tools/memory-model/MAINTAINERS into the main MAINTAINERS file, removing tools/memory-model/MAINTAINERS. This allows get_maintainer.pl to correctly identify the maintainers of tools/memory-model/. Suggested-by: Ingo Molnar <mingo@kernel.org> Signed-off-by: Andrea Parri <parri.andrea@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Acked-by: Will Deacon <will.deacon@arm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Link: http://lkml.kernel.org/r/1519169112-20593-2-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>