linux-kernel.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
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, parri.andrea@gmail.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 memory-model 0/3] Updates to the formal memory model
Date: Mon, 3 Dec 2018 15:04:11 -0800	[thread overview]
Message-ID: <20181203230411.GA27476@linux.ibm.com> (raw)

Hello, Ingo!

This series contains updates to the Linux kernel's formal memory model
in tools/memory-model.  These patches are ready for inclusion into -tip.

1.	Model smp_mb__after_unlock_lock(), courtesy of Andrea Parri.

2.	Add scripts to check github litmus tests.

3.	Make scripts take "-j" abbreviation for "--jobs".

There is another series in preparation to model SRCU, but this series
requires hot-off-the presses changes to the herd tool that have not yet
been released.  This SRCU series is therefore targeting the merge window
after the upcoming one.  People wishing to experiment with the prototype
SRCU model may obtain it from my -rcu tree at branch "dev", and use
a bleeding-edge herd7 built from https://github.com/herd/herdtools7/,
version 7.51+2(dev), which is (commit 10403b24070c) or later.

							Thanx, Paul

------------------------------------------------------------------------

 .gitignore                 |    1 
 README                     |    2 
 linux-kernel.bell          |    3 
 linux-kernel.cat           |    4 -
 linux-kernel.def           |    1 
 scripts/README             |   70 ++++++++++++++++++++++
 scripts/checkalllitmus.sh  |   53 +++++++----------
 scripts/checkghlitmus.sh   |   65 ++++++++++++++++++++
 scripts/checklitmus.sh     |   74 +++--------------------
 scripts/checklitmushist.sh |   60 +++++++++++++++++++
 scripts/cmplitmushist.sh   |   87 +++++++++++++++++++++++++++
 scripts/initlitmushist.sh  |   68 +++++++++++++++++++++
 scripts/judgelitmus.sh     |   78 +++++++++++++++++++++++++
 scripts/newlitmushist.sh   |   61 +++++++++++++++++++
 scripts/parseargs.sh       |  140 ++++++++++++++++++++++++++++++++++++++++++++-
 scripts/runlitmushist.sh   |   87 +++++++++++++++++++++++++++
 16 files changed, 757 insertions(+), 97 deletions(-)


             reply	other threads:[~2018-12-03 23:04 UTC|newest]

Thread overview: 14+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-12-03 23:04 Paul E. McKenney [this message]
2018-12-03 23:04 ` [PATCH memory-model 1/3] tools/memory-model: Model smp_mb__after_unlock_lock() Paul E. McKenney
2018-12-04  6:33   ` [tip:locking/core] " tip-bot for Andrea Parri
2019-01-21 11:23   ` tip-bot for Andrea Parri
2018-12-03 23:04 ` [PATCH memory-model 2/3] EXP tools/memory-model: Add scripts to check github litmus tests Paul E. McKenney
2018-12-04  6:34   ` [tip:locking/core] " tip-bot for Paul E. McKenney
2019-01-21 11:24   ` tip-bot for Paul E. McKenney
2018-12-03 23:04 ` [PATCH memory-model 3/3] EXP tools/memory-model: Make scripts take "-j" abbreviation for "--jobs" Paul E. McKenney
2018-12-04  6:35   ` [tip:locking/core] " tip-bot for Paul E. McKenney
2019-01-21 11:25   ` tip-bot for Paul E. McKenney
2018-12-03 23:28 ` [PATCH memory-model 0/3] Updates to the formal memory model Akira Yokosawa
2018-12-03 23:51   ` Paul E. McKenney
2018-12-04 15:40     ` Akira Yokosawa
2018-12-04 16:36       ` 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=20181203230411.GA27476@linux.ibm.com \
    --to=paulmck@linux.ibm.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=linux-kernel@vger.kernel.org \
    --cc=luc.maranget@inria.fr \
    --cc=mingo@kernel.org \
    --cc=npiggin@gmail.com \
    --cc=parri.andrea@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).