lkml.org 
[lkml]   [2018]   [Dec]   [3]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
Subject[PATCH memory-model 0/3] Updates to the formal memory model
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(-)

\
 
 \ /
  Last update: 2018-12-04 00:04    [W:0.122 / U:2.900 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site