From: "Paul E. McKenney" <paulmck@linux.ibm.com>
To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
mingo@kernel.org
Cc: stern@rowland.harvard.edu, andrea.parri@amarulasolutions.com,
will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com,
npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
luc.maranget@inria.fr, akiyks@gmail.com
Subject: [PATCH RFC memory-model 0/33] LKMM updates for review
Date: Thu, 30 May 2019 07:42:02 -0700 [thread overview]
Message-ID: <20190530144202.GA26201@linux.ibm.com> (raw)
Hello!
This series contains LKMM updates:
1-3. Add plain C-language accesses to the model, including data-race
detection, courtesy of Alan Stern.
4. Make scripts be executable.
5. Explain ordering provided by smp_mb__{before,after}_atomic(),
courtesy of Alan Stern.
6. Fix comment in MP+poonceonces.litmus, courtesy of Andrea Parri.
7. Make documentation referencing "herd" instead reference the
actual name of the command, "herd7", courtesy of Andrea Parri.
8-9. Make LKMM scripts note timeouts instead of just saying that
the validation was bad.
10. Make LKMM scripts identify litmus-test typos and use of
unsupported primitives instead of just saying that the validation
was bad.
11. Make LKMM scripts detect unconditional deadlocks.
12. Fix email address on LKMM scripts.
13-33. Leverage Boqun Feng's C-to-assembly litmus-test-translation
capability to allow verifying LKMM against hardware models for
checkalllitmus.sh. This is a work in progress.
Thanx, Paul
------------------------------------------------------------------------
Documentation/atomic_t.txt | 17 +-
tools/memory-model/linux-kernel.bell | 6
tools/memory-model/linux-kernel.cat | 82 ++++++++--
tools/memory-model/linux-kernel.def | 1
tools/memory-model/litmus-tests/.gitignore | 4
tools/memory-model/litmus-tests/MP+poonceonces.litmus | 2
tools/memory-model/litmus-tests/README | 2
tools/memory-model/lock.cat | 2
tools/memory-model/scripts/README | 20 +-
tools/memory-model/scripts/checkalllitmus.sh | 31 +--
tools/memory-model/scripts/checkghlitmus.sh | 11 -
tools/memory-model/scripts/checklitmus.sh | 103 +++++--------
tools/memory-model/scripts/checklitmushist.sh | 2
tools/memory-model/scripts/checktheselitmus.sh | 43 +++++
tools/memory-model/scripts/cmplitmushist.sh | 53 ++++++
tools/memory-model/scripts/hwfnseg.sh | 20 ++
tools/memory-model/scripts/initlitmushist.sh | 2
tools/memory-model/scripts/judgelitmus.sh | 136 +++++++++++++----
tools/memory-model/scripts/newlitmushist.sh | 4
tools/memory-model/scripts/parseargs.sh | 23 ++
tools/memory-model/scripts/runlitmus.sh | 142 ++++++++++++++----
tools/memory-model/scripts/runlitmushist.sh | 32 ++--
tools/memory-model/scripts/simpletest.sh | 35 ++++
23 files changed, 573 insertions(+), 200 deletions(-)
next reply other threads:[~2019-05-30 14:42 UTC|newest]
Thread overview: 68+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-05-30 14:42 Paul E. McKenney [this message]
2019-05-30 14:41 ` [PATCH RFC memory-model 01/33] tools/memory-model: Prepare for data-race detection Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:41 ` [PATCH RFC memory-model 02/33] tools/memory-model: Add definitions of plain and marked accesses Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:41 ` [PATCH RFC memory-model 03/33] tools/memory-model: Add data-race detection Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:41 ` [PATCH RFC memory-model 04/33] tools/memory-model: Make scripts be executable Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:41 ` [PATCH RFC memory-model 05/33] Documentation: atomic_t.txt: Explain ordering provided by smp_mb__{before,after}_atomic() Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:41 ` [PATCH RFC memory-model 06/33] tools/memory-model: Fix comment in MP+poonceonces.litmus Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:41 ` [PATCH RFC memory-model 07/33] tools/memory-model: Do not use "herd" to refer to "herd7" Paul E. McKenney
2019-05-30 14:41 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 08/33] tools/memory-model: Make judgelitmus.sh note timeouts Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 09/33] tools/memory-model: Make cmplitmushist.sh " Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 0/33] LKMM updates for review Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 10/33] tools/memory-model: Make judgelitmus.sh identify bad macros Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 11/33] tools/memory-model: Make judgelitmus.sh detect hard deadlocks Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 12/33] tools/memory-model: Fix paulmck email address on pre-existing scripts Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 13/33] tools/memory-model: Update parseargs.sh for hardware verification Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 14/33] tools/memory-model: Make judgelitmus.sh handle hardware verifications Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 15/33] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 16/33] tools/memory-model: Fix checkalllitmus.sh comment Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 17/33] tools/memory-model: Hardware checking for check{,all}litmus.sh Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 18/33] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 19/33] tools/memory-model: Split runlitmus.sh out of checklitmus.sh Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 20/33] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 21/33] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 22/33] tools/memory-model: Keep assembly-language litmus tests Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 23/33] tools/memory-model: Allow herd to deduce CPU type Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 24/33] tools/memory-model: Make runlitmus.sh check for jingle errors Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 25/33] tools/memory-model: Add -v flag to jingle7 runs Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 26/33] tools/memory-model: Implement --hw support for checkghlitmus.sh Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 27/33] tools/memory-model: Fix scripting --jobs argument Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 28/33] tools/memory-model: Make checkghlitmus.sh use mselect7 Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 29/33] tools/memory-model: Make history-check scripts " Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 30/33] tools/memory-model: Add "--" to parseargs.sh for additional arguments Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 31/33] tools/memory-model: Repair parseargs.sh header comment Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 32/33] tools/memory-model: Add checktheselitmus.sh to run specified litmus tests Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
2019-05-30 14:42 ` [PATCH RFC memory-model 33/33] tools/memory-model: Add data-race capabilities to judgelitmus.sh Paul E. McKenney
2019-05-30 14:42 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20190530144202.GA26201@linux.ibm.com \
--to=paulmck@linux.ibm.com \
--cc=akiyks@gmail.com \
--cc=andrea.parri@amarulasolutions.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=j.alglave@ucl.ac.uk \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mingo@kernel.org \
--cc=npiggin@gmail.com \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=will.deacon@arm.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).