Hello!
This series contains memory-model updates, not yet ready for inclusion:
1. Add extra ordering for locks and remove it for ordinary
release/acquire, courtesy of Alan Stern. There is some
remaining disagreement as to whether or not locks and ordinary
release/acquire should have identical ordering properties.
2. Replace smp_cond_acquire() with smp_cond_load_acquire(),
courtesy of Andrea Parri.
3. Expand the list of LKMM limitations.
4. Fix a README typo, courtesy of SeongJae Park.
5. Add scripts to check github litmus tests.
6. Make scripts take "-j" abbreviation for "--jobs".
7. Add .cfg and .cat files for s390, which is a not-for-mainline
placeholder.
Thanx, Paul
------------------------------------------------------------------------
Documentation/memory-barriers.txt | 3
tools/memory-model/.gitignore | 1
tools/memory-model/Documentation/explanation.txt | 186 +++++++---
tools/memory-model/Documentation/recipes.txt | 2
tools/memory-model/README | 41 ++
tools/memory-model/linux-kernel.cat | 8
tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7
tools/memory-model/s390.cat | 18
tools/memory-model/s390.cfg | 21 +
tools/memory-model/scripts/README | 70 +++
tools/memory-model/scripts/checkalllitmus.sh | 53 +-
tools/memory-model/scripts/checkghlitmus.sh | 65 +++
tools/memory-model/scripts/checklitmus.sh | 74 ---
tools/memory-model/scripts/checklitmushist.sh | 60 +++
tools/memory-model/scripts/cmplitmushist.sh | 87 ++++
tools/memory-model/scripts/initlitmushist.sh | 68 +++
tools/memory-model/scripts/judgelitmus.sh | 78 ++++
tools/memory-model/scripts/newlitmushist.sh | 61 +++
tools/memory-model/scripts/parseargs.sh | 140 +++++++
tools/memory-model/scripts/runlitmushist.sh | 87 ++++
20 files changed, 981 insertions(+), 149 deletions(-)
From: Andrea Parri <[email protected]>
Amend commit 1f03e8d2919270 ("locking/barriers: Replace smp_cond_acquire()
with smp_cond_load_acquire()") by updating the documentation accordingly.
Also remove some obsolete information related to the implementation.
Signed-off-by: Andrea Parri <[email protected]>
Cc: Alan Stern <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
Documentation/memory-barriers.txt | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 0d8d7ef131e9..c1d913944ad8 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -471,8 +471,7 @@ And a couple of implicit varieties:
operations after the ACQUIRE operation will appear to happen after the
ACQUIRE operation with respect to the other components of the system.
ACQUIRE operations include LOCK operations and both smp_load_acquire()
- and smp_cond_acquire() operations. The later builds the necessary ACQUIRE
- semantics from relying on a control dependency and smp_rmb().
+ and smp_cond_load_acquire() operations.
Memory operations that occur before an ACQUIRE operation may appear to
happen after it completes.
--
2.17.1
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.
Signed-off-by: Paul E. McKenney <[email protected]>
[ paulmck: History-check summary-line changes per Alan Stern feedback. ]
---
tools/memory-model/.gitignore | 1 +
tools/memory-model/README | 2 +
tools/memory-model/scripts/README | 70 ++++++++++
tools/memory-model/scripts/checkalllitmus.sh | 53 ++++----
tools/memory-model/scripts/checkghlitmus.sh | 65 +++++++++
tools/memory-model/scripts/checklitmus.sh | 74 ++--------
tools/memory-model/scripts/checklitmushist.sh | 60 +++++++++
tools/memory-model/scripts/cmplitmushist.sh | 87 ++++++++++++
tools/memory-model/scripts/initlitmushist.sh | 68 ++++++++++
tools/memory-model/scripts/judgelitmus.sh | 78 +++++++++++
tools/memory-model/scripts/newlitmushist.sh | 61 +++++++++
tools/memory-model/scripts/parseargs.sh | 126 ++++++++++++++++++
tools/memory-model/scripts/runlitmushist.sh | 87 ++++++++++++
13 files changed, 739 insertions(+), 93 deletions(-)
create mode 100644 tools/memory-model/.gitignore
create mode 100644 tools/memory-model/scripts/README
create mode 100755 tools/memory-model/scripts/checkghlitmus.sh
create mode 100755 tools/memory-model/scripts/checklitmushist.sh
create mode 100644 tools/memory-model/scripts/cmplitmushist.sh
create mode 100755 tools/memory-model/scripts/initlitmushist.sh
create mode 100755 tools/memory-model/scripts/judgelitmus.sh
create mode 100755 tools/memory-model/scripts/newlitmushist.sh
create mode 100755 tools/memory-model/scripts/parseargs.sh
create mode 100755 tools/memory-model/scripts/runlitmushist.sh
diff --git a/tools/memory-model/.gitignore b/tools/memory-model/.gitignore
new file mode 100644
index 000000000000..b1d34c52f3c3
--- /dev/null
+++ b/tools/memory-model/.gitignore
@@ -0,0 +1 @@
+litmus
diff --git a/tools/memory-model/README b/tools/memory-model/README
index acf9077cffaa..0f2c366518c6 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -156,6 +156,8 @@ lock.cat
README
This file.
+scripts Various scripts, see scripts/README.
+
===========
LIMITATIONS
diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
new file mode 100644
index 000000000000..29375a1fbbfa
--- /dev/null
+++ b/tools/memory-model/scripts/README
@@ -0,0 +1,70 @@
+ ============
+ LKMM SCRIPTS
+ ============
+
+
+These scripts are run from the tools/memory-model directory.
+
+checkalllitmus.sh
+
+ Run all litmus tests in the litmus-tests directory, checking
+ the results against the expected results recorded in the
+ "Result:" comment lines.
+
+checkghlitmus.sh
+
+ Run 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.
+
+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.
+
+checklitmus.sh
+
+ Check a single litmus test against its "Result:" expected result.
+
+cmplitmushist.sh
+
+ Compare output from two different runs of the same litmus tests,
+ with the absolute pathnames of the tests to run provided one
+ name per line on standard input. Not normally run manually,
+ provided instead for use by other scripts.
+
+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.
+
+judgelitmus.sh
+
+ Given a .litmus file and its .litmus.out herd output, check the
+ .litmus.out file against the .litmus file's "Result:" comment to
+ judge whether the test ran correctly. Not normally run manually,
+ provided instead for use by other scripts.
+
+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.
+
+parseargs.sh
+
+ Parse command-line arguments. Not normally run manually,
+ provided instead for use by other scripts.
+
+runlitmushist.sh
+
+ Run the litmus tests whose absolute pathnames are provided one
+ name per line on standard input. Not normally run manually,
+ provided instead for use by other scripts.
+
+README
+
+ This file
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index ca528f9a24d4..b35fcd61ecf6 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -1,42 +1,27 @@
#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
#
-# Run herd tests on all .litmus files in the specified directory (which
-# defaults to litmus-tests) and check each file's result against a "Result:"
-# comment within that litmus test. If the verification result does not
-# match that specified in the litmus test, this script prints an error
-# message prefixed with "^^^". It also outputs verification results to
-# a file whose name is that of the specified litmus test, but with ".out"
-# appended.
+# Run herd tests on all .litmus files in the litmus-tests directory
+# and check each file's result against a "Result:" comment within that
+# litmus test. If the verification result does not match that specified
+# in the litmus test, this script prints an error message prefixed with
+# "^^^". It also outputs verification results to a file whose name is
+# that of the specified litmus test, but with ".out" appended.
#
# Usage:
-# checkalllitmus.sh [ directory ]
+# checkalllitmus.sh
#
-# The LINUX_HERD_OPTIONS environment variable may be used to specify
-# arguments to herd, whose default is defined by the checklitmus.sh script.
-# Thus, one would normally run this in the directory containing the memory
-# model, specifying the pathname of the litmus test to check.
+# Run this in the directory containing the memory model.
#
# This script makes no attempt to run the litmus tests concurrently.
#
-# This program is free software; you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation; either version 2 of the License, or
-# (at your option) any later version.
-#
-# This program is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-# GNU General Public License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with this program; if not, you can access it online at
-# http://www.gnu.org/licenses/gpl-2.0.html.
-#
# Copyright IBM Corporation, 2018
#
# Author: Paul E. McKenney <[email protected]>
-litmusdir=${1-litmus-tests}
+. scripts/parseargs.sh
+
+litmusdir=litmus-tests
if test -d "$litmusdir" -a -r "$litmusdir" -a -x "$litmusdir"
then
:
@@ -45,6 +30,14 @@ else
exit 255
fi
+# Create any new directories that have appeared in the github litmus
+# repo since the last run.
+if test "$LKMM_DESTDIR" != "."
+then
+ find $litmusdir -type d -print |
+ ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
+fi
+
# Find the checklitmus script. If it is not where we expect it, then
# assume that the caller has the PATH environment variable set
# appropriately.
@@ -57,7 +50,7 @@ fi
# Run the script on all the litmus tests in the specified directory
ret=0
-for i in litmus-tests/*.litmus
+for i in $litmusdir/*.litmus
do
if ! $clscript $i
then
@@ -66,8 +59,8 @@ do
done
if test "$ret" -ne 0
then
- echo " ^^^ VERIFICATION MISMATCHES"
+ echo " ^^^ VERIFICATION MISMATCHES" 1>&2
else
- echo All litmus tests verified as was expected.
+ echo All litmus tests verified as was expected. 1>&2
fi
exit $ret
diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
new file mode 100755
index 000000000000..6589fbb6f653
--- /dev/null
+++ b/tools/memory-model/scripts/checkghlitmus.sh
@@ -0,0 +1,65 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Runs the C-language litmus tests having a maximum number of processes
+# to run, defaults to 6.
+#
+# sh checkghlitmus.sh
+#
+# Run from the Linux kernel tools/memory-model directory. See the
+# parseargs.sh scripts for arguments.
+
+. scripts/parseargs.sh
+
+T=/tmp/checkghlitmus.sh.$$
+trap 'rm -rf $T' 0
+mkdir $T
+
+# Clone the repository if it is not already present.
+if test -d litmus
+then
+ :
+else
+ git clone https://github.com/paulmckrcu/litmus
+ ( cd litmus; git checkout origin/master )
+fi
+
+# Create any new directories that have appeared in the github litmus
+# repo since the last run.
+if test "$LKMM_DESTDIR" != "."
+then
+ find litmus -type d -print |
+ ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
+fi
+
+# Create a list of the C-language litmus tests previously run.
+( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
+ sed -e 's/\.out$//' |
+ xargs -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' |
+ xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
+
+# Create a list of C-language litmus tests with "Result:" commands and
+# no more than the specified number of processes.
+find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
+xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result
+xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short
+
+# Form list of tests without corresponding .litmus.out files
+sort $T/list-C-already $T/list-C-result-short | uniq -u > $T/list-C-needed
+
+# Run any needed tests.
+if scripts/runlitmushist.sh < $T/list-C-needed > $T/run.stdout 2> $T/run.stderr
+then
+ errs=
+else
+ errs=1
+fi
+
+sed < $T/list-C-result-short -e 's,^,scripts/judgelitmus.sh ,' |
+ sh > $T/judge.stdout 2> $T/judge.stderr
+
+if test -n "$errs"
+then
+ cat $T/run.stderr 1>&2
+fi
+grep '!!!' $T/judge.stdout
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index bf12a75c0719..dd08801a30b0 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -1,40 +1,24 @@
#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
#
-# Run a herd test and check the result against a "Result:" comment within
-# the litmus test. If the verification result does not match that specified
-# in the litmus test, this script prints an error message prefixed with
-# "^^^" and exits with a non-zero status. It also outputs verification
+# Run a herd test and invokes judgelitmus.sh to check the result against
+# a "Result:" comment within the litmus test. It also outputs verification
# results to a file whose name is that of the specified litmus test, but
# with ".out" appended.
#
# Usage:
# checklitmus.sh file.litmus
#
-# The LINUX_HERD_OPTIONS environment variable may be used to specify
-# arguments to herd, which default to "-conf linux-kernel.cfg". Thus,
-# one would normally run this in the directory containing the memory model,
-# specifying the pathname of the litmus test to check.
-#
-# This program is free software; you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation; either version 2 of the License, or
-# (at your option) any later version.
-#
-# This program is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-# GNU General Public License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with this program; if not, you can access it online at
-# http://www.gnu.org/licenses/gpl-2.0.html.
+# Run this in the directory containing the memory model, specifying the
+# pathname of the litmus test to check. The caller is expected to have
+# properly set up the LKMM environment variables.
#
# Copyright IBM Corporation, 2018
#
# Author: Paul E. McKenney <[email protected]>
litmus=$1
-herdoptions=${LINUX_HERD_OPTIONS--conf linux-kernel.cfg}
+herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
if test -f "$litmus" -a -r "$litmus"
then
@@ -43,44 +27,8 @@ else
echo ' --- ' error: \"$litmus\" is not a readable file
exit 255
fi
-if grep -q '^ \* Result: ' $litmus
-then
- outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
-else
- outcome=specified
-fi
-echo Herd options: $herdoptions > $litmus.out
-/usr/bin/time herd7 -o ~/tmp $herdoptions $litmus >> $litmus.out 2>&1
-grep "Herd options:" $litmus.out
-grep '^Observation' $litmus.out
-if grep -q '^Observation' $litmus.out
-then
- :
-else
- cat $litmus.out
- echo ' ^^^ Verification error'
- echo ' ^^^ Verification error' >> $litmus.out 2>&1
- exit 255
-fi
-if test "$outcome" = DEADLOCK
-then
- echo grep 3 and 4
- if grep '^Observation' $litmus.out | grep -q 'Never 0 0$'
- then
- ret=0
- else
- echo " ^^^ Unexpected non-$outcome verification"
- echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
- ret=1
- fi
-elif grep '^Observation' $litmus.out | grep -q $outcome || test "$outcome" = Maybe
-then
- ret=0
-else
- echo " ^^^ Unexpected non-$outcome verification"
- echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
- ret=1
-fi
-tail -2 $litmus.out | head -1
-exit $ret
+echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+
+scripts/judgelitmus.sh $litmus
diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh
new file mode 100755
index 000000000000..1d210ffb7c8a
--- /dev/null
+++ b/tools/memory-model/scripts/checklitmushist.sh
@@ -0,0 +1,60 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Reruns the C-language litmus tests previously run that match the
+# specified criteria, and compares the result to that of the previous
+# runs from initlitmushist.sh and/or newlitmushist.sh.
+#
+# sh checklitmushist.sh
+#
+# Run from the Linux kernel tools/memory-model directory.
+# See scripts/parseargs.sh for list of arguments.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <[email protected]>
+
+. scripts/parseargs.sh
+
+T=/tmp/checklitmushist.sh.$$
+trap 'rm -rf $T' 0
+mkdir $T
+
+if test -d litmus
+then
+ :
+else
+ echo Run scripts/initlitmushist.sh first, need litmus repo.
+ exit 1
+fi
+
+# Create the results directory and populate it with subdirectories.
+# The initial output is created here to avoid clobbering the output
+# generated earlier.
+mkdir $T/results
+find litmus -type d -print | ( cd $T/results; sed -e 's/^/mkdir -p /' | sh )
+
+# Create the list of litmus tests already run, then remove those that
+# are excluded by this run's --procs argument.
+( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
+ sed -e 's/\.out$//' |
+ xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
+xargs < $T/list-C-already -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
+
+# Redirect output, run tests, then restore destination directory.
+destdir="$LKMM_DESTDIR"
+LKMM_DESTDIR=$T/results; export LKMM_DESTDIR
+scripts/runlitmushist.sh < $T/list-C-short > $T/runlitmushist.sh.out 2>&1
+LKMM_DESTDIR="$destdir"; export LKMM_DESTDIR
+
+# Move the newly generated .litmus.out files to .litmus.out.new files
+# in the destination directory.
+cdir=`pwd`
+ddir=`awk -v c="$cdir" -v d="$LKMM_DESTDIR" \
+ 'END { if (d ~ /^\//) print d; else print c "/" d; }' < /dev/null`
+( cd $T/results; find litmus -type f -name '*.litmus.out' -print |
+ sed -e 's,^.*$,cp & '"$ddir"'/&.new,' | sh )
+
+sed < $T/list-C-short -e 's,^,'"$LKMM_DESTDIR/"',' |
+ sh scripts/cmplitmushist.sh
+exit $?
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
new file mode 100644
index 000000000000..0f498aeeccf5
--- /dev/null
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -0,0 +1,87 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Compares .out and .out.new files for each name on standard input,
+# one full pathname per line. Outputs comparison results followed by
+# a summary.
+#
+# sh cmplitmushist.sh
+
+T=/tmp/cmplitmushist.sh.$$
+trap 'rm -rf $T' 0
+mkdir $T
+
+# comparetest oldpath newpath
+perfect=0
+obsline=0
+noobsline=0
+obsresult=0
+badcompare=0
+comparetest () {
+ grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout
+ grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout
+ if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1
+ then
+ echo Exact output match: $2
+ perfect=`expr "$perfect" + 1`
+ return 0
+ fi
+
+ grep '^Observation' $1 > $T/oldout
+ grep '^Observation' $2 > $T/newout
+ if test -s $T/oldout -o -s $T/newout
+ then
+ if cmp -s $T/oldout $T/newout
+ then
+ echo Matching Observation result and counts: $2
+ obsline=`expr "$obsline" + 1`
+ return 0
+ fi
+ else
+ echo Missing Observation line "(e.g., herd7 timeout)": $2
+ noobsline=`expr "$noobsline" + 1`
+ return 0
+ fi
+
+ grep '^Observation' $1 | awk '{ print $3 }' > $T/oldout
+ grep '^Observation' $2 | awk '{ print $3 }' > $T/newout
+ if cmp -s $T/oldout $T/newout
+ then
+ echo Matching Observation Always/Sometimes/Never result: $2
+ obsresult=`expr "$obsresult" + 1`
+ return 0
+ fi
+ echo ' !!!' Result changed: $2
+ badcompare=`expr "$badcompare" + 1`
+ return 1
+}
+
+sed -e 's/^.*$/comparetest &.out &.out.new/' > $T/cmpscript
+. $T/cmpscript > $T/cmpscript.out
+cat $T/cmpscript.out
+
+echo ' ---' Summary: 1>&2
+grep '!!!' $T/cmpscript.out 1>&2
+if test "$perfect" -ne 0
+then
+ echo Exact output matches: $perfect 1>&2
+fi
+if test "$obsline" -ne 0
+then
+ echo Matching Observation result and counts: $obsline 1>&2
+fi
+if test "$noobsline" -ne 0
+then
+ echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2
+fi
+if test "$obsresult" -ne 0
+then
+ echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2
+fi
+if test "$badcompare" -ne 0
+then
+ echo "!!!" Result changed: $badcompare 1>&2
+ exit 1
+fi
+
+exit 0
diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh
new file mode 100755
index 000000000000..956b6957484d
--- /dev/null
+++ b/tools/memory-model/scripts/initlitmushist.sh
@@ -0,0 +1,68 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Runs the C-language litmus tests matching the specified criteria.
+# Generates the output for each .litmus file into a corresponding
+# .litmus.out file, and does not judge the result.
+#
+# sh initlitmushist.sh
+#
+# Run from the Linux kernel tools/memory-model directory.
+# See scripts/parseargs.sh for list of arguments.
+#
+# This script can consume significant wallclock time and CPU, especially as
+# the value of --procs rises. On a four-core (eight hardware threads)
+# 2.5GHz x86 with a one-minute per-run timeout:
+#
+# --procs wallclock CPU timeouts tests
+# 1 0m11.241s 0m1.086s 0 19
+# 2 1m12.598s 2m8.459s 2 393
+# 3 1m30.007s 6m2.479s 4 2291
+# 4 3m26.042s 18m5.139s 9 3217
+# 5 4m26.661s 23m54.128s 13 3784
+# 6 4m41.900s 26m4.721s 13 4352
+# 7 5m51.463s 35m50.868s 13 4626
+# 8 10m5.235s 68m43.672s 34 5117
+# 9 15m57.80s 105m58.101s 69 5156
+# 10 16m14.13s 103m35.009s 69 5165
+# 20 27m48.55s 198m3.286s 156 5269
+#
+# Increasing the timeout on the 20-process run to five minutes increases
+# the runtime to about 90 minutes with the CPU time rising to about
+# 10 hours. On the other hand, it decreases the number of timeouts to 101.
+#
+# Note that there are historical tests for which herd7 will fail
+# completely, for example, litmus/manual/atomic/C-unlock-wait-00.litmus
+# contains a call to spin_unlock_wait(), which no longer exists in either
+# the kernel or LKMM.
+
+. scripts/parseargs.sh
+
+T=/tmp/initlitmushist.sh.$$
+trap 'rm -rf $T' 0
+mkdir $T
+
+if test -d litmus
+then
+ :
+else
+ git clone https://github.com/paulmckrcu/litmus
+ ( cd litmus; git checkout origin/master )
+fi
+
+# Create any new directories that have appeared in the github litmus
+# repo since the last run.
+if test "$LKMM_DESTDIR" != "."
+then
+ find litmus -type d -print |
+ ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
+fi
+
+# Create a list of the C-language litmus tests with no more than the
+# specified number of processes (per the --procs argument).
+find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
+xargs < $T/list-C -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
+
+scripts/runlitmushist.sh < $T/list-C-short
+
+exit 0
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
new file mode 100755
index 000000000000..0cc63875e395
--- /dev/null
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -0,0 +1,78 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Given a .litmus test and the corresponding .litmus.out file, check
+# the .litmus.out file against the "Result:" comment to judge whether
+# the test ran correctly.
+#
+# Usage:
+# judgelitmus.sh file.litmus
+#
+# Run this in the directory containing the memory model, specifying the
+# pathname of the litmus test to check.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <[email protected]>
+
+litmus=$1
+
+if test -f "$litmus" -a -r "$litmus"
+then
+ :
+else
+ echo ' --- ' error: \"$litmus\" is not a readable file
+ exit 255
+fi
+if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
+then
+ :
+else
+ echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
+ exit 255
+fi
+if grep -q '^ \* Result: ' $litmus
+then
+ outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
+else
+ outcome=specified
+fi
+
+grep '^Observation' $LKMM_DESTDIR/$litmus.out
+if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
+then
+ :
+else
+ echo ' !!! Verification error' $litmus
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ then
+ echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
+ fi
+ exit 255
+fi
+if test "$outcome" = DEADLOCK
+then
+ if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+ then
+ ret=0
+ else
+ echo " !!! Unexpected non-$outcome verification" $litmus
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ then
+ echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
+ fi
+ ret=1
+ fi
+elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
+then
+ ret=0
+else
+ echo " !!! Unexpected non-$outcome verification" $litmus
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ then
+ echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
+ fi
+ ret=1
+fi
+tail -2 $LKMM_DESTDIR/$litmus.out | head -1
+exit $ret
diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh
new file mode 100755
index 000000000000..991f8f814881
--- /dev/null
+++ b/tools/memory-model/scripts/newlitmushist.sh
@@ -0,0 +1,61 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Runs the C-language litmus tests matching the specified criteria
+# that do not already have a corresponding .litmus.out file, and does
+# not judge the result.
+#
+# sh newlitmushist.sh
+#
+# Run from the Linux kernel tools/memory-model directory.
+# See scripts/parseargs.sh for list of arguments.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <[email protected]>
+
+. scripts/parseargs.sh
+
+T=/tmp/newlitmushist.sh.$$
+trap 'rm -rf $T' 0
+mkdir $T
+
+if test -d litmus
+then
+ :
+else
+ echo Run scripts/initlitmushist.sh first, need litmus repo.
+ exit 1
+fi
+
+# Create any new directories that have appeared in the github litmus
+# repo since the last run.
+if test "$LKMM_DESTDIR" != "."
+then
+ find litmus -type d -print |
+ ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
+fi
+
+# Create a list of the C-language litmus tests previously run.
+( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
+ sed -e 's/\.out$//' |
+ xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
+
+# Form full list of litmus tests with no more than the specified
+# number of processes (per the --procs argument).
+find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C-all
+xargs < $T/list-C-all -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
+
+# Form list of new tests. Note: This does not handle litmus-test deletion!
+sort $T/list-C-already $T/list-C-short | uniq -u > $T/list-C-new
+
+# Form list of litmus tests that have changed since the last run.
+sed < $T/list-C-short -e 's,^.*$,if test & -nt '"$LKMM_DESTDIR"'/&.out; then echo &; fi,' > $T/list-C-script
+sh $T/list-C-script > $T/list-C-newer
+
+# Merge the list of new and of updated litmus tests: These must be (re)run.
+sort -u $T/list-C-new $T/list-C-newer > $T/list-C-needed
+
+scripts/runlitmushist.sh < $T/list-C-needed
+
+exit 0
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
new file mode 100755
index 000000000000..96b307c8d64a
--- /dev/null
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -0,0 +1,126 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# the corresponding .litmus.out file, and does not judge the result.
+#
+# . scripts/parseargs.sh
+#
+# Include into other Linux kernel tools/memory-model scripts.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <[email protected]>
+
+T=/tmp/parseargs.sh.$$
+mkdir $T
+
+# Initialize one parameter: initparam name default
+initparam () {
+ echo if test -z '"$'$1'"' > $T/s
+ echo then >> $T/s
+ echo $1='"'$2'"' >> $T/s
+ echo export $1 >> $T/s
+ echo fi >> $T/s
+ echo $1_DEF='$'$1 >> $T/s
+ . $T/s
+}
+
+initparam LKMM_DESTDIR "."
+initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg"
+initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN`
+initparam LKMM_PROCS "3"
+initparam LKMM_TIMEOUT "1m"
+
+scriptname=$0
+
+usagehelp () {
+ echo "Usage $scriptname [ arguments ]"
+ echo " --destdir path (place for .litmus.out, default by .litmus)"
+ echo " --herdopts -conf linux-kernel.cfg ..."
+ echo " --jobs N (number of jobs, default one per CPU)"
+ echo " --procs N (litmus tests with at most this many processes)"
+ echo " --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')"
+ echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
+ exit 1
+}
+
+usage () {
+ usagehelp 1>&2
+}
+
+# checkarg --argname argtype $# arg mustmatch cannotmatch
+checkarg () {
+ if test $3 -le 1
+ then
+ echo $1 needs argument $2 matching \"$5\"
+ usage
+ fi
+ if echo "$4" | grep -q -e "$5"
+ then
+ :
+ else
+ echo $1 $2 \"$4\" must match \"$5\"
+ usage
+ fi
+ if echo "$4" | grep -q -e "$6"
+ then
+ echo $1 $2 \"$4\" must not match \"$6\"
+ usage
+ fi
+}
+
+while test $# -gt 0
+do
+ case "$1" in
+ --destdir)
+ checkarg --destdir "(path to directory)" "$#" "$2" '.\+' '^--'
+ LKMM_DESTDIR="$2"
+ mkdir $LKMM_DESTDIR > /dev/null 2>&1
+ if ! test -e "$LKMM_DESTDIR"
+ then
+ echo "Cannot create directory --destdir '$LKMM_DESTDIR'"
+ usage
+ fi
+ if test -d "$LKMM_DESTDIR" -a -w "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR"
+ then
+ :
+ else
+ echo "Directory --destdir '$LKMM_DESTDIR' insufficient permissions to create files"
+ usage
+ fi
+ shift
+ ;;
+ --herdopts|--herdopt)
+ checkarg --destdir "(herd options)" "$#" "$2" '.*' '^--'
+ LKMM_HERD_OPTIONS="$2"
+ shift
+ ;;
+ --jobs|--job)
+ checkarg --jobs "(number)" "$#" "$2" '^[0-9]\+$' '^--'
+ LKMM_JOBS="$2"
+ shift
+ ;;
+ --procs|--proc)
+ checkarg --procs "(number)" "$#" "$2" '^[0-9]\+$' '^--'
+ LKMM_PROCS="$2"
+ shift
+ ;;
+ --timeout)
+ checkarg --timeout "(timeout spec)" "$#" "$2" '^\([0-9]\+[smhd]\?\|\)$' '^--'
+ LKMM_TIMEOUT="$2"
+ shift
+ ;;
+ *)
+ echo Unknown argument $1
+ usage
+ ;;
+ esac
+ shift
+done
+if test -z "$LKMM_TIMEOUT"
+then
+ LKMM_TIMEOUT_CMD=""; export LKMM_TIMEOUT_CMD
+else
+ LKMM_TIMEOUT_CMD="timeout $LKMM_TIMEOUT"; export LKMM_TIMEOUT_CMD
+fi
+rm -rf $T
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
new file mode 100755
index 000000000000..e507f5f933d5
--- /dev/null
+++ b/tools/memory-model/scripts/runlitmushist.sh
@@ -0,0 +1,87 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Runs the C-language litmus tests specified on standard input, using up
+# to the specified number of CPUs (defaulting to all of them) and placing
+# the results in the specified directory (defaulting to the same place
+# the litmus test came from).
+#
+# sh runlitmushist.sh
+#
+# Run from the Linux kernel tools/memory-model directory.
+# This script uses environment variables produced by parseargs.sh.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <[email protected]>
+
+T=/tmp/runlitmushist.sh.$$
+trap 'rm -rf $T' 0
+mkdir $T
+
+if test -d litmus
+then
+ :
+else
+ echo Directory \"litmus\" missing, aborting run.
+ exit 1
+fi
+
+# Prefixes for per-CPU scripts
+for ((i=0;i<$LKMM_JOBS;i++))
+do
+ echo dir="$LKMM_DESTDIR" > $T/$i.sh
+ echo T=$T >> $T/$i.sh
+ echo herdoptions=\"$LKMM_HERD_OPTIONS\" >> $T/$i.sh
+ cat << '___EOF___' >> $T/$i.sh
+ runtest () {
+ echo ' ... ' /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 '>' $dir/$1.out '2>&1'
+ if /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 > $dir/$1.out 2>&1
+ then
+ if ! grep -q '^Observation ' $dir/$1.out
+ then
+ echo ' !!! Herd failed, no Observation:' $1
+ fi
+ else
+ exitcode=$?
+ if test "$exitcode" -eq 124
+ then
+ exitmsg="timed out"
+ else
+ exitmsg="failed, exit code $exitcode"
+ fi
+ echo ' !!! Herd' ${exitmsg}: $1
+ fi
+ }
+___EOF___
+done
+
+awk -v q="'" -v b='\\' '
+{
+ print "echo `grep " q "^P[0-9]" b "+(" q " " $0 " | tail -1 | sed -e " q "s/^P" b "([0-9]" b "+" b ")(.*$/" b "1/" q "` " $0
+}' | bash |
+sort -k1n |
+awk -v ncpu=$LKMM_JOBS -v t=$T '
+{
+ print "runtest " $2 >> t "/" NR % ncpu ".sh";
+}
+
+END {
+ for (i = 0; i < ncpu; i++) {
+ print "sh " t "/" i ".sh > " t "/" i ".sh.out 2>&1 &";
+ close(t "/" i ".sh");
+ }
+ print "wait";
+}' | sh
+cat $T/*.sh.out
+if grep -q '!!!' $T/*.sh.out
+then
+ echo ' ---' Summary: 1>&2
+ grep '!!!' $T/*.sh.out 1>&2
+ nfail="`grep '!!!' $T/*.sh.out | wc -l`"
+ echo 'Number of failed herd runs (e.g., timeout): ' $nfail 1>&2
+ exit 1
+else
+ echo All runs completed successfully. 1>&2
+ exit 0
+fi
--
2.17.1
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/parseargs.sh | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 96b307c8d64a..859e1d581e05 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -95,8 +95,18 @@ do
LKMM_HERD_OPTIONS="$2"
shift
;;
- --jobs|--job)
- checkarg --jobs "(number)" "$#" "$2" '^[0-9]\+$' '^--'
+ -j[1-9]*)
+ njobs="`echo $1 | sed -e 's/^-j//'`"
+ trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`"
+ if test -n "$trailchars"
+ then
+ echo $1 trailing characters "'$trailchars'"
+ usagehelp
+ fi
+ LKMM_JOBS="`echo $njobs | sed -e 's/^\([0-9]\+\).*$/\1/'`"
+ ;;
+ --jobs|--job|-j)
+ checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]\+$' '^--'
LKMM_JOBS="$2"
shift
;;
--
2.17.1
This commit adds more detail about compiler optimizations and
not-yet-modeled Linux-kernel APIs.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/README | 39 +++++++++++++++++++++++++++++++++++++++
1 file changed, 39 insertions(+)
diff --git a/tools/memory-model/README b/tools/memory-model/README
index ee987ce20aae..acf9077cffaa 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -171,6 +171,12 @@ The Linux-kernel memory model has the following limitations:
particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
and "A WARNING" sections).
+ Note that this limitation in turn limits LKMM's ability to
+ accurately model address, control, and data dependencies.
+ For example, if the compiler can deduce the value of some variable
+ carrying a dependency, then the compiler can break that dependency
+ by substituting a constant of that value.
+
2. Multiple access sizes for a single variable are not supported,
and neither are misaligned or partially overlapping accesses.
@@ -190,6 +196,36 @@ The Linux-kernel memory model has the following limitations:
However, a substantial amount of support is provided for these
operations, as shown in the linux-kernel.def file.
+ a. When rcu_assign_pointer() is passed NULL, the Linux
+ kernel provides no ordering, but LKMM models this
+ case as a store release.
+
+ b. The "unless" RMW operations are not currently modeled:
+ atomic_long_add_unless(), atomic_add_unless(),
+ atomic_inc_unless_negative(), and
+ atomic_dec_unless_positive(). These can be emulated
+ in litmus tests, for example, by using atomic_cmpxchg().
+
+ c. The call_rcu() function is not modeled. It can be
+ emulated in litmus tests by adding another process that
+ invokes synchronize_rcu() and the body of the callback
+ function, with (for example) a release-acquire from
+ the site of the emulated call_rcu() to the beginning
+ of the additional process.
+
+ d. The rcu_barrier() function is not modeled. It can be
+ emulated in litmus tests emulating call_rcu() via
+ (for example) a release-acquire from the end of each
+ additional call_rcu() process to the site of the
+ emulated rcu-barrier().
+
+ e. Sleepable RCU (SRCU) is not modeled. It can be
+ emulated, but perhaps not simply.
+
+ f. Reader-writer locking is not modeled. It can be
+ emulated in litmus tests using atomic read-modify-write
+ operations.
+
The "herd7" tool has some additional limitations of its own, apart from
the memory model:
@@ -204,3 +240,6 @@ the memory model:
Some of these limitations may be overcome in the future, but others are
more likely to be addressed by incorporating the Linux-kernel memory model
into other tools.
+
+Finally, please note that LKMM is subject to change as hardware, use cases,
+and compilers evolve.
--
2.17.1
From: Alan Stern <[email protected]>
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.
All the architectures supported by the Linux kernel (including RISC-V)
do provide this ordering for locks, albeit for varying reasons.
Therefore this patch changes the model in accordance with the
developers' wishes.
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Reviewed-by: Will Deacon <[email protected]>
Acked-by: Peter Zijlstra (Intel) <[email protected]>
---
.../Documentation/explanation.txt | 186 ++++++++++++++----
tools/memory-model/linux-kernel.cat | 8 +-
...ISA2+pooncelock+pooncelock+pombonce.litmus | 7 +-
3 files changed, 150 insertions(+), 51 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 0cbd1ef8f86d..35bff92cc773 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -28,7 +28,8 @@ Explanation of the Linux-Kernel Memory Consistency Model
20. THE HAPPENS-BEFORE RELATION: hb
21. THE PROPAGATES-BEFORE RELATION: pb
22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
- 23. ODDS AND ENDS
+ 23. LOCKING
+ 24. ODDS AND ENDS
@@ -1067,28 +1068,6 @@ allowing out-of-order writes like this to occur. The model avoided
violating the write-write coherence rule by requiring the CPU not to
send the W write to the memory subsystem at all!)
-There is one last example of preserved program order in the LKMM: when
-a load-acquire reads from an earlier store-release. For example:
-
- smp_store_release(&x, 123);
- r1 = smp_load_acquire(&x);
-
-If the smp_load_acquire() ends up obtaining the 123 value that was
-stored by the smp_store_release(), the LKMM says that the load must be
-executed after the store; the store cannot be forwarded to the load.
-This requirement does not arise from the operational model, but it
-yields correct predictions on all architectures supported by the Linux
-kernel, although for differing reasons.
-
-On some architectures, including x86 and ARMv8, it is true that the
-store cannot be forwarded to the load. On others, including PowerPC
-and ARMv7, smp_store_release() generates object code that starts with
-a fence and smp_load_acquire() generates object code that ends with a
-fence. The upshot is that even though the store may be forwarded to
-the load, it is still true that any instruction preceding the store
-will be executed before the load or any following instructions, and
-the store will be executed before any instruction following the load.
-
AND THEN THERE WAS ALPHA
------------------------
@@ -1766,6 +1745,147 @@ before it does, and the critical section in P2 both starts after P1's
grace period does and ends after it does.
+LOCKING
+-------
+
+The LKMM includes locking. In fact, there is special code for locking
+in the formal model, added in order to make tools run faster.
+However, this special code is intended to be more or less equivalent
+to concepts we have already covered. A spinlock_t variable is treated
+the same as an int, and spin_lock(&s) is treated almost the same as:
+
+ while (cmpxchg_acquire(&s, 0, 1) != 0)
+ cpu_relax();
+
+This waits until s is equal to 0 and then atomically sets it to 1,
+and the read part of the cmpxchg operation acts as an acquire fence.
+An alternate way to express the same thing would be:
+
+ r = xchg_acquire(&s, 1);
+
+along with a requirement that at the end, r = 0. Similarly,
+spin_trylock(&s) is treated almost the same as:
+
+ return !cmpxchg_acquire(&s, 0, 1);
+
+which atomically sets s to 1 if it is currently equal to 0 and returns
+true if it succeeds (the read part of the cmpxchg operation acts as an
+acquire fence only if the operation is successful). spin_unlock(&s)
+is treated almost the same as:
+
+ smp_store_release(&s, 0);
+
+The "almost" qualifiers above need some explanation. In the LKMM, the
+store-release in a spin_unlock() and the load-acquire which forms the
+first half of the atomic rmw update in a spin_lock() or a successful
+spin_trylock() -- we can call these things lock-releases and
+lock-acquires -- have two properties beyond those of ordinary releases
+and acquires.
+
+First, when a lock-acquire reads from a lock-release, the LKMM
+requires that every instruction po-before the lock-release must
+execute before any instruction po-after the lock-acquire. This would
+naturally hold if the release and acquire operations were on different
+CPUs, but the LKMM says it holds even when they are on the same CPU.
+For example:
+
+ int x, y;
+ spinlock_t s;
+
+ P0()
+ {
+ int r1, r2;
+
+ spin_lock(&s);
+ r1 = READ_ONCE(x);
+ spin_unlock(&s);
+ spin_lock(&s);
+ r2 = READ_ONCE(y);
+ spin_unlock(&s);
+ }
+
+ P1()
+ {
+ WRITE_ONCE(y, 1);
+ smp_wmb();
+ WRITE_ONCE(x, 1);
+ }
+
+Here the second spin_lock() reads from the first spin_unlock(), and
+therefore the load of x must execute before the load of y. Thus we
+cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
+MP pattern).
+
+This requirement does not apply to ordinary release and acquire
+fences, only to lock-related operations. For instance, suppose P0()
+in the example had been written as:
+
+ P0()
+ {
+ int r1, r2, r3;
+
+ r1 = READ_ONCE(x);
+ smp_store_release(&s, 1);
+ r3 = smp_load_acquire(&s);
+ r2 = READ_ONCE(y);
+ }
+
+Then the CPU would be allowed to forward the s = 1 value from the
+smp_store_release() to the smp_load_acquire(), executing the
+instructions in the following order:
+
+ r3 = smp_load_acquire(&s); // Obtains r3 = 1
+ r2 = READ_ONCE(y);
+ r1 = READ_ONCE(x);
+ smp_store_release(&s, 1); // Value is forwarded
+
+and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
+
+Second, when a lock-acquire reads from a lock-release, and some other
+stores W and W' occur po-before the lock-release and po-after the
+lock-acquire respectively, the LKMM requires that W must propagate to
+each CPU before W' does. For example, consider:
+
+ int x, y;
+ spinlock_t x;
+
+ P0()
+ {
+ spin_lock(&s);
+ WRITE_ONCE(x, 1);
+ spin_unlock(&s);
+ }
+
+ P1()
+ {
+ int r1;
+
+ spin_lock(&s);
+ r1 = READ_ONCE(x);
+ WRITE_ONCE(y, 1);
+ spin_unlock(&s);
+ }
+
+ P2()
+ {
+ int r2, r3;
+
+ r2 = READ_ONCE(y);
+ smp_rmb();
+ r3 = READ_ONCE(x);
+ }
+
+If r1 = 1 at the end then the spin_lock() in P1 must have read from
+the spin_unlock() in P0. Hence the store to x must propagate to P2
+before the store to y does, so we cannot have r2 = 1 and r3 = 0.
+
+These two special requirements for lock-release and lock-acquire do
+not arise from the operational model. Nevertheless, kernel developers
+have come to expect and rely on them because they do hold on all
+architectures supported by the Linux kernel, albeit for various
+differing reasons.
+
+
ODDS AND ENDS
-------------
@@ -1831,26 +1951,6 @@ they behave as follows:
events and the events preceding them against all po-later
events.
-The LKMM includes locking. In fact, there is special code for locking
-in the formal model, added in order to make tools run faster.
-However, this special code is intended to be exactly equivalent to
-concepts we have already covered. A spinlock_t variable is treated
-the same as an int, and spin_lock(&s) is treated the same as:
-
- while (cmpxchg_acquire(&s, 0, 1) != 0)
- cpu_relax();
-
-which waits until s is equal to 0 and then atomically sets it to 1,
-and where the read part of the atomic update is also an acquire fence.
-An alternate way to express the same thing would be:
-
- r = xchg_acquire(&s, 1);
-
-along with a requirement that at the end, r = 0. spin_unlock(&s) is
-treated the same as:
-
- smp_store_release(&s, 0);
-
Interestingly, RCU and locking each introduce the possibility of
deadlock. When faced with code sequences such as:
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 59b5cbe6b624..882fc33274ac 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -38,7 +38,7 @@ let strong-fence = mb | gp
(* Release Acquire *)
let acq-po = [Acquire] ; po ; [M]
let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
(**********************************)
(* Fundamental coherence ordering *)
@@ -60,13 +60,13 @@ let dep = addr | data
let rwdep = (dep | ctrl) ; [W]
let overwrite = co | fr
let to-w = rwdep | (overwrite & int)
-let to-r = addr | (dep ; rfi) | rfi-rel-acq
+let to-r = addr | (dep ; rfi)
let fence = strong-fence | wmb | po-rel | rmb | acq-po
-let ppo = to-r | to-w | fence
+let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
(* Propagation: Ordering from release operations and strong fences. *)
let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po
let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
(*
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 0f749e419b34..094d58df7789 100644
--- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
+++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -1,11 +1,10 @@
C ISA2+pooncelock+pooncelock+pombonce
(*
- * Result: Sometimes
+ * Result: Never
*
- * This test shows that the ordering provided by a lock-protected S
- * litmus test (P0() and P1()) are not visible to external process P2().
- * This is likely to change soon.
+ * This test shows that write-write ordering provided by locks
+ * (in P0() and P1()) is visible to external process P2().
*)
{}
--
2.17.1
This commit adds s390.cat and s390.cfg files to allow users to check
litmus tests for s390-specific code. Note that this change only enables
herd7 checking of C-language litmus tests. Larger changes are required
to enable the litmus7 and klitmus7 tools to check litmus tests on real
hardare.
Suggested-by: Martin Schwidefsky <[email protected]>
Suggested-by: Christian Borntraeger <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
[ paulmck: Add fixes suggested by Alan Stern. ]
---
tools/memory-model/s390.cat | 18 ++++++++++++++++++
tools/memory-model/s390.cfg | 21 +++++++++++++++++++++
2 files changed, 39 insertions(+)
create mode 100644 tools/memory-model/s390.cat
create mode 100644 tools/memory-model/s390.cfg
diff --git a/tools/memory-model/s390.cat b/tools/memory-model/s390.cat
new file mode 100644
index 000000000000..216bf33d3ffe
--- /dev/null
+++ b/tools/memory-model/s390.cat
@@ -0,0 +1,18 @@
+s390
+
+include "fences.cat"
+include "cos.cat"
+
+(* Fundamental coherence ordering *)
+let com = rf | co | fr
+acyclic po-loc | com as coherence
+
+(* Atomic *)
+empty rmw & (fre;coe) as atom
+
+(* Fences *)
+let mb = [M] ; fencerel(Mb) ; [M]
+
+(* TSO with multicopy atomicity (tso-mca) *)
+let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W])
+acyclic mb | po-ghb | fr | rf | co as tso-mca
diff --git a/tools/memory-model/s390.cfg b/tools/memory-model/s390.cfg
new file mode 100644
index 000000000000..d77e05d2395c
--- /dev/null
+++ b/tools/memory-model/s390.cfg
@@ -0,0 +1,21 @@
+macros linux-kernel.def
+bell linux-kernel.bell
+model s390.cat
+graph columns
+squished true
+showevents noregs
+movelabel true
+fontsize 8
+xscale 2.0
+yscale 1.5
+arrowsize 0.8
+showinitrf false
+showfinalrf false
+showinitwrites false
+splines spline
+pad 0.1
+edgeattr hb,color,indigo
+edgeattr co,color,blue
+edgeattr mb,color,darkgreen
+edgeattr wmb,color,darkgreen
+edgeattr rmb,color,darkgreen
--
2.17.1
From: SeongJae Park <[email protected]>
This commit fixes a duplicate-"the" typo in README.
Signed-off-by: SeongJae Park <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Alan Stern <[email protected]>
---
tools/memory-model/Documentation/recipes.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt
index af72700cc20a..7fe8d7aa3029 100644
--- a/tools/memory-model/Documentation/recipes.txt
+++ b/tools/memory-model/Documentation/recipes.txt
@@ -311,7 +311,7 @@ The smp_wmb() macro orders prior stores against later stores, and the
smp_rmb() macro orders prior loads against later loads. Therefore, if
the final value of r0 is 1, the final value of r1 must also be 1.
-The the xlog_state_switch_iclogs() function in fs/xfs/xfs_log.c contains
+The xlog_state_switch_iclogs() function in fs/xfs/xfs_log.c contains
the following write-side code fragment:
log->l_curr_block -= log->l_logBBsize;
--
2.17.1
On Wed, Aug 29, 2018 at 02:10:49PM -0700, Paul E. McKenney wrote:
> This commit adds more detail about compiler optimizations and
> not-yet-modeled Linux-kernel APIs.
>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> tools/memory-model/README | 39 +++++++++++++++++++++++++++++++++++++++
> 1 file changed, 39 insertions(+)
>
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index ee987ce20aae..acf9077cffaa 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -171,6 +171,12 @@ The Linux-kernel memory model has the following limitations:
> particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
> and "A WARNING" sections).
>
> + Note that this limitation in turn limits LKMM's ability to
> + accurately model address, control, and data dependencies.
> + For example, if the compiler can deduce the value of some variable
> + carrying a dependency, then the compiler can break that dependency
> + by substituting a constant of that value.
> +
> 2. Multiple access sizes for a single variable are not supported,
> and neither are misaligned or partially overlapping accesses.
>
> @@ -190,6 +196,36 @@ The Linux-kernel memory model has the following limitations:
> However, a substantial amount of support is provided for these
> operations, as shown in the linux-kernel.def file.
>
> + a. When rcu_assign_pointer() is passed NULL, the Linux
> + kernel provides no ordering, but LKMM models this
> + case as a store release.
> +
> + b. The "unless" RMW operations are not currently modeled:
> + atomic_long_add_unless(), atomic_add_unless(),
> + atomic_inc_unless_negative(), and
> + atomic_dec_unless_positive(). These can be emulated
> + in litmus tests, for example, by using atomic_cmpxchg().
There is a prototype atomic_add_unless(): with current herd7,
$ cat atomic_add_unless.litmus
C atomic_add_unless
{}
P0(atomic_t *u, atomic_t *v)
{
int r0;
int r1;
r0 = atomic_add_unless(u, 1, 2);
r1 = atomic_read(v);
}
P1(atomic_t *u, atomic_t *v)
{
int r0;
int r1;
r0 = atomic_add_unless(v, 1, 2);
r1 = atomic_read(u);
}
exists (0:r1=0 /\ 1:r1=0)
$ herd7 -conf linux-kernel.cfg atomic_add_unless.litmus
Test atomic_add_unless Allowed
States 3
0:r1=0; 1:r1=1;
0:r1=1; 1:r1=0;
0:r1=1; 1:r1=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r1=0 /\ 1:r1=0)
Observation atomic_add_unless Never 0 3
Time atomic_add_unless 0.00
Hash=fa37a2359831690299e4cc394e45d966
The last commit in the herdtools7 repo. related to this implementation
(AFAICT) is:
9523c340917b6a ("herd/linux: make atomic_add_unless a primitive, so as to yield more precise dependencies for the returned boolean.")
but I can only vaguely remember those dependencies issues now :/ ...;
maybe we can now solve these issues? or should we change herd7 to re-
turn a warning? (Notice that this primitive is currently not exported
to the linux-kernel.def file.)
Andrea
> +
> + c. The call_rcu() function is not modeled. It can be
> + emulated in litmus tests by adding another process that
> + invokes synchronize_rcu() and the body of the callback
> + function, with (for example) a release-acquire from
> + the site of the emulated call_rcu() to the beginning
> + of the additional process.
> +
> + d. The rcu_barrier() function is not modeled. It can be
> + emulated in litmus tests emulating call_rcu() via
> + (for example) a release-acquire from the end of each
> + additional call_rcu() process to the site of the
> + emulated rcu-barrier().
> +
> + e. Sleepable RCU (SRCU) is not modeled. It can be
> + emulated, but perhaps not simply.
> +
> + f. Reader-writer locking is not modeled. It can be
> + emulated in litmus tests using atomic read-modify-write
> + operations.
> +
> The "herd7" tool has some additional limitations of its own, apart from
> the memory model:
>
> @@ -204,3 +240,6 @@ the memory model:
> Some of these limitations may be overcome in the future, but others are
> more likely to be addressed by incorporating the Linux-kernel memory model
> into other tools.
> +
> +Finally, please note that LKMM is subject to change as hardware, use cases,
> +and compilers evolve.
> --
> 2.17.1
>
On Wed, Aug 29, 2018 at 02:10:47PM -0700, Paul E. McKenney wrote:
> From: Alan Stern <[email protected]>
>
> 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.
>
> All the architectures supported by the Linux kernel (including RISC-V)
> do provide this ordering for locks, albeit for varying reasons.
> Therefore this patch changes the model in accordance with the
> developers' wishes.
>
> Signed-off-by: Alan Stern <[email protected]>
> Signed-off-by: Paul E. McKenney <[email protected]>
> Reviewed-by: Will Deacon <[email protected]>
> Acked-by: Peter Zijlstra (Intel) <[email protected]>
Round 2 ;-), I guess... Let me start from the uncontroversial points:
1) being able to use the LKMM to reason about generic locking code
is useful and desirable (paraphrasing Peter in [1]);
2) strengthening the ordering requirements of such code isn't going
to boost performance (that's "real maths").
This patch is taking (1) away from us and it is formalizing (2), with
almost _no_ reason (no reason at all, if we stick to the commit msg.).
In [2], Will wrote:
"[...] having them [the RMWs] closer to RCsc[/to the semantics of
locks] would make it easier to implement and reason about generic
locking implementations (i.e. reduce the number of special ordering
cases and/or magic barrier macros)"
"magic barrier macros" as in "mmh, if we accept this patch, we _should_
be auditing the various implementations/code to decide where to place a
smp_barrier_promote_ordinary_release_acquire_to_unlock_lock()" ;-)
or the like, and "special ordering cases" as in "arrgh, (otherwise) we
are forced to reason on a per-arch basis while looking at generic code".
(Remark: ordinary release/acquire are building blocks for code such as
qspinlock, (q)rwlock, mutex, rwsem, ... and what else??).
To avoid further repetition, I conclude by confirming all the concerns
and my assessment of this patch as pointed out in [3]; the subsequent
discussion, although not conclusive, presented several suggestions for
improvement (IMO).
Andrea
[1] http://lkml.kernel.org/r/[email protected]
[2] http://lkml.kernel.org/r/[email protected]
[3] http://lkml.kernel.org/r/20180710093821.GA5414@andrea
http://lkml.kernel.org/r/20180711161717.GA14635@andrea
> ---
> .../Documentation/explanation.txt | 186 ++++++++++++++----
> tools/memory-model/linux-kernel.cat | 8 +-
> ...ISA2+pooncelock+pooncelock+pombonce.litmus | 7 +-
> 3 files changed, 150 insertions(+), 51 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 0cbd1ef8f86d..35bff92cc773 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -28,7 +28,8 @@ Explanation of the Linux-Kernel Memory Consistency Model
> 20. THE HAPPENS-BEFORE RELATION: hb
> 21. THE PROPAGATES-BEFORE RELATION: pb
> 22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
> - 23. ODDS AND ENDS
> + 23. LOCKING
> + 24. ODDS AND ENDS
>
>
>
> @@ -1067,28 +1068,6 @@ allowing out-of-order writes like this to occur. The model avoided
> violating the write-write coherence rule by requiring the CPU not to
> send the W write to the memory subsystem at all!)
>
> -There is one last example of preserved program order in the LKMM: when
> -a load-acquire reads from an earlier store-release. For example:
> -
> - smp_store_release(&x, 123);
> - r1 = smp_load_acquire(&x);
> -
> -If the smp_load_acquire() ends up obtaining the 123 value that was
> -stored by the smp_store_release(), the LKMM says that the load must be
> -executed after the store; the store cannot be forwarded to the load.
> -This requirement does not arise from the operational model, but it
> -yields correct predictions on all architectures supported by the Linux
> -kernel, although for differing reasons.
> -
> -On some architectures, including x86 and ARMv8, it is true that the
> -store cannot be forwarded to the load. On others, including PowerPC
> -and ARMv7, smp_store_release() generates object code that starts with
> -a fence and smp_load_acquire() generates object code that ends with a
> -fence. The upshot is that even though the store may be forwarded to
> -the load, it is still true that any instruction preceding the store
> -will be executed before the load or any following instructions, and
> -the store will be executed before any instruction following the load.
> -
>
> AND THEN THERE WAS ALPHA
> ------------------------
> @@ -1766,6 +1745,147 @@ before it does, and the critical section in P2 both starts after P1's
> grace period does and ends after it does.
>
>
> +LOCKING
> +-------
> +
> +The LKMM includes locking. In fact, there is special code for locking
> +in the formal model, added in order to make tools run faster.
> +However, this special code is intended to be more or less equivalent
> +to concepts we have already covered. A spinlock_t variable is treated
> +the same as an int, and spin_lock(&s) is treated almost the same as:
> +
> + while (cmpxchg_acquire(&s, 0, 1) != 0)
> + cpu_relax();
> +
> +This waits until s is equal to 0 and then atomically sets it to 1,
> +and the read part of the cmpxchg operation acts as an acquire fence.
> +An alternate way to express the same thing would be:
> +
> + r = xchg_acquire(&s, 1);
> +
> +along with a requirement that at the end, r = 0. Similarly,
> +spin_trylock(&s) is treated almost the same as:
> +
> + return !cmpxchg_acquire(&s, 0, 1);
> +
> +which atomically sets s to 1 if it is currently equal to 0 and returns
> +true if it succeeds (the read part of the cmpxchg operation acts as an
> +acquire fence only if the operation is successful). spin_unlock(&s)
> +is treated almost the same as:
> +
> + smp_store_release(&s, 0);
> +
> +The "almost" qualifiers above need some explanation. In the LKMM, the
> +store-release in a spin_unlock() and the load-acquire which forms the
> +first half of the atomic rmw update in a spin_lock() or a successful
> +spin_trylock() -- we can call these things lock-releases and
> +lock-acquires -- have two properties beyond those of ordinary releases
> +and acquires.
> +
> +First, when a lock-acquire reads from a lock-release, the LKMM
> +requires that every instruction po-before the lock-release must
> +execute before any instruction po-after the lock-acquire. This would
> +naturally hold if the release and acquire operations were on different
> +CPUs, but the LKMM says it holds even when they are on the same CPU.
> +For example:
> +
> + int x, y;
> + spinlock_t s;
> +
> + P0()
> + {
> + int r1, r2;
> +
> + spin_lock(&s);
> + r1 = READ_ONCE(x);
> + spin_unlock(&s);
> + spin_lock(&s);
> + r2 = READ_ONCE(y);
> + spin_unlock(&s);
> + }
> +
> + P1()
> + {
> + WRITE_ONCE(y, 1);
> + smp_wmb();
> + WRITE_ONCE(x, 1);
> + }
> +
> +Here the second spin_lock() reads from the first spin_unlock(), and
> +therefore the load of x must execute before the load of y. Thus we
> +cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
> +MP pattern).
> +
> +This requirement does not apply to ordinary release and acquire
> +fences, only to lock-related operations. For instance, suppose P0()
> +in the example had been written as:
> +
> + P0()
> + {
> + int r1, r2, r3;
> +
> + r1 = READ_ONCE(x);
> + smp_store_release(&s, 1);
> + r3 = smp_load_acquire(&s);
> + r2 = READ_ONCE(y);
> + }
> +
> +Then the CPU would be allowed to forward the s = 1 value from the
> +smp_store_release() to the smp_load_acquire(), executing the
> +instructions in the following order:
> +
> + r3 = smp_load_acquire(&s); // Obtains r3 = 1
> + r2 = READ_ONCE(y);
> + r1 = READ_ONCE(x);
> + smp_store_release(&s, 1); // Value is forwarded
> +
> +and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
> +
> +Second, when a lock-acquire reads from a lock-release, and some other
> +stores W and W' occur po-before the lock-release and po-after the
> +lock-acquire respectively, the LKMM requires that W must propagate to
> +each CPU before W' does. For example, consider:
> +
> + int x, y;
> + spinlock_t x;
> +
> + P0()
> + {
> + spin_lock(&s);
> + WRITE_ONCE(x, 1);
> + spin_unlock(&s);
> + }
> +
> + P1()
> + {
> + int r1;
> +
> + spin_lock(&s);
> + r1 = READ_ONCE(x);
> + WRITE_ONCE(y, 1);
> + spin_unlock(&s);
> + }
> +
> + P2()
> + {
> + int r2, r3;
> +
> + r2 = READ_ONCE(y);
> + smp_rmb();
> + r3 = READ_ONCE(x);
> + }
> +
> +If r1 = 1 at the end then the spin_lock() in P1 must have read from
> +the spin_unlock() in P0. Hence the store to x must propagate to P2
> +before the store to y does, so we cannot have r2 = 1 and r3 = 0.
> +
> +These two special requirements for lock-release and lock-acquire do
> +not arise from the operational model. Nevertheless, kernel developers
> +have come to expect and rely on them because they do hold on all
> +architectures supported by the Linux kernel, albeit for various
> +differing reasons.
> +
> +
> ODDS AND ENDS
> -------------
>
> @@ -1831,26 +1951,6 @@ they behave as follows:
> events and the events preceding them against all po-later
> events.
>
> -The LKMM includes locking. In fact, there is special code for locking
> -in the formal model, added in order to make tools run faster.
> -However, this special code is intended to be exactly equivalent to
> -concepts we have already covered. A spinlock_t variable is treated
> -the same as an int, and spin_lock(&s) is treated the same as:
> -
> - while (cmpxchg_acquire(&s, 0, 1) != 0)
> - cpu_relax();
> -
> -which waits until s is equal to 0 and then atomically sets it to 1,
> -and where the read part of the atomic update is also an acquire fence.
> -An alternate way to express the same thing would be:
> -
> - r = xchg_acquire(&s, 1);
> -
> -along with a requirement that at the end, r = 0. spin_unlock(&s) is
> -treated the same as:
> -
> - smp_store_release(&s, 0);
> -
> Interestingly, RCU and locking each introduce the possibility of
> deadlock. When faced with code sequences such as:
>
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 59b5cbe6b624..882fc33274ac 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -38,7 +38,7 @@ let strong-fence = mb | gp
> (* Release Acquire *)
> let acq-po = [Acquire] ; po ; [M]
> let po-rel = [M] ; po ; [Release]
> -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
> +let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
>
> (**********************************)
> (* Fundamental coherence ordering *)
> @@ -60,13 +60,13 @@ let dep = addr | data
> let rwdep = (dep | ctrl) ; [W]
> let overwrite = co | fr
> let to-w = rwdep | (overwrite & int)
> -let to-r = addr | (dep ; rfi) | rfi-rel-acq
> +let to-r = addr | (dep ; rfi)
> let fence = strong-fence | wmb | po-rel | rmb | acq-po
> -let ppo = to-r | to-w | fence
> +let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
>
> (* Propagation: Ordering from release operations and strong fences. *)
> let A-cumul(r) = rfe? ; r
> -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
> +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po
> let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
>
> (*
> 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 0f749e419b34..094d58df7789 100644
> --- a/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> +++ b/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -1,11 +1,10 @@
> C ISA2+pooncelock+pooncelock+pombonce
>
> (*
> - * Result: Sometimes
> + * Result: Never
> *
> - * This test shows that the ordering provided by a lock-protected S
> - * litmus test (P0() and P1()) are not visible to external process P2().
> - * This is likely to change soon.
> + * This test shows that write-write ordering provided by locks
> + * (in P0() and P1()) is visible to external process P2().
> *)
>
> {}
> --
> 2.17.1
>
On Thu, 30 Aug 2018, Andrea Parri wrote:
> > All the architectures supported by the Linux kernel (including RISC-V)
> > do provide this ordering for locks, albeit for varying reasons.
> > Therefore this patch changes the model in accordance with the
> > developers' wishes.
> >
> > Signed-off-by: Alan Stern <[email protected]>
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > Reviewed-by: Will Deacon <[email protected]>
> > Acked-by: Peter Zijlstra (Intel) <[email protected]>
>
> Round 2 ;-), I guess... Let me start from the uncontroversial points:
>
> 1) being able to use the LKMM to reason about generic locking code
> is useful and desirable (paraphrasing Peter in [1]);
>
> 2) strengthening the ordering requirements of such code isn't going
> to boost performance (that's "real maths").
>
> This patch is taking (1) away from us and it is formalizing (2), with
> almost _no_ reason (no reason at all, if we stick to the commit msg.).
That's not quite fair. Generic code isn't always universally
applicable; some of it is opt-in -- meant only for the architectures
that can support it. In general, the LKMM allows us to reason about
higher abstractions (such as locking) at a higher level, without
necessarily being able to verify the architecture-specific details of
the implementations.
> In [2], Will wrote:
>
> "[...] having them [the RMWs] closer to RCsc[/to the semantics of
> locks] would make it easier to implement and reason about generic
> locking implementations (i.e. reduce the number of special ordering
> cases and/or magic barrier macros)"
>
> "magic barrier macros" as in "mmh, if we accept this patch, we _should_
> be auditing the various implementations/code to decide where to place a
>
> smp_barrier_promote_ordinary_release_acquire_to_unlock_lock()" ;-)
>
> or the like, and "special ordering cases" as in "arrgh, (otherwise) we
> are forced to reason on a per-arch basis while looking at generic code".
Currently the LKMM does not permit architecture-specific reasoning. It
would have to be extended (in a different way for each architecture)
first.
For example, one could use herd's POWER model combined with the POWER
compilation scheme and the POWER-specific implementation of spinlocks
for such reasoning. The LKMM alone is not sufficient.
Sure, programming and reasoning about the kernel would be easier if all
architectures were the same. Unfortunately, we (and the kernel) have
to live in the real world.
> (Remark: ordinary release/acquire are building blocks for code such as
> qspinlock, (q)rwlock, mutex, rwsem, ... and what else??).
But are these building blocks used the same way for all architectures?
> To avoid further repetition, I conclude by confirming all the concerns
> and my assessment of this patch as pointed out in [3]; the subsequent
> discussion, although not conclusive, presented several suggestions for
> improvement (IMO).
Alan
On Thu, Aug 30, 2018 at 11:17:13AM +0200, Andrea Parri wrote:
> On Wed, Aug 29, 2018 at 02:10:49PM -0700, Paul E. McKenney wrote:
> > This commit adds more detail about compiler optimizations and
> > not-yet-modeled Linux-kernel APIs.
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > tools/memory-model/README | 39 +++++++++++++++++++++++++++++++++++++++
> > 1 file changed, 39 insertions(+)
> >
> > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > index ee987ce20aae..acf9077cffaa 100644
> > --- a/tools/memory-model/README
> > +++ b/tools/memory-model/README
> > @@ -171,6 +171,12 @@ The Linux-kernel memory model has the following limitations:
> > particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
> > and "A WARNING" sections).
> >
> > + Note that this limitation in turn limits LKMM's ability to
> > + accurately model address, control, and data dependencies.
> > + For example, if the compiler can deduce the value of some variable
> > + carrying a dependency, then the compiler can break that dependency
> > + by substituting a constant of that value.
> > +
> > 2. Multiple access sizes for a single variable are not supported,
> > and neither are misaligned or partially overlapping accesses.
> >
> > @@ -190,6 +196,36 @@ The Linux-kernel memory model has the following limitations:
> > However, a substantial amount of support is provided for these
> > operations, as shown in the linux-kernel.def file.
> >
> > + a. When rcu_assign_pointer() is passed NULL, the Linux
> > + kernel provides no ordering, but LKMM models this
> > + case as a store release.
> > +
> > + b. The "unless" RMW operations are not currently modeled:
> > + atomic_long_add_unless(), atomic_add_unless(),
> > + atomic_inc_unless_negative(), and
> > + atomic_dec_unless_positive(). These can be emulated
> > + in litmus tests, for example, by using atomic_cmpxchg().
>
> There is a prototype atomic_add_unless(): with current herd7,
>
> $ cat atomic_add_unless.litmus
> C atomic_add_unless
>
> {}
>
> P0(atomic_t *u, atomic_t *v)
> {
> int r0;
> int r1;
>
> r0 = atomic_add_unless(u, 1, 2);
> r1 = atomic_read(v);
> }
>
> P1(atomic_t *u, atomic_t *v)
> {
> int r0;
> int r1;
>
> r0 = atomic_add_unless(v, 1, 2);
> r1 = atomic_read(u);
> }
>
> exists (0:r1=0 /\ 1:r1=0)
>
> $ herd7 -conf linux-kernel.cfg atomic_add_unless.litmus
> Test atomic_add_unless Allowed
> States 3
> 0:r1=0; 1:r1=1;
> 0:r1=1; 1:r1=0;
> 0:r1=1; 1:r1=1;
> No
> Witnesses
> Positive: 0 Negative: 3
> Condition exists (0:r1=0 /\ 1:r1=0)
> Observation atomic_add_unless Never 0 3
> Time atomic_add_unless 0.00
> Hash=fa37a2359831690299e4cc394e45d966
>
> The last commit in the herdtools7 repo. related to this implementation
> (AFAICT) is:
>
> 9523c340917b6a ("herd/linux: make atomic_add_unless a primitive, so as to yield more precise dependencies for the returned boolean.")
>
> but I can only vaguely remember those dependencies issues now :/ ...;
> maybe we can now solve these issues? or should we change herd7 to re-
> turn a warning? (Notice that this primitive is currently not exported
> to the linux-kernel.def file.)
Cool! It would be good to add this to the .def file once the underlying
herd7 machinery is ready. And then I would update the documentation
accordingly. Or happily accept a patch updating the documentation,
as the case might be. ;-)
Thanx, Paul
> Andrea
>
>
> > +
> > + c. The call_rcu() function is not modeled. It can be
> > + emulated in litmus tests by adding another process that
> > + invokes synchronize_rcu() and the body of the callback
> > + function, with (for example) a release-acquire from
> > + the site of the emulated call_rcu() to the beginning
> > + of the additional process.
> > +
> > + d. The rcu_barrier() function is not modeled. It can be
> > + emulated in litmus tests emulating call_rcu() via
> > + (for example) a release-acquire from the end of each
> > + additional call_rcu() process to the site of the
> > + emulated rcu-barrier().
> > +
> > + e. Sleepable RCU (SRCU) is not modeled. It can be
> > + emulated, but perhaps not simply.
> > +
> > + f. Reader-writer locking is not modeled. It can be
> > + emulated in litmus tests using atomic read-modify-write
> > + operations.
> > +
> > The "herd7" tool has some additional limitations of its own, apart from
> > the memory model:
> >
> > @@ -204,3 +240,6 @@ the memory model:
> > Some of these limitations may be overcome in the future, but others are
> > more likely to be addressed by incorporating the Linux-kernel memory model
> > into other tools.
> > +
> > +Finally, please note that LKMM is subject to change as hardware, use cases,
> > +and compilers evolve.
> > --
> > 2.17.1
> >
>
On Thu, Aug 30, 2018 at 05:31:32PM -0400, Alan Stern wrote:
> On Thu, 30 Aug 2018, Andrea Parri wrote:
>
> > > All the architectures supported by the Linux kernel (including RISC-V)
> > > do provide this ordering for locks, albeit for varying reasons.
> > > Therefore this patch changes the model in accordance with the
> > > developers' wishes.
> > >
> > > Signed-off-by: Alan Stern <[email protected]>
> > > Signed-off-by: Paul E. McKenney <[email protected]>
> > > Reviewed-by: Will Deacon <[email protected]>
> > > Acked-by: Peter Zijlstra (Intel) <[email protected]>
> >
> > Round 2 ;-), I guess... Let me start from the uncontroversial points:
> >
> > 1) being able to use the LKMM to reason about generic locking code
> > is useful and desirable (paraphrasing Peter in [1]);
> >
> > 2) strengthening the ordering requirements of such code isn't going
> > to boost performance (that's "real maths").
> >
> > This patch is taking (1) away from us and it is formalizing (2), with
> > almost _no_ reason (no reason at all, if we stick to the commit msg.).
>
> That's not quite fair. Generic code isn't always universally
> applicable; some of it is opt-in -- meant only for the architectures
> that can support it. In general, the LKMM allows us to reason about
> higher abstractions (such as locking) at a higher level, without
> necessarily being able to verify the architecture-specific details of
> the implementations.
No, generic code is "universally applicable" by definition; see below
for more on this point.
>
> > In [2], Will wrote:
> >
> > "[...] having them [the RMWs] closer to RCsc[/to the semantics of
> > locks] would make it easier to implement and reason about generic
> > locking implementations (i.e. reduce the number of special ordering
> > cases and/or magic barrier macros)"
> >
> > "magic barrier macros" as in "mmh, if we accept this patch, we _should_
> > be auditing the various implementations/code to decide where to place a
> >
> > smp_barrier_promote_ordinary_release_acquire_to_unlock_lock()" ;-)
> >
> > or the like, and "special ordering cases" as in "arrgh, (otherwise) we
> > are forced to reason on a per-arch basis while looking at generic code".
>
> Currently the LKMM does not permit architecture-specific reasoning. It
> would have to be extended (in a different way for each architecture)
> first.
Completely agreed; that's why I said that this patch is detrimental to
the applicability of the LKMM...
>
> For example, one could use herd's POWER model combined with the POWER
> compilation scheme and the POWER-specific implementation of spinlocks
> for such reasoning. The LKMM alone is not sufficient.
>
> Sure, programming and reasoning about the kernel would be easier if all
> architectures were the same. Unfortunately, we (and the kernel) have
> to live in the real world.
>
> > (Remark: ordinary release/acquire are building blocks for code such as
> > qspinlock, (q)rwlock, mutex, rwsem, ... and what else??).
>
> But are these building blocks used the same way for all architectures?
The more, the better! (because then we have the LKMM tools)
We already discussed the "fast path" example: the fast paths of the
above all resemble:
*_lock(s): atomic_cmpxchg_acquire(&s->val, UNLOCKED_VAL, LOCKED_VAL) ...
*_unlock(s): ... atomic_set_release(&s->val, UNLOCKED_VAL)
When I read this code, I think "Of course." (unless some arch. has
messed the implementation of cmpxchg_* up, which can happen...); but
then I read the subject line of this patch and I think "Wait, what?".
You can argue that this is not generic code, sure; but why on Earth
would you like to do so?!
Andrea
>
> > To avoid further repetition, I conclude by confirming all the concerns
> > and my assessment of this patch as pointed out in [3]; the subsequent
> > discussion, although not conclusive, presented several suggestions for
> > improvement (IMO).
>
> Alan
>
> > > + b. The "unless" RMW operations are not currently modeled:
> > > + atomic_long_add_unless(), atomic_add_unless(),
> > > + atomic_inc_unless_negative(), and
> > > + atomic_dec_unless_positive(). These can be emulated
> > > + in litmus tests, for example, by using atomic_cmpxchg().
> >
> > There is a prototype atomic_add_unless(): with current herd7,
> >
> > $ cat atomic_add_unless.litmus
> > C atomic_add_unless
> >
> > {}
> >
> > P0(atomic_t *u, atomic_t *v)
> > {
> > int r0;
> > int r1;
> >
> > r0 = atomic_add_unless(u, 1, 2);
> > r1 = atomic_read(v);
> > }
> >
> > P1(atomic_t *u, atomic_t *v)
> > {
> > int r0;
> > int r1;
> >
> > r0 = atomic_add_unless(v, 1, 2);
> > r1 = atomic_read(u);
> > }
> >
> > exists (0:r1=0 /\ 1:r1=0)
> >
> > $ herd7 -conf linux-kernel.cfg atomic_add_unless.litmus
> > Test atomic_add_unless Allowed
> > States 3
> > 0:r1=0; 1:r1=1;
> > 0:r1=1; 1:r1=0;
> > 0:r1=1; 1:r1=1;
> > No
> > Witnesses
> > Positive: 0 Negative: 3
> > Condition exists (0:r1=0 /\ 1:r1=0)
> > Observation atomic_add_unless Never 0 3
> > Time atomic_add_unless 0.00
> > Hash=fa37a2359831690299e4cc394e45d966
> >
> > The last commit in the herdtools7 repo. related to this implementation
> > (AFAICT) is:
> >
> > 9523c340917b6a ("herd/linux: make atomic_add_unless a primitive, so as to yield more precise dependencies for the returned boolean.")
> >
> > but I can only vaguely remember those dependencies issues now :/ ...;
> > maybe we can now solve these issues? or should we change herd7 to re-
> > turn a warning? (Notice that this primitive is currently not exported
> > to the linux-kernel.def file.)
>
> Cool! It would be good to add this to the .def file once the underlying
> herd7 machinery is ready. And then I would update the documentation
> accordingly. Or happily accept a patch updating the documentation,
> as the case might be. ;-)
Fair enough, ;-) Please feel free to add:
Reviewed-by: Andrea Parri <[email protected]>
Andrea
On Fri, 31 Aug 2018, Andrea Parri wrote:
> On Thu, Aug 30, 2018 at 05:31:32PM -0400, Alan Stern wrote:
> > On Thu, 30 Aug 2018, Andrea Parri wrote:
> >
> > > > All the architectures supported by the Linux kernel (including RISC-V)
> > > > do provide this ordering for locks, albeit for varying reasons.
> > > > Therefore this patch changes the model in accordance with the
> > > > developers' wishes.
> > > >
> > > > Signed-off-by: Alan Stern <[email protected]>
> > > > Signed-off-by: Paul E. McKenney <[email protected]>
> > > > Reviewed-by: Will Deacon <[email protected]>
> > > > Acked-by: Peter Zijlstra (Intel) <[email protected]>
> > >
> > > Round 2 ;-), I guess... Let me start from the uncontroversial points:
> > >
> > > 1) being able to use the LKMM to reason about generic locking code
> > > is useful and desirable (paraphrasing Peter in [1]);
> > >
> > > 2) strengthening the ordering requirements of such code isn't going
> > > to boost performance (that's "real maths").
> > >
> > > This patch is taking (1) away from us and it is formalizing (2), with
> > > almost _no_ reason (no reason at all, if we stick to the commit msg.).
> >
> > That's not quite fair. Generic code isn't always universally
> > applicable; some of it is opt-in -- meant only for the architectures
> > that can support it. In general, the LKMM allows us to reason about
> > higher abstractions (such as locking) at a higher level, without
> > necessarily being able to verify the architecture-specific details of
> > the implementations.
>
> No, generic code is "universally applicable" by definition; see below
> for more on this point.
Then perhaps we should be talking about "partially generic" code; i.e.,
code that applies to many but not all architectures.
> > > In [2], Will wrote:
> > >
> > > "[...] having them [the RMWs] closer to RCsc[/to the semantics of
> > > locks] would make it easier to implement and reason about generic
> > > locking implementations (i.e. reduce the number of special ordering
> > > cases and/or magic barrier macros)"
> > >
> > > "magic barrier macros" as in "mmh, if we accept this patch, we _should_
> > > be auditing the various implementations/code to decide where to place a
> > >
> > > smp_barrier_promote_ordinary_release_acquire_to_unlock_lock()" ;-)
> > >
> > > or the like, and "special ordering cases" as in "arrgh, (otherwise) we
> > > are forced to reason on a per-arch basis while looking at generic code".
> >
> > Currently the LKMM does not permit architecture-specific reasoning. It
> > would have to be extended (in a different way for each architecture)
> > first.
>
> Completely agreed; that's why I said that this patch is detrimental to
> the applicability of the LKMM...
This ignores the attitude of the kernel developers who want locking to
have the stronger RCtso semantics. From their point of view, the patch
enhances the LKMM's applicability.
> > For example, one could use herd's POWER model combined with the POWER
> > compilation scheme and the POWER-specific implementation of spinlocks
> > for such reasoning. The LKMM alone is not sufficient.
> >
> > Sure, programming and reasoning about the kernel would be easier if all
> > architectures were the same. Unfortunately, we (and the kernel) have
> > to live in the real world.
> >
> > > (Remark: ordinary release/acquire are building blocks for code such as
> > > qspinlock, (q)rwlock, mutex, rwsem, ... and what else??).
> >
> > But are these building blocks used the same way for all architectures?
>
> The more, the better! (because then we have the LKMM tools)
>
> We already discussed the "fast path" example: the fast paths of the
> above all resemble:
>
> *_lock(s): atomic_cmpxchg_acquire(&s->val, UNLOCKED_VAL, LOCKED_VAL) ...
> *_unlock(s): ... atomic_set_release(&s->val, UNLOCKED_VAL)
>
> When I read this code, I think "Of course." (unless some arch. has
> messed the implementation of cmpxchg_* up, which can happen...); but
> then I read the subject line of this patch and I think "Wait, what?".
>
> You can argue that this is not generic code, sure; but why on Earth
> would you like to do so?!
Because the code might not work! On RISC-V, for example, the
implementation of ordinary release/acquire is currently not as strong
as atomic release/acquire.
Yes, it's true that implementing locks with atomic_cmpxchg_acquire
should be correct on all existing architectures. And Paul has invited
a patch to modify the LKMM accordingly. If you feel that such a change
would be a useful enhancement to the LKMM's applicability, please write
it.
Alan
Hi Paul,
On Wed, Aug 29, 2018 at 02:10:53PM -0700, Paul E. McKenney wrote:
> This commit adds s390.cat and s390.cfg files to allow users to check
> litmus tests for s390-specific code. Note that this change only enables
> herd7 checking of C-language litmus tests. Larger changes are required
> to enable the litmus7 and klitmus7 tools to check litmus tests on real
> hardare.
>
> Suggested-by: Martin Schwidefsky <[email protected]>
> Suggested-by: Christian Borntraeger <[email protected]>
> Signed-off-by: Paul E. McKenney <[email protected]>
> [ paulmck: Add fixes suggested by Alan Stern. ]
> ---
> tools/memory-model/s390.cat | 18 ++++++++++++++++++
> tools/memory-model/s390.cfg | 21 +++++++++++++++++++++
> 2 files changed, 39 insertions(+)
> create mode 100644 tools/memory-model/s390.cat
> create mode 100644 tools/memory-model/s390.cfg
As I said before, I'd *much* prefer this to be part of the upstream
herdtools7 repository. It's not really anything to do with the Linux
kernel, so I don't think it belongs in the source tree.
Cheers,
Will
On Fri, Aug 31, 2018 at 10:52:54AM -0400, Alan Stern wrote:
> On Fri, 31 Aug 2018, Andrea Parri wrote:
> > On Thu, Aug 30, 2018 at 05:31:32PM -0400, Alan Stern wrote:
> > > On Thu, 30 Aug 2018, Andrea Parri wrote:
> > > > (Remark: ordinary release/acquire are building blocks for code such as
> > > > qspinlock, (q)rwlock, mutex, rwsem, ... and what else??).
> > >
> > > But are these building blocks used the same way for all architectures?
> >
> > The more, the better! (because then we have the LKMM tools)
> >
> > We already discussed the "fast path" example: the fast paths of the
> > above all resemble:
> >
> > *_lock(s): atomic_cmpxchg_acquire(&s->val, UNLOCKED_VAL, LOCKED_VAL) ...
> > *_unlock(s): ... atomic_set_release(&s->val, UNLOCKED_VAL)
> >
> > When I read this code, I think "Of course." (unless some arch. has
> > messed the implementation of cmpxchg_* up, which can happen...); but
> > then I read the subject line of this patch and I think "Wait, what?".
> >
> > You can argue that this is not generic code, sure; but why on Earth
> > would you like to do so?!
>
> Because the code might not work! On RISC-V, for example, the
> implementation of ordinary release/acquire is currently not as strong
> as atomic release/acquire.
>
> Yes, it's true that implementing locks with atomic_cmpxchg_acquire
> should be correct on all existing architectures. And Paul has invited
> a patch to modify the LKMM accordingly. If you feel that such a change
> would be a useful enhancement to the LKMM's applicability, please write
> it.
Yes, please! That would be the "RmW" discussion which Andrea partially
quoted earlier on, so getting that going independently from this patch
sounds like a great idea to me.
Cheers,
Will
On Fri, Aug 31, 2018 at 10:52:54AM -0400, Alan Stern wrote:
> On Fri, 31 Aug 2018, Andrea Parri wrote:
>
> > On Thu, Aug 30, 2018 at 05:31:32PM -0400, Alan Stern wrote:
> > > On Thu, 30 Aug 2018, Andrea Parri wrote:
> > >
> > > > > All the architectures supported by the Linux kernel (including RISC-V)
> > > > > do provide this ordering for locks, albeit for varying reasons.
> > > > > Therefore this patch changes the model in accordance with the
> > > > > developers' wishes.
> > > > >
> > > > > Signed-off-by: Alan Stern <[email protected]>
> > > > > Signed-off-by: Paul E. McKenney <[email protected]>
> > > > > Reviewed-by: Will Deacon <[email protected]>
> > > > > Acked-by: Peter Zijlstra (Intel) <[email protected]>
> > > >
> > > > Round 2 ;-), I guess... Let me start from the uncontroversial points:
> > > >
> > > > 1) being able to use the LKMM to reason about generic locking code
> > > > is useful and desirable (paraphrasing Peter in [1]);
> > > >
> > > > 2) strengthening the ordering requirements of such code isn't going
> > > > to boost performance (that's "real maths").
> > > >
> > > > This patch is taking (1) away from us and it is formalizing (2), with
> > > > almost _no_ reason (no reason at all, if we stick to the commit msg.).
> > >
> > > That's not quite fair. Generic code isn't always universally
> > > applicable; some of it is opt-in -- meant only for the architectures
> > > that can support it. In general, the LKMM allows us to reason about
> > > higher abstractions (such as locking) at a higher level, without
> > > necessarily being able to verify the architecture-specific details of
> > > the implementations.
> >
> > No, generic code is "universally applicable" by definition; see below
> > for more on this point.
>
> Then perhaps we should be talking about "partially generic" code; i.e.,
> code that applies to many but not all architectures.
Perhaps. I call this "non-generic". ;-)
>
> > > > In [2], Will wrote:
> > > >
> > > > "[...] having them [the RMWs] closer to RCsc[/to the semantics of
> > > > locks] would make it easier to implement and reason about generic
> > > > locking implementations (i.e. reduce the number of special ordering
> > > > cases and/or magic barrier macros)"
> > > >
> > > > "magic barrier macros" as in "mmh, if we accept this patch, we _should_
> > > > be auditing the various implementations/code to decide where to place a
> > > >
> > > > smp_barrier_promote_ordinary_release_acquire_to_unlock_lock()" ;-)
> > > >
> > > > or the like, and "special ordering cases" as in "arrgh, (otherwise) we
> > > > are forced to reason on a per-arch basis while looking at generic code".
> > >
> > > Currently the LKMM does not permit architecture-specific reasoning. It
> > > would have to be extended (in a different way for each architecture)
> > > first.
> >
> > Completely agreed; that's why I said that this patch is detrimental to
> > the applicability of the LKMM...
>
> This ignores the attitude of the kernel developers who want locking to
> have the stronger RCtso semantics. From their point of view, the patch
> enhances the LKMM's applicability.
Please stop. We spent weeks discussing how to make such a transition
properly, and I suggested ways to do this above and in other threads.
(Again, your commit message says nothing about that "enhancement"...)
>
> > > For example, one could use herd's POWER model combined with the POWER
> > > compilation scheme and the POWER-specific implementation of spinlocks
> > > for such reasoning. The LKMM alone is not sufficient.
> > >
> > > Sure, programming and reasoning about the kernel would be easier if all
> > > architectures were the same. Unfortunately, we (and the kernel) have
> > > to live in the real world.
> > >
> > > > (Remark: ordinary release/acquire are building blocks for code such as
> > > > qspinlock, (q)rwlock, mutex, rwsem, ... and what else??).
> > >
> > > But are these building blocks used the same way for all architectures?
> >
> > The more, the better! (because then we have the LKMM tools)
> >
> > We already discussed the "fast path" example: the fast paths of the
> > above all resemble:
> >
> > *_lock(s): atomic_cmpxchg_acquire(&s->val, UNLOCKED_VAL, LOCKED_VAL) ...
> > *_unlock(s): ... atomic_set_release(&s->val, UNLOCKED_VAL)
> >
> > When I read this code, I think "Of course." (unless some arch. has
> > messed the implementation of cmpxchg_* up, which can happen...); but
> > then I read the subject line of this patch and I think "Wait, what?".
> >
> > You can argue that this is not generic code, sure; but why on Earth
> > would you like to do so?!
>
> Because the code might not work! On RISC-V, for example, the
> implementation of ordinary release/acquire is currently not as strong
> as atomic release/acquire.
No doubt it "might not work". ;-) Concerning the RISC-V implementation,
I almost (re)did that, so at least you know who to blame if what you are
saying turned out to be correct.
>
> Yes, it's true that implementing locks with atomic_cmpxchg_acquire
> should be correct on all existing architectures. And Paul has invited
> a patch to modify the LKMM accordingly. If you feel that such a change
> would be a useful enhancement to the LKMM's applicability, please write
> it.
Hey, it's your patch that is introducing concerns! "my patch" would
partially _but_ substantially revert yours (see earlier discussions):
I'm still hoping that we'll be able to find an agreement...
Andrea
>
> Alan
>
> > Yes, it's true that implementing locks with atomic_cmpxchg_acquire
> > should be correct on all existing architectures. And Paul has invited
> > a patch to modify the LKMM accordingly. If you feel that such a change
> > would be a useful enhancement to the LKMM's applicability, please write
> > it.
>
> Yes, please! That would be the "RmW" discussion which Andrea partially
> quoted earlier on, so getting that going independently from this patch
> sounds like a great idea to me.
That was indeed one of the proposal we discussed. As you recalled, that
proposal only covered RmWs load-acquire (and ordinary store-release); in
particular, I realized that comments such as:
"The atomic_cond_read_acquire() call above has provided the
necessary acquire semantics required for locking."
[from kernel/locking/qspinlock.c]
(for example) would still _not have "generic validity" _if we added the
above po-unlock-rf-lock-po term... (which, again, makes me somehow uncon-
fortable); Would to have _all_ the acquire be admissible for you?
Andrea
>
> Cheers,
>
> Will
On Fri, Aug 31, 2018 at 05:06:30PM +0100, Will Deacon wrote:
> Hi Paul,
>
> On Wed, Aug 29, 2018 at 02:10:53PM -0700, Paul E. McKenney wrote:
> > This commit adds s390.cat and s390.cfg files to allow users to check
> > litmus tests for s390-specific code. Note that this change only enables
> > herd7 checking of C-language litmus tests. Larger changes are required
> > to enable the litmus7 and klitmus7 tools to check litmus tests on real
> > hardare.
> >
> > Suggested-by: Martin Schwidefsky <[email protected]>
> > Suggested-by: Christian Borntraeger <[email protected]>
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > [ paulmck: Add fixes suggested by Alan Stern. ]
> > ---
> > tools/memory-model/s390.cat | 18 ++++++++++++++++++
> > tools/memory-model/s390.cfg | 21 +++++++++++++++++++++
> > 2 files changed, 39 insertions(+)
> > create mode 100644 tools/memory-model/s390.cat
> > create mode 100644 tools/memory-model/s390.cfg
>
> As I said before, I'd *much* prefer this to be part of the upstream
> herdtools7 repository. It's not really anything to do with the Linux
> kernel, so I don't think it belongs in the source tree.
Agreed. As the cover letter says, "Add .cfg and .cat files for s390,
which is a not-for-mainline placeholder."
Thanx, Paul
On Fri, Aug 31, 2018 at 08:28:46PM +0200, Andrea Parri wrote:
> > > Yes, it's true that implementing locks with atomic_cmpxchg_acquire
> > > should be correct on all existing architectures. And Paul has invited
> > > a patch to modify the LKMM accordingly. If you feel that such a change
> > > would be a useful enhancement to the LKMM's applicability, please write
> > > it.
> >
> > Yes, please! That would be the "RmW" discussion which Andrea partially
> > quoted earlier on, so getting that going independently from this patch
> > sounds like a great idea to me.
>
> That was indeed one of the proposal we discussed. As you recalled, that
> proposal only covered RmWs load-acquire (and ordinary store-release); in
> particular, I realized that comments such as:
>
> "The atomic_cond_read_acquire() call above has provided the
> necessary acquire semantics required for locking."
>
> [from kernel/locking/qspinlock.c]
>
> (for example) would still _not have "generic validity" _if we added the
> above po-unlock-rf-lock-po term... (which, again, makes me somehow uncon-
> fortable); Would to have _all_ the acquire be admissible for you?
In Cat speak,
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 59b5cbe6b6240..fd9c0831adf0a 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -38,7 +38,7 @@ let strong-fence = mb | gp
(* Release Acquire *)
let acq-po = [Acquire] ; po ; [M]
let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let po-rel-rf-acq-po = po ; [Release] ; rf ; [Acquire] ; po
(**********************************)
(* Fundamental coherence ordering *)
@@ -60,13 +60,13 @@ let dep = addr | data
let rwdep = (dep | ctrl) ; [W]
let overwrite = co | fr
let to-w = rwdep | (overwrite & int)
-let to-r = addr | (dep ; rfi) | rfi-rel-acq
+let to-r = addr | (dep ; rfi)
let fence = strong-fence | wmb | po-rel | rmb | acq-po
-let ppo = to-r | to-w | fence
+let ppo = to-r | to-w | fence | (po-rel-rf-acq-po & int)
(* Propagation: Ordering from release operations and strong fences. *)
let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-rel-rf-acq-po
let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
(*
I take this opportunity to summarize my viewpoint on these matters:
Someone would have to write the commit message for the above diff ...
that is, to describe -why- we should go RCtso (and update the documen-
tation accordingly); by now, the only argument for this appears to be:
"(most) people expect strong ordering" _and they will be "lazy enough"
to not check their expectations by using the LKMM tool (paraphrasing
from [1]); IAC, Linux "might work" better if we add this ordering to
the LKMM. Agreeing on such an approach would mean agreeing that this
argument "wins" over:
"We want new architectures to implement acquire/release efficiently,
and it's not unlikely that they will have acquire loads that are
similar in semantics to LDAPR." [2]
"RISC-V probably would have been RCpc [...] it takes extra fences
to go from RCpc to either "RCtso" or RCsc." [3]
(or similar instances) since, of course, there is no such thing as a
"free strong ordering"; and I'm not only talking about "efficiency",
I'm also thinking at the fact that someone will have to maintain that
ordering across all the architectures and in the LKMM.
If, OTOH, we agree that the above "win"/assumption is valid only for
locks or, in other/better words, if we agree that we should maintain
_two_ distinct release-acquire orderings (a first one for unlock-lock
sequences and a second one for ordinary/atomic release-acquire, say,
as proposed in the patch under RFC), I ask that we audit and modify
the generic code accordingly/as suggested in other posts _before_ we
upstream the changes for the LKMM: we should identify those places
where (the newly introduced) _gap_ between unlock-lock and the other
release-acquire is not admissible and fix those places (notice that
this entails, in part., agreeing on what/where the generic code is).
Finally, if we don't agree with the above assumption at all (that is,
no matter if we are considering unlock-lock or other release-acquire
sequences), then we should go RCpc [4].
I described three different approaches (which are NOT "independent",
clearly; let us find an agreement...); even though some of them look
insane to me, I'm currently open to all of them: thoughts?
Andrea
[1] http://lkml.kernel.org/r/[email protected]
http://lkml.kernel.org/r/CA+55aFwKpkU5C23OYt1HCiD3X5bJHVh1jz5G2dSnF1+kVrOCTA@mail.gmail.com
[2] http://lkml.kernel.org/r/[email protected]
[3] http://lkml.kernel.org/r/[email protected]
[4] http://lkml.kernel.org/r/20180711123421.GA9673@andrea
http://lkml.kernel.org/r/[email protected]
On Fri, Aug 31, 2018 at 08:28:46PM +0200, Andrea Parri wrote:
> > > Yes, it's true that implementing locks with atomic_cmpxchg_acquire
> > > should be correct on all existing architectures. And Paul has invited
> > > a patch to modify the LKMM accordingly. If you feel that such a change
> > > would be a useful enhancement to the LKMM's applicability, please write
> > > it.
> >
> > Yes, please! That would be the "RmW" discussion which Andrea partially
> > quoted earlier on, so getting that going independently from this patch
> > sounds like a great idea to me.
>
> That was indeed one of the proposal we discussed. As you recalled, that
> proposal only covered RmWs load-acquire (and ordinary store-release); in
> particular, I realized that comments such as:
>
> "The atomic_cond_read_acquire() call above has provided the
> necessary acquire semantics required for locking."
>
> [from kernel/locking/qspinlock.c]
>
> (for example) would still _not have "generic validity" _if we added the
> above po-unlock-rf-lock-po term... (which, again, makes me somehow uncon-
> fortable); Would to have _all_ the acquire be admissible for you?
I think you've missed some words here, but if you're asking if I'd be
ok strengthening all acquire operations, then the answer is no. See the
huge amount of previous discussion.
Will
Andrea,
On Mon, Sep 03, 2018 at 11:01:53AM +0200, Andrea Parri wrote:
> On Fri, Aug 31, 2018 at 08:28:46PM +0200, Andrea Parri wrote:
> > > > Yes, it's true that implementing locks with atomic_cmpxchg_acquire
> > > > should be correct on all existing architectures. And Paul has invited
> > > > a patch to modify the LKMM accordingly. If you feel that such a change
> > > > would be a useful enhancement to the LKMM's applicability, please write
> > > > it.
> > >
> > > Yes, please! That would be the "RmW" discussion which Andrea partially
> > > quoted earlier on, so getting that going independently from this patch
> > > sounds like a great idea to me.
> >
> > That was indeed one of the proposal we discussed. As you recalled, that
> > proposal only covered RmWs load-acquire (and ordinary store-release); in
> > particular, I realized that comments such as:
> >
> > "The atomic_cond_read_acquire() call above has provided the
> > necessary acquire semantics required for locking."
> >
> > [from kernel/locking/qspinlock.c]
> >
> > (for example) would still _not have "generic validity" _if we added the
> > above po-unlock-rf-lock-po term... (which, again, makes me somehow uncon-
> > fortable); Would to have _all_ the acquire be admissible for you?
>
> In Cat speak,
>
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 59b5cbe6b6240..fd9c0831adf0a 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -38,7 +38,7 @@ let strong-fence = mb | gp
> (* Release Acquire *)
> let acq-po = [Acquire] ; po ; [M]
> let po-rel = [M] ; po ; [Release]
> -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
> +let po-rel-rf-acq-po = po ; [Release] ; rf ; [Acquire] ; po
>
> (**********************************)
> (* Fundamental coherence ordering *)
> @@ -60,13 +60,13 @@ let dep = addr | data
> let rwdep = (dep | ctrl) ; [W]
> let overwrite = co | fr
> let to-w = rwdep | (overwrite & int)
> -let to-r = addr | (dep ; rfi) | rfi-rel-acq
> +let to-r = addr | (dep ; rfi)
> let fence = strong-fence | wmb | po-rel | rmb | acq-po
> -let ppo = to-r | to-w | fence
> +let ppo = to-r | to-w | fence | (po-rel-rf-acq-po & int)
>
> (* Propagation: Ordering from release operations and strong fences. *)
> let A-cumul(r) = rfe? ; r
> -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
> +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-rel-rf-acq-po
> let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
>
> (*
Isn't the job of the memory model to formalise the guarantees provided by
the implementation? Your diff appears to do exactly the opposite.
> I take this opportunity to summarize my viewpoint on these matters:
>
> Someone would have to write the commit message for the above diff ...
> that is, to describe -why- we should go RCtso (and update the documen-
> tation accordingly); by now, the only argument for this appears to be:
> "(most) people expect strong ordering" _and they will be "lazy enough"
> to not check their expectations by using the LKMM tool (paraphrasing
> from [1]); IAC, Linux "might work" better if we add this ordering to
> the LKMM. Agreeing on such an approach would mean agreeing that this
> argument "wins" over:
>
> "We want new architectures to implement acquire/release efficiently,
> and it's not unlikely that they will have acquire loads that are
> similar in semantics to LDAPR." [2]
>
> "RISC-V probably would have been RCpc [...] it takes extra fences
> to go from RCpc to either "RCtso" or RCsc." [3]
>
> (or similar instances) since, of course, there is no such thing as a
> "free strong ordering"; and I'm not only talking about "efficiency",
> I'm also thinking at the fact that someone will have to maintain that
> ordering across all the architectures and in the LKMM.
>
> If, OTOH, we agree that the above "win"/assumption is valid only for
> locks or, in other/better words, if we agree that we should maintain
> _two_ distinct release-acquire orderings (a first one for unlock-lock
> sequences and a second one for ordinary/atomic release-acquire, say,
> as proposed in the patch under RFC), I ask that we audit and modify
> the generic code accordingly/as suggested in other posts _before_ we
> upstream the changes for the LKMM: we should identify those places
> where (the newly introduced) _gap_ between unlock-lock and the other
> release-acquire is not admissible and fix those places (notice that
> this entails, in part., agreeing on what/where the generic code is).
This is completely unrealistic. Have we already audited the kernel for the
current definition of the memory model? Should we revert it until we have?
Of course not.
Right now, LKMM offers stronger guarantees that can portably be relied upon
in the codebase. Alan's patch fixes that, and holding back a fix for a known
issue runs counter to kernel development best practices.
> Finally, if we don't agree with the above assumption at all (that is,
> no matter if we are considering unlock-lock or other release-acquire
> sequences), then we should go RCpc [4].
>
> I described three different approaches (which are NOT "independent",
> clearly; let us find an agreement...); even though some of them look
> insane to me, I'm currently open to all of them: thoughts?
I'm very confused by your statements hypothesising about where our opinions
may lie. We've discussed this to death, and it's clear that everybody who's
commented apart from you is happy to weaken acquire/release but leave
locking alone. Alan's written a patch to that effect which, again, only you
seem to have a problem with.
The problem isn't about "if we agree foo" or "if we don't agree bar", the
problem is that you're the only person raising an objection, so please can
you provide a constructive argument against Alan's patch, rather than a
confusing monologue of "what-if"s and unreasonable demands of anonymous
contributors? We don't have to solve all of our problems before we can
make any progress.
Thanks,
Will
On Mon, 3 Sep 2018, Andrea Parri wrote:
> In Cat speak,
>
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 59b5cbe6b6240..fd9c0831adf0a 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -38,7 +38,7 @@ let strong-fence = mb | gp
> (* Release Acquire *)
> let acq-po = [Acquire] ; po ; [M]
> let po-rel = [M] ; po ; [Release]
> -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
> +let po-rel-rf-acq-po = po ; [Release] ; rf ; [Acquire] ; po
>
> (**********************************)
> (* Fundamental coherence ordering *)
> @@ -60,13 +60,13 @@ let dep = addr | data
> let rwdep = (dep | ctrl) ; [W]
> let overwrite = co | fr
> let to-w = rwdep | (overwrite & int)
> -let to-r = addr | (dep ; rfi) | rfi-rel-acq
> +let to-r = addr | (dep ; rfi)
> let fence = strong-fence | wmb | po-rel | rmb | acq-po
> -let ppo = to-r | to-w | fence
> +let ppo = to-r | to-w | fence | (po-rel-rf-acq-po & int)
>
> (* Propagation: Ordering from release operations and strong fences. *)
> let A-cumul(r) = rfe? ; r
> -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
> +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-rel-rf-acq-po
> let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
>
> (*
I thought the goal you were aiming for was a patch making
atomic-acquire/ordinary-release be RCtso (along with lock/unlock),
while leaving ordinary-acquire/ordinary-release to remain RCpc.
Clearly that is not what this patch does.
Alan
On Mon, Sep 03, 2018 at 01:52:07PM -0400, Alan Stern wrote:
> On Mon, 3 Sep 2018, Andrea Parri wrote:
>
> > In Cat speak,
> >
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index 59b5cbe6b6240..fd9c0831adf0a 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -38,7 +38,7 @@ let strong-fence = mb | gp
> > (* Release Acquire *)
> > let acq-po = [Acquire] ; po ; [M]
> > let po-rel = [M] ; po ; [Release]
> > -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
> > +let po-rel-rf-acq-po = po ; [Release] ; rf ; [Acquire] ; po
> >
> > (**********************************)
> > (* Fundamental coherence ordering *)
> > @@ -60,13 +60,13 @@ let dep = addr | data
> > let rwdep = (dep | ctrl) ; [W]
> > let overwrite = co | fr
> > let to-w = rwdep | (overwrite & int)
> > -let to-r = addr | (dep ; rfi) | rfi-rel-acq
> > +let to-r = addr | (dep ; rfi)
> > let fence = strong-fence | wmb | po-rel | rmb | acq-po
> > -let ppo = to-r | to-w | fence
> > +let ppo = to-r | to-w | fence | (po-rel-rf-acq-po & int)
> >
> > (* Propagation: Ordering from release operations and strong fences. *)
> > let A-cumul(r) = rfe? ; r
> > -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
> > +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-rel-rf-acq-po
> > let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
> >
> > (*
>
> I thought the goal you were aiming for was a patch making
> atomic-acquire/ordinary-release be RCtso (along with lock/unlock),
> while leaving ordinary-acquire/ordinary-release to remain RCpc.
Such a patch would belong to the second approach (the "two distinct
release-acquire" approach from my previous email).
> Clearly that is not what this patch does.
I meant the above ;-) to illustrate yet another approach (not that
it makes me happy, as should be clear from previous posts ;-).
Andrea
>
> Alan
>
> > In Cat speak,
> >
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index 59b5cbe6b6240..fd9c0831adf0a 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -38,7 +38,7 @@ let strong-fence = mb | gp
> > (* Release Acquire *)
> > let acq-po = [Acquire] ; po ; [M]
> > let po-rel = [M] ; po ; [Release]
> > -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
> > +let po-rel-rf-acq-po = po ; [Release] ; rf ; [Acquire] ; po
> >
> > (**********************************)
> > (* Fundamental coherence ordering *)
> > @@ -60,13 +60,13 @@ let dep = addr | data
> > let rwdep = (dep | ctrl) ; [W]
> > let overwrite = co | fr
> > let to-w = rwdep | (overwrite & int)
> > -let to-r = addr | (dep ; rfi) | rfi-rel-acq
> > +let to-r = addr | (dep ; rfi)
> > let fence = strong-fence | wmb | po-rel | rmb | acq-po
> > -let ppo = to-r | to-w | fence
> > +let ppo = to-r | to-w | fence | (po-rel-rf-acq-po & int)
> >
> > (* Propagation: Ordering from release operations and strong fences. *)
> > let A-cumul(r) = rfe? ; r
> > -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
> > +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-rel-rf-acq-po
> > let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
> >
> > (*
>
> Isn't the job of the memory model to formalise the guarantees provided by
> the implementation? Your diff appears to do exactly the opposite.
This wouldn't be the first time..., but what am I missing?
>
> > I take this opportunity to summarize my viewpoint on these matters:
> >
> > Someone would have to write the commit message for the above diff ...
> > that is, to describe -why- we should go RCtso (and update the documen-
> > tation accordingly); by now, the only argument for this appears to be:
> > "(most) people expect strong ordering" _and they will be "lazy enough"
> > to not check their expectations by using the LKMM tool (paraphrasing
> > from [1]); IAC, Linux "might work" better if we add this ordering to
> > the LKMM. Agreeing on such an approach would mean agreeing that this
> > argument "wins" over:
> >
> > "We want new architectures to implement acquire/release efficiently,
> > and it's not unlikely that they will have acquire loads that are
> > similar in semantics to LDAPR." [2]
> >
> > "RISC-V probably would have been RCpc [...] it takes extra fences
> > to go from RCpc to either "RCtso" or RCsc." [3]
> >
> > (or similar instances) since, of course, there is no such thing as a
> > "free strong ordering"; and I'm not only talking about "efficiency",
> > I'm also thinking at the fact that someone will have to maintain that
> > ordering across all the architectures and in the LKMM.
> >
> > If, OTOH, we agree that the above "win"/assumption is valid only for
> > locks or, in other/better words, if we agree that we should maintain
> > _two_ distinct release-acquire orderings (a first one for unlock-lock
> > sequences and a second one for ordinary/atomic release-acquire, say,
> > as proposed in the patch under RFC), I ask that we audit and modify
> > the generic code accordingly/as suggested in other posts _before_ we
> > upstream the changes for the LKMM: we should identify those places
> > where (the newly introduced) _gap_ between unlock-lock and the other
> > release-acquire is not admissible and fix those places (notice that
> > this entails, in part., agreeing on what/where the generic code is).
>
> This is completely unrealistic. Have we already audited the kernel for the
> current definition of the memory model? Should we revert it until we have?
?? The fact that we've not audited the entire kernel does not mean
that we should throw away what has been already audited and verified
(over time).
IIUC, you're telling that we have a bunch of acquire/release spread
across generic locking code _and_ responsible for providing the lock
/unlock ordering guarantees, BUT we have no means to identify them.
I would have said "hard", but hear you say "unrealistic" represents
for me a very strong ARGUMENT AGAINST that "let us have two release-
acquire..."
>
> Of course not.
>
> Right now, LKMM offers stronger guarantees that can portably be relied upon
> in the codebase. Alan's patch fixes that, and holding back a fix for a known
> issue runs counter to kernel development best practices.
Then say so (and explain) in the commit message; AFAICT, failing to
do so would also run counter best practices.
>
> > Finally, if we don't agree with the above assumption at all (that is,
> > no matter if we are considering unlock-lock or other release-acquire
> > sequences), then we should go RCpc [4].
> >
> > I described three different approaches (which are NOT "independent",
> > clearly; let us find an agreement...); even though some of them look
> > insane to me, I'm currently open to all of them: thoughts?
>
> I'm very confused by your statements hypothesising about where our opinions
> may lie. We've discussed this to death, and it's clear that everybody who's
> commented apart from you is happy to weaken acquire/release but leave
> locking alone. Alan's written a patch to that effect which, again, only you
> seem to have a problem with.
Heh, your confusion might be the reflection of mine... ;-) That was
indeed a long and not conclusive discussion (meaning there're pending
issues); and I cannot claim to find "arguments" such as:
"More than one kernel developer has expressed the opinion that
the LKMM should enforce ordering of writes by locking."
particularly helpful (I do tend to be convinced by arguments rather
than by opinions). In fact, you can take the following as my only
current "constructive argument" against the patch [1,2]:
THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
>
> The problem isn't about "if we agree foo" or "if we don't agree bar", the
> problem is that you're the only person raising an objection, so please can
> you provide a constructive argument against Alan's patch, rather than a
> confusing monologue of "what-if"s and unreasonable demands of anonymous
> contributors? We don't have to solve all of our problems before we can
> make any progress.
Hope the above can help,
Andrea
[1] http://lkml.kernel.org/r/20180710093821.GA5414@andrea
[2] http://lkml.kernel.org/r/20180830125045.GA6936@andrea
>
> Thanks,
>
> Will
On Tue, 4 Sep 2018, Andrea Parri wrote:
> Heh, your confusion might be the reflection of mine... ;-) That was
> indeed a long and not conclusive discussion (meaning there're pending
> issues); and I cannot claim to find "arguments" such as:
>
> "More than one kernel developer has expressed the opinion that
> the LKMM should enforce ordering of writes by locking."
>
> particularly helpful (I do tend to be convinced by arguments rather
> than by opinions). In fact, you can take the following as my only
> current "constructive argument" against the patch [1,2]:
>
> THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
> SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
Do you have any concrete suggestions (i.e., some actual text) for
improvements to the patch description? Earlier in your message you
mentioned that Will's comment:
LKMM offers stronger guarantees that can portably be relied upon
in the codebase.
would make a good addition. Suitably edited, it could be added to the
description. I can think of a few other things myself, but I'd like to
hear your thoughts. Anything else?
Alan
On Tue, Sep 04, 2018 at 03:09:49PM -0400, Alan Stern wrote:
> On Tue, 4 Sep 2018, Andrea Parri wrote:
> > Heh, your confusion might be the reflection of mine... ;-) That was
> > indeed a long and not conclusive discussion (meaning there're pending
> > issues); and I cannot claim to find "arguments" such as:
> >
> > "More than one kernel developer has expressed the opinion that
> > the LKMM should enforce ordering of writes by locking."
> >
> > particularly helpful (I do tend to be convinced by arguments rather
> > than by opinions). In fact, you can take the following as my only
> > current "constructive argument" against the patch [1,2]:
> >
> > THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
> > SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
>
> Do you have any concrete suggestions (i.e., some actual text) for
> improvements to the patch description? Earlier in your message you
> mentioned that Will's comment:
>
> LKMM offers stronger guarantees that can portably be relied upon
> in the codebase.
>
> would make a good addition. Suitably edited, it could be added to the
> description. I can think of a few other things myself, but I'd like to
> hear your thoughts. Anything else?
Yes: I do sometimes have the impression that your "rules" for trimming
text in emails/replies are too aggressive...
Andrea
>
> Alan
>
On 2018/09/05 09:21:51 +0200, Andrea Parri wrote:
> On Tue, Sep 04, 2018 at 03:09:49PM -0400, Alan Stern wrote:
>> On Tue, 4 Sep 2018, Andrea Parri wrote:
>>> Heh, your confusion might be the reflection of mine... ;-) That was
>>> indeed a long and not conclusive discussion (meaning there're pending
>>> issues); and I cannot claim to find "arguments" such as:
>>>
>>> "More than one kernel developer has expressed the opinion that
>>> the LKMM should enforce ordering of writes by locking."
>>>
>>> particularly helpful (I do tend to be convinced by arguments rather
>>> than by opinions). In fact, you can take the following as my only
>>> current "constructive argument" against the patch [1,2]:
>>>
>>> THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
>>> SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
>>
>> Do you have any concrete suggestions (i.e., some actual text) for
>> improvements to the patch description? Earlier in your message you
>> mentioned that Will's comment:
>>
>> LKMM offers stronger guarantees that can portably be relied upon
>> in the codebase.
>>
>> would make a good addition. Suitably edited, it could be added to the
>> description. I can think of a few other things myself, but I'd like to
>> hear your thoughts. Anything else?
>
> Yes: I do sometimes have the impression that your "rules" for trimming
> text in emails/replies are too aggressive...
Andrea, by saying "Yes:", do you mean you have something else to be added?
I don't think you do, but want to make sure.
I'm a bit surprised to see all you wanted was the amendment of the
commit log...
Akira
>
> Andrea
>
>
>>
>> Alan
>>
On Wed, Sep 05, 2018 at 11:33:08PM +0900, Akira Yokosawa wrote:
> On 2018/09/05 09:21:51 +0200, Andrea Parri wrote:
> > On Tue, Sep 04, 2018 at 03:09:49PM -0400, Alan Stern wrote:
> >> On Tue, 4 Sep 2018, Andrea Parri wrote:
> >>> Heh, your confusion might be the reflection of mine... ;-) That was
> >>> indeed a long and not conclusive discussion (meaning there're pending
> >>> issues); and I cannot claim to find "arguments" such as:
> >>>
> >>> "More than one kernel developer has expressed the opinion that
> >>> the LKMM should enforce ordering of writes by locking."
> >>>
> >>> particularly helpful (I do tend to be convinced by arguments rather
> >>> than by opinions). In fact, you can take the following as my only
> >>> current "constructive argument" against the patch [1,2]:
> >>>
> >>> THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
> >>> SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
> >>
> >> Do you have any concrete suggestions (i.e., some actual text) for
> >> improvements to the patch description? Earlier in your message you
> >> mentioned that Will's comment:
> >>
> >> LKMM offers stronger guarantees that can portably be relied upon
> >> in the codebase.
> >>
> >> would make a good addition. Suitably edited, it could be added to the
> >> description. I can think of a few other things myself, but I'd like to
> >> hear your thoughts. Anything else?
> >
> > Yes: I do sometimes have the impression that your "rules" for trimming
> > text in emails/replies are too aggressive...
>
> Andrea, by saying "Yes:", do you mean you have something else to be added?
> I don't think you do, but want to make sure.
>
> I'm a bit surprised to see all you wanted was the amendment of the
> commit log...
My guess is that Andrea would prefer that locking acquire/release and
load-store-RMW acquire/release to have the same ordering rules (which
Will has argued against), and that Andrea's "Yes" above is expressing
irritation that some point he wished to reiterate was trimmed somewhere
in the exchange. And yes, both the act of replying to emails and
of establishing multi-architecture ordering rules can be a bit messy
at times.
Andrea's patch had no Signed-off-by and does not apply to the -rcu tree's
dev branch, so I am guessing that he was thinking in terms of replacing
some subset of the patches that are currently queued, presumably including
Alan's patch that Will reviewed and Peter acked. (I don't yet have a
new lkmm branch because I need to sort out a few of the commits first.)
If replacement is the intent, the people Andrea needs to convince include
Alan, Peter, and Will.
Thanx, Paul
On Wed, Sep 05, 2018 at 11:33:08PM +0900, Akira Yokosawa wrote:
> On 2018/09/05 09:21:51 +0200, Andrea Parri wrote:
> > On Tue, Sep 04, 2018 at 03:09:49PM -0400, Alan Stern wrote:
> >> On Tue, 4 Sep 2018, Andrea Parri wrote:
> >>> Heh, your confusion might be the reflection of mine... ;-) That was
> >>> indeed a long and not conclusive discussion (meaning there're pending
> >>> issues); and I cannot claim to find "arguments" such as:
> >>>
> >>> "More than one kernel developer has expressed the opinion that
> >>> the LKMM should enforce ordering of writes by locking."
> >>>
> >>> particularly helpful (I do tend to be convinced by arguments rather
> >>> than by opinions). In fact, you can take the following as my only
> >>> current "constructive argument" against the patch [1,2]:
> >>>
> >>> THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
> >>> SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
> >>
> >> Do you have any concrete suggestions (i.e., some actual text) for
> >> improvements to the patch description? Earlier in your message you
> >> mentioned that Will's comment:
> >>
> >> LKMM offers stronger guarantees that can portably be relied upon
> >> in the codebase.
> >>
> >> would make a good addition. Suitably edited, it could be added to the
> >> description. I can think of a few other things myself, but I'd like to
> >> hear your thoughts. Anything else?
> >
> > Yes: I do sometimes have the impression that your "rules" for trimming
> > text in emails/replies are too aggressive...
>
> Andrea, by saying "Yes:", do you mean you have something else to be added?
Indeed (examples in the trimmed text).
> I don't think you do, but want to make sure.
>
> I'm a bit surprised to see all you wanted was the amendment of the
> commit log...
Well, I said that it was my only current constructive argument...
Andrea
>
> Akira
>
> >
> > Andrea
> >
> >
> >>
> >> Alan
> >>
>
On 2018/09/06 0:00, Andrea Parri wrote:
> On Wed, Sep 05, 2018 at 11:33:08PM +0900, Akira Yokosawa wrote:
>> On 2018/09/05 09:21:51 +0200, Andrea Parri wrote:
>>> On Tue, Sep 04, 2018 at 03:09:49PM -0400, Alan Stern wrote:
>>>> On Tue, 4 Sep 2018, Andrea Parri wrote:
>>>>> Heh, your confusion might be the reflection of mine... ;-) That was
>>>>> indeed a long and not conclusive discussion (meaning there're pending
>>>>> issues); and I cannot claim to find "arguments" such as:
>>>>>
>>>>> "More than one kernel developer has expressed the opinion that
>>>>> the LKMM should enforce ordering of writes by locking."
>>>>>
>>>>> particularly helpful (I do tend to be convinced by arguments rather
>>>>> than by opinions). In fact, you can take the following as my only
>>>>> current "constructive argument" against the patch [1,2]:
>>>>>
>>>>> THE COMMIT MESSAGE IS RIDICULOUS; PLEASE EXPAND ON IT, AND DO
>>>>> SO BY LEVERAGING BOTH PROS AND CONS OF THE APPLIED CHANGES
>>>>
>>>> Do you have any concrete suggestions (i.e., some actual text) for
>>>> improvements to the patch description? Earlier in your message you
>>>> mentioned that Will's comment:
>>>>
>>>> LKMM offers stronger guarantees that can portably be relied upon
>>>> in the codebase.
>>>>
>>>> would make a good addition. Suitably edited, it could be added to the
>>>> description. I can think of a few other things myself, but I'd like to
>>>> hear your thoughts. Anything else?
>>>
>>> Yes: I do sometimes have the impression that your "rules" for trimming
>>> text in emails/replies are too aggressive...
>>
>> Andrea, by saying "Yes:", do you mean you have something else to be added?
>
> Indeed (examples in the trimmed text).
So, you mean just amending commit log does not work for you?
>
>
>> I don't think you do, but want to make sure.
>>
>> I'm a bit surprised to see all you wanted was the amendment of the
>> commit log...
>
> Well, I said that it was my only current constructive argument...
This thread is getting quite hard for me to follow...
Akira
>
> Andrea
>
>
>>
>> Akira
>>
>>>
>>> Andrea
>>>
>>>
>>>>
>>>> Alan
>>>>
>>
> >>>> Do you have any concrete suggestions (i.e., some actual text) for
> >>>> improvements to the patch description? Earlier in your message you
> >>>> mentioned that Will's comment:
> >>>>
> >>>> LKMM offers stronger guarantees that can portably be relied upon
> >>>> in the codebase.
> >>>>
> >>>> would make a good addition. Suitably edited, it could be added to the
> >>>> description. I can think of a few other things myself, but I'd like to
> >>>> hear your thoughts. Anything else?
> >>>
> >>> Yes: I do sometimes have the impression that your "rules" for trimming
> >>> text in emails/replies are too aggressive...
> >>
> >> Andrea, by saying "Yes:", do you mean you have something else to be added?
> >
> > Indeed (examples in the trimmed text).
"examples" of "concrete suggestions" (pros or cons) to amend the log.
>
> So, you mean just amending commit log does not work for you?
I can't really answer this...; let's see the revisited log first.
Andrea
>
> >
> >
> >> I don't think you do, but want to make sure.
> >>
> >> I'm a bit surprised to see all you wanted was the amendment of the
> >> commit log...
> >
> > Well, I said that it was my only current constructive argument...
>
> This thread is getting quite hard for me to follow...
>
> Akira
>
> >
> > Andrea
> >
> >
> >>
> >> Akira
> >>
> >>>
> >>> Andrea
> >>>
> >>>
> >>>>
> >>>> Alan
> >>>>
> >>
>
On Mon, 3 Sep 2018, Andrea Parri wrote:
> I take this opportunity to summarize my viewpoint on these matters:
>
> Someone would have to write the commit message for the above diff ...
> that is, to describe -why- we should go RCtso (and update the documen-
> tation accordingly); by now, the only argument for this appears to be:
> "(most) people expect strong ordering" _and they will be "lazy enough"
> to not check their expectations by using the LKMM tool (paraphrasing
> from [1]); IAC, Linux "might work" better if we add this ordering to
> the LKMM. Agreeing on such an approach would mean agreeing that this
> argument "wins" over:
>
> "We want new architectures to implement acquire/release efficiently,
> and it's not unlikely that they will have acquire loads that are
> similar in semantics to LDAPR." [2]
>
> "RISC-V probably would have been RCpc [...] it takes extra fences
> to go from RCpc to either "RCtso" or RCsc." [3]
>
> (or similar instances) since, of course, there is no such thing as a
> "free strong ordering"; and I'm not only talking about "efficiency",
> I'm also thinking at the fact that someone will have to maintain that
> ordering across all the architectures and in the LKMM.
>
> If, OTOH, we agree that the above "win"/assumption is valid only for
> locks or, in other/better words, if we agree that we should maintain
> _two_ distinct release-acquire orderings (a first one for unlock-lock
> sequences and a second one for ordinary/atomic release-acquire, say,
> as proposed in the patch under RFC),
In fact, there have have been _two_ proposals along this line. One as
you describe here (which is what the 1/7 patch under discussion does),
and another in which unlock-lock sequences and atomic acquire-release
sequences both have "RCtso" semantics while ordinary acquire/release
sequences have RCpc semantics. You should consider the second
proposal. It could be put into the LKMM quite easily by building upon
this 1/7 patch.
> I ask that we audit and modify
> the generic code accordingly/as suggested in other posts _before_ we
> upstream the changes for the LKMM: we should identify those places
> where (the newly introduced) _gap_ between unlock-lock and the other
> release-acquire is not admissible and fix those places (notice that
> this entails, in part., agreeing on what/where the generic code is).
Have you noticed any part of the generic code that relies on ordinary
acquire-release (rather than atomic RMW acquire-release) in order to
implement locking constructs?
> Finally, if we don't agree with the above assumption at all (that is,
> no matter if we are considering unlock-lock or other release-acquire
> sequences), then we should go RCpc [4].
>
> I described three different approaches (which are NOT "independent",
> clearly; let us find an agreement...); even though some of them look
> insane to me, I'm currently open to all of them: thoughts?
How about this fourth approach?
Alan
> Andrea
>
> [1] http://lkml.kernel.org/r/[email protected]
> http://lkml.kernel.org/r/CA+55aFwKpkU5C23OYt1HCiD3X5bJHVh1jz5G2dSnF1+kVrOCTA@mail.gmail.com
> [2] http://lkml.kernel.org/r/[email protected]
> [3] http://lkml.kernel.org/r/[email protected]
> [4] http://lkml.kernel.org/r/20180711123421.GA9673@andrea
> http://lkml.kernel.org/r/[email protected]
On Wed, Sep 05, 2018 at 09:25:40PM -0400, Alan Stern wrote:
> On Mon, 3 Sep 2018, Andrea Parri wrote:
>
> > I take this opportunity to summarize my viewpoint on these matters:
> >
[1st approach/fix]
> > Someone would have to write the commit message for the above diff ...
> > that is, to describe -why- we should go RCtso (and update the documen-
> > tation accordingly); by now, the only argument for this appears to be:
> > "(most) people expect strong ordering" _and they will be "lazy enough"
> > to not check their expectations by using the LKMM tool (paraphrasing
> > from [1]); IAC, Linux "might work" better if we add this ordering to
> > the LKMM. Agreeing on such an approach would mean agreeing that this
> > argument "wins" over:
> >
> > "We want new architectures to implement acquire/release efficiently,
> > and it's not unlikely that they will have acquire loads that are
> > similar in semantics to LDAPR." [2]
> >
> > "RISC-V probably would have been RCpc [...] it takes extra fences
> > to go from RCpc to either "RCtso" or RCsc." [3]
> >
> > (or similar instances) since, of course, there is no such thing as a
> > "free strong ordering"; and I'm not only talking about "efficiency",
> > I'm also thinking at the fact that someone will have to maintain that
> > ordering across all the architectures and in the LKMM.
> >
[2nd approach/fix]
> > If, OTOH, we agree that the above "win"/assumption is valid only for
> > locks or, in other/better words, if we agree that we should maintain
> > _two_ distinct release-acquire orderings (a first one for unlock-lock
> > sequences and a second one for ordinary/atomic release-acquire, say,
> > as proposed in the patch under RFC),
>
> In fact, there have have been _two_ proposals along this line. One as
> you describe here (which is what the 1/7 patch under discussion does),
> and another in which unlock-lock sequences and atomic acquire-release
> sequences both have "RCtso" semantics while ordinary acquire/release
> sequences have RCpc semantics. You should consider the second
> proposal. It could be put into the LKMM quite easily by building upon
> this 1/7 patch.
I posted a prototype here (no replies from other LKMM maintainers):
http://lkml.kernel.org/r/20180712212351.GA5480@andrea
I'm certainly willing to consider it, but I would agree with you in
saying that this proposal follows this second "approach" above (in
part., it might be subject to the same/similar counterarguments).
>
> > I ask that we audit and modify
> > the generic code accordingly/as suggested in other posts _before_ we
> > upstream the changes for the LKMM: we should identify those places
> > where (the newly introduced) _gap_ between unlock-lock and the other
> > release-acquire is not admissible and fix those places (notice that
> > this entails, in part., agreeing on what/where the generic code is).
>
> Have you noticed any part of the generic code that relies on ordinary
> acquire-release (rather than atomic RMW acquire-release) in order to
> implement locking constructs?
There are several places in code where the "lock-acquire" seems to be
provided by an atomic_cond_read_acquire/smp_cond_load_acquire: I have
mentioned one in qspinlock in this thread; qrwlock and mcs_spinlock
provide other examples (grep for the primitives...).
As long as we don't consider these primitive as RMW (which would seem
odd...) or as acquire for which "most people expect strong ordering"
(see above), these provides other examples for the _gap_ I mentioned.
Notice that the issue/counter-argument here is not only:
"the proposal is taking us away from a tested-and-verified-over
-years design kernel developers are _used to reason with [have
one release-acquire] in favor of an "unrealistically" or harder,
FWIW, verifiable one [as if one wasn't enough fun already... ;-)]"
The issue is also how to realize the proposed "abstract" design in
kernel code!, since that "gap" makes doing so _not straightforward
at _least (examples: arm64 using LDAPR for its acquire and having
to fix its *cond_read* implementation; or riscv using .aq/.rl for
its atomics and having to audit generic code, which is "hard" ...).
>
[3rd approach/fix]
> > Finally, if we don't agree with the above assumption at all (that is,
> > no matter if we are considering unlock-lock or other release-acquire
> > sequences), then we should go RCpc [4].
> >
> > I described three different approaches (which are NOT "independent",
> > clearly; let us find an agreement...); even though some of them look
> > insane to me, I'm currently open to all of them: thoughts?
>
> How about this fourth approach?
Are you referring to the variation on the 2nd approach remarked above?
if so, please see above; otherwise, I'd ask "which one?".
Andrea
>
> Alan
>
> > Andrea
> >
> > [1] http://lkml.kernel.org/r/[email protected]
> > http://lkml.kernel.org/r/CA+55aFwKpkU5C23OYt1HCiD3X5bJHVh1jz5G2dSnF1+kVrOCTA@mail.gmail.com
> > [2] http://lkml.kernel.org/r/[email protected]
> > [3] http://lkml.kernel.org/r/[email protected]
> > [4] http://lkml.kernel.org/r/20180711123421.GA9673@andrea
> > http://lkml.kernel.org/r/[email protected]
>
On Fri, Aug 31, 2018 at 11:43:42AM +0200, Andrea Parri wrote:
> > > > + b. The "unless" RMW operations are not currently modeled:
> > > > + atomic_long_add_unless(), atomic_add_unless(),
> > > > + atomic_inc_unless_negative(), and
> > > > + atomic_dec_unless_positive(). These can be emulated
> > > > + in litmus tests, for example, by using atomic_cmpxchg().
> > >
> > > There is a prototype atomic_add_unless(): with current herd7,
> > >
> > > $ cat atomic_add_unless.litmus
> > > C atomic_add_unless
> > >
> > > {}
> > >
> > > P0(atomic_t *u, atomic_t *v)
> > > {
> > > int r0;
> > > int r1;
> > >
> > > r0 = atomic_add_unless(u, 1, 2);
> > > r1 = atomic_read(v);
> > > }
> > >
> > > P1(atomic_t *u, atomic_t *v)
> > > {
> > > int r0;
> > > int r1;
> > >
> > > r0 = atomic_add_unless(v, 1, 2);
> > > r1 = atomic_read(u);
> > > }
> > >
> > > exists (0:r1=0 /\ 1:r1=0)
> > >
> > > $ herd7 -conf linux-kernel.cfg atomic_add_unless.litmus
> > > Test atomic_add_unless Allowed
> > > States 3
> > > 0:r1=0; 1:r1=1;
> > > 0:r1=1; 1:r1=0;
> > > 0:r1=1; 1:r1=1;
> > > No
> > > Witnesses
> > > Positive: 0 Negative: 3
> > > Condition exists (0:r1=0 /\ 1:r1=0)
> > > Observation atomic_add_unless Never 0 3
> > > Time atomic_add_unless 0.00
> > > Hash=fa37a2359831690299e4cc394e45d966
> > >
> > > The last commit in the herdtools7 repo. related to this implementation
> > > (AFAICT) is:
> > >
> > > 9523c340917b6a ("herd/linux: make atomic_add_unless a primitive, so as to yield more precise dependencies for the returned boolean.")
> > >
> > > but I can only vaguely remember those dependencies issues now :/ ...;
> > > maybe we can now solve these issues? or should we change herd7 to re-
> > > turn a warning? (Notice that this primitive is currently not exported
> > > to the linux-kernel.def file.)
> >
> > Cool! It would be good to add this to the .def file once the underlying
> > herd7 machinery is ready. And then I would update the documentation
> > accordingly. Or happily accept a patch updating the documentation,
> > as the case might be. ;-)
>
> Fair enough, ;-) Please feel free to add:
>
> Reviewed-by: Andrea Parri <[email protected]>
Thank you! Applied and pushed out, updating the lkmm branch in the
process.
Thanx, Paul
On Thu, 6 Sep 2018, Andrea Parri wrote:
> > Have you noticed any part of the generic code that relies on ordinary
> > acquire-release (rather than atomic RMW acquire-release) in order to
> > implement locking constructs?
>
> There are several places in code where the "lock-acquire" seems to be
> provided by an atomic_cond_read_acquire/smp_cond_load_acquire: I have
> mentioned one in qspinlock in this thread; qrwlock and mcs_spinlock
> provide other examples (grep for the primitives...).
>
> As long as we don't consider these primitive as RMW (which would seem
> odd...) or as acquire for which "most people expect strong ordering"
> (see above), these provides other examples for the _gap_ I mentioned.
Okay, now I understand your objection. It does appear that on RISC-V,
if nowhere else, the current implementations of qspinlock, qrwlock,
etc. will not provide "RCtso" ordering.
The discussions surrounding this topic have been so lengthy and
confusing that I have lost track of any comments Palmer or Daniel may
have made concerning this potential problem.
One possible resolution would be to define smp_cond_load_acquire()
specially on RISC-V so that it provided the same ordering guarantees as
RMW-acquire. (Plus adding a comment in the asm-generic/barrier.h
pointing out the necessity for the stronger guarantee on all
architectures.)
Another would be to replace the usages of atomic/smp_cond_load_acquire
in the locking constructs with a new function that would otherwise be
the same but would provide the ordering guarantee we want.
Do you think either of these would be an adequate fix?
Alan
On Fri, Sep 07, 2018 at 12:00:19PM -0400, Alan Stern wrote:
> On Thu, 6 Sep 2018, Andrea Parri wrote:
>
> > > Have you noticed any part of the generic code that relies on ordinary
> > > acquire-release (rather than atomic RMW acquire-release) in order to
> > > implement locking constructs?
> >
> > There are several places in code where the "lock-acquire" seems to be
> > provided by an atomic_cond_read_acquire/smp_cond_load_acquire: I have
> > mentioned one in qspinlock in this thread; qrwlock and mcs_spinlock
> > provide other examples (grep for the primitives...).
> >
> > As long as we don't consider these primitive as RMW (which would seem
> > odd...) or as acquire for which "most people expect strong ordering"
> > (see above), these provides other examples for the _gap_ I mentioned.
>
> Okay, now I understand your objection. It does appear that on RISC-V,
> if nowhere else, the current implementations of qspinlock, qrwlock,
> etc. will not provide "RCtso" ordering.
>
> The discussions surrounding this topic have been so lengthy and
> confusing that I have lost track of any comments Palmer or Daniel may
> have made concerning this potential problem.
>
> One possible resolution would be to define smp_cond_load_acquire()
> specially on RISC-V so that it provided the same ordering guarantees as
> RMW-acquire. (Plus adding a comment in the asm-generic/barrier.h
> pointing out the necessity for the stronger guarantee on all
> architectures.)
>
> Another would be to replace the usages of atomic/smp_cond_load_acquire
> in the locking constructs with a new function that would otherwise be
> the same but would provide the ordering guarantee we want.
>
> Do you think either of these would be an adequate fix?
I didn't think RISC-V used qspinlock or qrwlock, so I'm not sure there's
actually anything to fix, is there?
Will
On 9/7/2018 9:09 AM, Will Deacon wrote:
> On Fri, Sep 07, 2018 at 12:00:19PM -0400, Alan Stern wrote:
>> On Thu, 6 Sep 2018, Andrea Parri wrote:
>>
>>>> Have you noticed any part of the generic code that relies on ordinary
>>>> acquire-release (rather than atomic RMW acquire-release) in order to
>>>> implement locking constructs?
>>>
>>> There are several places in code where the "lock-acquire" seems to be
>>> provided by an atomic_cond_read_acquire/smp_cond_load_acquire: I have
>>> mentioned one in qspinlock in this thread; qrwlock and mcs_spinlock
>>> provide other examples (grep for the primitives...).
>>>
>>> As long as we don't consider these primitive as RMW (which would seem
>>> odd...) or as acquire for which "most people expect strong ordering"
>>> (see above), these provides other examples for the _gap_ I mentioned.
>>
>> Okay, now I understand your objection. It does appear that on RISC-V,
>> if nowhere else, the current implementations of qspinlock, qrwlock,
>> etc. will not provide "RCtso" ordering.
>>
>> The discussions surrounding this topic have been so lengthy and
>> confusing that I have lost track of any comments Palmer or Daniel may
>> have made concerning this potential problem.
>>
>> One possible resolution would be to define smp_cond_load_acquire()
>> specially on RISC-V so that it provided the same ordering guarantees as
>> RMW-acquire. (Plus adding a comment in the asm-generic/barrier.h
>> pointing out the necessity for the stronger guarantee on all
>> architectures.)
>>
>> Another would be to replace the usages of atomic/smp_cond_load_acquire
>> in the locking constructs with a new function that would otherwise be
>> the same but would provide the ordering guarantee we want.
>>
>> Do you think either of these would be an adequate fix?
>
> I didn't think RISC-V used qspinlock or qrwlock, so I'm not sure there's
> actually anything to fix, is there?
>
> Will
I've also lost track of whether the current preference is or is not for
RCtso, or in which subset of cases RCtso is currently preferred. For
whichever cases do in fact need to be RCtso, the RISC-V approach would
still be the same as what I've written in the past, as far as I can
tell [1].
In a nutshell, if a data structure uses only atomics with .aq/.rl,
RISC-V provides RCtso already anyway. If a data structure uses fences,
or mixes fences and atomics, we can replace a "fence r,rw" or a
"fence rw,w" with a "fence.tso" (== fence r,rw + fence rw,w) as
necessary, at the cost of some amount of performance.
I suppose the answer to the question of whether smp_cond_load_acquire()
needs to change depends on where exactly RCtso is needed, and which
data structures actually use that vs. some other macro.
Does that answer your question Alan? Does it make sense?
[1] https://lore.kernel.org/lkml/[email protected]/
Dan
On Fri, 7 Sep 2018, Daniel Lustig wrote:
> On 9/7/2018 9:09 AM, Will Deacon wrote:
> > On Fri, Sep 07, 2018 at 12:00:19PM -0400, Alan Stern wrote:
> >> On Thu, 6 Sep 2018, Andrea Parri wrote:
> >>
> >>>> Have you noticed any part of the generic code that relies on ordinary
> >>>> acquire-release (rather than atomic RMW acquire-release) in order to
> >>>> implement locking constructs?
> >>>
> >>> There are several places in code where the "lock-acquire" seems to be
> >>> provided by an atomic_cond_read_acquire/smp_cond_load_acquire: I have
> >>> mentioned one in qspinlock in this thread; qrwlock and mcs_spinlock
> >>> provide other examples (grep for the primitives...).
> >>>
> >>> As long as we don't consider these primitive as RMW (which would seem
> >>> odd...) or as acquire for which "most people expect strong ordering"
> >>> (see above), these provides other examples for the _gap_ I mentioned.
> >>
> >> Okay, now I understand your objection. It does appear that on RISC-V,
> >> if nowhere else, the current implementations of qspinlock, qrwlock,
> >> etc. will not provide "RCtso" ordering.
> >>
> >> The discussions surrounding this topic have been so lengthy and
> >> confusing that I have lost track of any comments Palmer or Daniel may
> >> have made concerning this potential problem.
> >>
> >> One possible resolution would be to define smp_cond_load_acquire()
> >> specially on RISC-V so that it provided the same ordering guarantees as
> >> RMW-acquire. (Plus adding a comment in the asm-generic/barrier.h
> >> pointing out the necessity for the stronger guarantee on all
> >> architectures.)
> >>
> >> Another would be to replace the usages of atomic/smp_cond_load_acquire
> >> in the locking constructs with a new function that would otherwise be
> >> the same but would provide the ordering guarantee we want.
> >>
> >> Do you think either of these would be an adequate fix?
> >
> > I didn't think RISC-V used qspinlock or qrwlock, so I'm not sure there's
> > actually anything to fix, is there?
> >
> > Will
>
> I've also lost track of whether the current preference is or is not for
> RCtso, or in which subset of cases RCtso is currently preferred. For
> whichever cases do in fact need to be RCtso, the RISC-V approach would
> still be the same as what I've written in the past, as far as I can
> tell [1].
The patch which Paul plans to send in for the next merge window makes
the LKMM require RCtso ordering for spinlocks, and by extension, for
all locking operations. As I understand it, the current RISC-V
implementation of spinlocks does provide this ordering.
We have discussed creating another patch for the LKMM which would
require RMW-acquire/ordinary-release also to have RCtso ordering.
Nobody has written the patch yet, but it would be straightfoward. The
rationale is that many types of locks are implemented in terms of
RMW-acquire, so if the locks are required to be RCtso then so should
the lower-level operations they are built from.
Will feels strongly (and Linus agrees) that the LKMM should not require
ordinary acquire and release to be any stronger than RCpc.
The issue that Andrea raised has to do with qspinlock, qrwlock, and
mcs_spinlock, which are implemented using smp_cond_load_acquire()
instead of RMW-acquire. This provides only the ordering properties of
smp_load_acquire(), namely RCpc, which means that qspinlocks etc. might
not be RCtso.
Since we do want locks to be RCtso, the question is how to resolve this
discrepancy.
> In a nutshell, if a data structure uses only atomics with .aq/.rl,
> RISC-V provides RCtso already anyway. If a data structure uses fences,
> or mixes fences and atomics, we can replace a "fence r,rw" or a
> "fence rw,w" with a "fence.tso" (== fence r,rw + fence rw,w) as
> necessary, at the cost of some amount of performance.
>
> I suppose the answer to the question of whether smp_cond_load_acquire()
> needs to change depends on where exactly RCtso is needed, and which
> data structures actually use that vs. some other macro.
>
> Does that answer your question Alan? Does it make sense?
On all other architectures, as far as I know, smp_cond_load_acquire()
is in fact RCtso. Any changes would only be needed on RISC-V.
A quick grep of the kernel source (not quite up-to-date, unfortunately)
turns up only the following additional usages of
smp_cond_load_acquire():
It is used in kernel/smp.c for csd_lock(); I don't know what
that is meant for.
It is also used in the scheduler core (kernel/sched/core.c). I
don't know what ordering requirements the scheduler has for it,
but Peter does.
There's a usage in drivers/iommu/arm-smmu-v3.c, but no comment
to explain why it is needed.
To tell the truth, I'm not aware of any code in the kernel that
actually _needs_ RCtso ordering for locks, but Peter and Will are quite
firm that it should be required. Linus would actually like locks to be
RCsc, but he recognizes that this would incur a noticeable performance
penalty on Power so he'll settle for RCtso.
I'm not in a position to say whether smp_cond_load_acquire() should be
changed, but hopefully this information will help others to make that
determination.
Alan
> [1] https://lore.kernel.org/lkml/[email protected]/
>
> Dan
On 9/7/2018 10:38 AM, Alan Stern wrote:
> On Fri, 7 Sep 2018, Daniel Lustig wrote:
>
>> On 9/7/2018 9:09 AM, Will Deacon wrote:
>>> On Fri, Sep 07, 2018 at 12:00:19PM -0400, Alan Stern wrote:
>>>> On Thu, 6 Sep 2018, Andrea Parri wrote:
>>>>
>>>>>> Have you noticed any part of the generic code that relies on ordinary
>>>>>> acquire-release (rather than atomic RMW acquire-release) in order to
>>>>>> implement locking constructs?
>>>>>
>>>>> There are several places in code where the "lock-acquire" seems to be
>>>>> provided by an atomic_cond_read_acquire/smp_cond_load_acquire: I have
>>>>> mentioned one in qspinlock in this thread; qrwlock and mcs_spinlock
>>>>> provide other examples (grep for the primitives...).
>>>>>
>>>>> As long as we don't consider these primitive as RMW (which would seem
>>>>> odd...) or as acquire for which "most people expect strong ordering"
>>>>> (see above), these provides other examples for the _gap_ I mentioned.
>>>>
>>>> Okay, now I understand your objection. It does appear that on RISC-V,
>>>> if nowhere else, the current implementations of qspinlock, qrwlock,
>>>> etc. will not provide "RCtso" ordering.
>>>>
>>>> The discussions surrounding this topic have been so lengthy and
>>>> confusing that I have lost track of any comments Palmer or Daniel may
>>>> have made concerning this potential problem.
>>>>
>>>> One possible resolution would be to define smp_cond_load_acquire()
>>>> specially on RISC-V so that it provided the same ordering guarantees as
>>>> RMW-acquire. (Plus adding a comment in the asm-generic/barrier.h
>>>> pointing out the necessity for the stronger guarantee on all
>>>> architectures.)
>>>>
>>>> Another would be to replace the usages of atomic/smp_cond_load_acquire
>>>> in the locking constructs with a new function that would otherwise be
>>>> the same but would provide the ordering guarantee we want.
>>>>
>>>> Do you think either of these would be an adequate fix?
>>>
>>> I didn't think RISC-V used qspinlock or qrwlock, so I'm not sure there's
>>> actually anything to fix, is there?
>>>
>>> Will
>>
>> I've also lost track of whether the current preference is or is not for
>> RCtso, or in which subset of cases RCtso is currently preferred. For
>> whichever cases do in fact need to be RCtso, the RISC-V approach would
>> still be the same as what I've written in the past, as far as I can
>> tell [1].
>
> The patch which Paul plans to send in for the next merge window makes
> the LKMM require RCtso ordering for spinlocks, and by extension, for
> all locking operations. As I understand it, the current RISC-V
> implementation of spinlocks does provide this ordering.
>
> We have discussed creating another patch for the LKMM which would
> require RMW-acquire/ordinary-release also to have RCtso ordering.
> Nobody has written the patch yet, but it would be straightfoward. The
> rationale is that many types of locks are implemented in terms of
> RMW-acquire, so if the locks are required to be RCtso then so should
> the lower-level operations they are built from.
>
> Will feels strongly (and Linus agrees) that the LKMM should not require
> ordinary acquire and release to be any stronger than RCpc.
>
> The issue that Andrea raised has to do with qspinlock, qrwlock, and
> mcs_spinlock, which are implemented using smp_cond_load_acquire()
> instead of RMW-acquire. This provides only the ordering properties of
> smp_load_acquire(), namely RCpc, which means that qspinlocks etc. might
> not be RCtso.
>
> Since we do want locks to be RCtso, the question is how to resolve this
> discrepancy.
Thanks for the summary Alan!
I think RISC-V might actually get RCtso with smp_cond_load_acquire()
implemented using fence r,rw, believe it or not :)
The read->read and read->write requirements are covered by the fence r,rw, so
what we need to add on is the write->write ordering requirement. On RISC-V,
we can get release semantics in three ways: fence rw,w, AMO.rl, and SC.rl.
If we use fence rw,w for release, then the "w,w" part covers it.
If we use AMO.rl for release, then the prior stores are ordered before the
AMO, and the fence r,rw orders the AMO before subsequent stores.
If we use SC.rl, then the prior stores are ordered before the SC, and the
branch to check whether the SC succeeded induces a control dependency that
keeps subsequent stores ordered after the SC.
So, it seems to work anyway. I did a quick check of this property against
my Alloy model and it seems to agree as well.
The one combination that doesn't quite get you RCtso on RISC-V is pairing a
fence r,rw with an LR.aq. I think everything else works, including pairing
fence r,rw with AMO.aq. So it's really this one case we have to look out for.
Does that seem plausible to you all?
Dan
>> In a nutshell, if a data structure uses only atomics with .aq/.rl,
>> RISC-V provides RCtso already anyway. If a data structure uses fences,
>> or mixes fences and atomics, we can replace a "fence r,rw" or a
>> "fence rw,w" with a "fence.tso" (== fence r,rw + fence rw,w) as
>> necessary, at the cost of some amount of performance.
>>
>> I suppose the answer to the question of whether smp_cond_load_acquire()
>> needs to change depends on where exactly RCtso is needed, and which
>> data structures actually use that vs. some other macro.
>>
>> Does that answer your question Alan? Does it make sense?
>
> On all other architectures, as far as I know, smp_cond_load_acquire()
> is in fact RCtso. Any changes would only be needed on RISC-V.
>
> A quick grep of the kernel source (not quite up-to-date, unfortunately)
> turns up only the following additional usages of
> smp_cond_load_acquire():
>
> It is used in kernel/smp.c for csd_lock(); I don't know what
> that is meant for.
>
> It is also used in the scheduler core (kernel/sched/core.c). I
> don't know what ordering requirements the scheduler has for it,
> but Peter does.
>
> There's a usage in drivers/iommu/arm-smmu-v3.c, but no comment
> to explain why it is needed.
>
> To tell the truth, I'm not aware of any code in the kernel that
> actually _needs_ RCtso ordering for locks, but Peter and Will are quite
> firm that it should be required. Linus would actually like locks to be
> RCsc, but he recognizes that this would incur a noticeable performance
> penalty on Power so he'll settle for RCtso.
>
> I'm not in a position to say whether smp_cond_load_acquire() should be
> changed, but hopefully this information will help others to make that
> determination.
>
> Alan
>
>> [1] https://lore.kernel.org/lkml/[email protected]/
>>
>> Dan
>
> Will feels strongly (and Linus agrees) that the LKMM should not require
> ordinary acquire and release to be any stronger than RCpc.
>
> The issue that Andrea raised has to do with qspinlock, qrwlock, and
> mcs_spinlock, which are implemented using smp_cond_load_acquire()
> instead of RMW-acquire. This provides only the ordering properties of
> smp_load_acquire(), namely RCpc, which means that qspinlocks etc. might
> not be RCtso.
>
> Since we do want locks to be RCtso, the question is how to resolve this
> discrepancy.
[...]
> To tell the truth, I'm not aware of any code in the kernel that
> actually _needs_ RCtso ordering for locks, but Peter and Will are quite
> firm that it should be required. Linus would actually like locks to be
> RCsc, but he recognizes that this would incur a noticeable performance
> penalty on Power so he'll settle for RCtso.
It does look like Will, Peter, Linus and me could help you put together
a satisfactory patch description! ;-) I'm not sure I agree with all
you're claiming/concluding above..., but again: why don't you try to
collect what, in your opinion, are the relevant arguments/comments from
previous reviews of the patch (which, unfortunately, goes back to July)
and then send an updated version? (I do have the impression that these
discussions would have been much more "easy to follow" if you only did
that time ago/with higher frequency...)
Andrea
On Thu, 12 Jul 2018, Paul E. McKenney wrote:
> > > Take for instance the pattern where RCU relies on RCsc locks, this is an
> > > entirely simple and straight forward use of locks, yet completely fails
> > > on this subtle point.
> >
> > Do you happen to remember exactly where in the kernel source this
> > occurs?
>
> Look for the uses of raw_spin_lock_irq_rcu_node() and friends in
> kernel/rcu and include/linux/*rcu*, along with the explanation in
> Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html
I just now started looking at this for the first time, and I was struck
by the sloppy thinking displayed in the very first paragraph of the
HTML document! For example, consider the third sentence:
Similarly, any code that happens before the beginning of a
given RCU grace period is guaranteed to see the effects of all
accesses following the end of that grace period that are within
RCU read-side critical sections.
Is RCU now a time machine? :-)
I think what you meant to write in the second and third sentences was
something more like this:
Any code in an RCU critical section that extends beyond the
end of a given RCU grace period is guaranteed to see the
effects of all accesses which were visible to the grace
period's CPU before the start of the grace period. Similarly,
any code that follows an RCU grace period (on the grace
period's CPU) is guaranteed to see the effects of all accesses
which were visible to an RCU critical section that began
before the start of the grace period.
Also, the document doesn't seem to explain how Tree RCU relies on the
lock-ordering guarantees of raw_spin_lock_rcu_node() and friends. It
_says_ that these guarantees are used, but not how or where. (Unless I
missed something; I didn't read the document all that carefully.)
In any case, you should bear in mind that the lock ordering provided by
Peter's raw_spin_lock_rcu_node() and friends is not the same as what we
have been discussing for the LKMM:
Peter's routines are meant for the case where you release
one lock and then acquire another (for example, locks in
two different levels of the RCU tree).
The LKMM patch applies only to cases where one CPU releases
a lock and then that CPU or another acquires the _same_ lock
again.
As another difference, the litmus test given near the start of the
"Tree RCU Grace Period Memory Ordering Building Blocks" section would
not be forbidden by the LKMM, even with RCtso locks, if it didn't use
raw_spin_lock_rcu_node(). This is because the litmus test is forbidden
only when locks are RCsc, which is what raw_spin_lock_rcu_node()
provides.
So I don't see how the RCU code can be held up as an example either for
or against requiring locks to be RCtso.
Alan
On Tue, Sep 11, 2018 at 03:31:53PM -0400, Alan Stern wrote:
> On Thu, 12 Jul 2018, Paul E. McKenney wrote:
>
> > > > Take for instance the pattern where RCU relies on RCsc locks, this is an
> > > > entirely simple and straight forward use of locks, yet completely fails
> > > > on this subtle point.
> > >
> > > Do you happen to remember exactly where in the kernel source this
> > > occurs?
> >
> > Look for the uses of raw_spin_lock_irq_rcu_node() and friends in
> > kernel/rcu and include/linux/*rcu*, along with the explanation in
> > Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html
>
> I just now started looking at this for the first time, and I was struck
> by the sloppy thinking displayed in the very first paragraph of the
> HTML document! For example, consider the third sentence:
>
> Similarly, any code that happens before the beginning of a
> given RCU grace period is guaranteed to see the effects of all
> accesses following the end of that grace period that are within
> RCU read-side critical sections.
>
> Is RCU now a time machine? :-)
Why not? ;-)
> I think what you meant to write in the second and third sentences was
> something more like this:
>
> Any code in an RCU critical section that extends beyond the
> end of a given RCU grace period is guaranteed to see the
> effects of all accesses which were visible to the grace
> period's CPU before the start of the grace period. Similarly,
> any code that follows an RCU grace period (on the grace
> period's CPU) is guaranteed to see the effects of all accesses
> which were visible to an RCU critical section that began
> before the start of the grace period.
That looks to me to be an improvement, other than that the "(on the
grace period's CPU)" seems a bit restrictive -- you could for example
have a release-acquire chain starting after the grace period, right?
> Also, the document doesn't seem to explain how Tree RCU relies on the
> lock-ordering guarantees of raw_spin_lock_rcu_node() and friends. It
> _says_ that these guarantees are used, but not how or where. (Unless I
> missed something; I didn't read the document all that carefully.)
The closest is this sentence: "But the only part of rcu_prepare_for_idle()
that really matters for this discussion are lines 37–39", which
refers to this code:
37 raw_spin_lock_rcu_node(rnp);
38 needwake = rcu_accelerate_cbs(rsp, rnp, rdp);
39 raw_spin_unlock_rcu_node(rnp);
I could add a sentence explaining the importance of the
smp_mb__after_unlock_lock() -- is that what you are getting at?
> In any case, you should bear in mind that the lock ordering provided by
> Peter's raw_spin_lock_rcu_node() and friends is not the same as what we
> have been discussing for the LKMM:
>
> Peter's routines are meant for the case where you release
> one lock and then acquire another (for example, locks in
> two different levels of the RCU tree).
>
> The LKMM patch applies only to cases where one CPU releases
> a lock and then that CPU or another acquires the _same_ lock
> again.
>
> As another difference, the litmus test given near the start of the
> "Tree RCU Grace Period Memory Ordering Building Blocks" section would
> not be forbidden by the LKMM, even with RCtso locks, if it didn't use
> raw_spin_lock_rcu_node(). This is because the litmus test is forbidden
> only when locks are RCsc, which is what raw_spin_lock_rcu_node()
> provides.
Agreed.
> So I don't see how the RCU code can be held up as an example either for
> or against requiring locks to be RCtso.
Agreed again. The use of smp_mb__after_unlock_lock() instead
provides RCsc. But this use case is deemed sufficiently rare that
smp_mb__after_unlock_lock() is defined within RCU.
Thanx, Paul
On Tue, 11 Sep 2018, Paul E. McKenney wrote:
> > I think what you meant to write in the second and third sentences was
> > something more like this:
> >
> > Any code in an RCU critical section that extends beyond the
> > end of a given RCU grace period is guaranteed to see the
> > effects of all accesses which were visible to the grace
> > period's CPU before the start of the grace period. Similarly,
> > any code that follows an RCU grace period (on the grace
> > period's CPU) is guaranteed to see the effects of all accesses
> > which were visible to an RCU critical section that began
> > before the start of the grace period.
>
> That looks to me to be an improvement, other than that the "(on the
> grace period's CPU)" seems a bit restrictive -- you could for example
> have a release-acquire chain starting after the grace period, right?
The restriction was deliberate. Without the restriction people might
think it applies to any code that happens after a grace period, which
is not true (depending on what you mean by "happens after").
The business about a release-acquire chain is derivable from what I
wrote. Since the chain starts on the grace period's CPU, the effect is
guaranteed to be visible there. Then since release-acquire chains
preserve visibility, the effect is guaranteed to be visible to the code
at the end of the chain.
> > Also, the document doesn't seem to explain how Tree RCU relies on the
> > lock-ordering guarantees of raw_spin_lock_rcu_node() and friends. It
> > _says_ that these guarantees are used, but not how or where. (Unless I
> > missed something; I didn't read the document all that carefully.)
>
> The closest is this sentence: "But the only part of rcu_prepare_for_idle()
> that really matters for this discussion are lines 37–39", which
> refers to this code:
>
> 37 raw_spin_lock_rcu_node(rnp);
> 38 needwake = rcu_accelerate_cbs(rsp, rnp, rdp);
> 39 raw_spin_unlock_rcu_node(rnp);
>
> I could add a sentence explaining the importance of the
> smp_mb__after_unlock_lock() -- is that what you are getting at?
What I was really asking is for the document to explain what could go
wrong if the smp_mb__after_unlock_lock() call was omitted from
raw_spin_lock_rcu_node(). What assumptions or requirements in the Tree
RCU code might fail, and how/where in the code are these assumptions or
requirements used?
> > In any case, you should bear in mind that the lock ordering provided by
> > Peter's raw_spin_lock_rcu_node() and friends is not the same as what we
> > have been discussing for the LKMM:
> >
> > Peter's routines are meant for the case where you release
> > one lock and then acquire another (for example, locks in
> > two different levels of the RCU tree).
> >
> > The LKMM patch applies only to cases where one CPU releases
> > a lock and then that CPU or another acquires the _same_ lock
> > again.
> >
> > As another difference, the litmus test given near the start of the
> > "Tree RCU Grace Period Memory Ordering Building Blocks" section would
> > not be forbidden by the LKMM, even with RCtso locks, if it didn't use
> > raw_spin_lock_rcu_node(). This is because the litmus test is forbidden
> > only when locks are RCsc, which is what raw_spin_lock_rcu_node()
> > provides.
>
> Agreed.
>
> > So I don't see how the RCU code can be held up as an example either for
> > or against requiring locks to be RCtso.
>
> Agreed again. The use of smp_mb__after_unlock_lock() instead
> provides RCsc. But this use case is deemed sufficiently rare that
> smp_mb__after_unlock_lock() is defined within RCU.
So let me repeat the original question which started this train of
thought: Can anybody point to any actual code in the kernel that relies
on locks being RCtso, or that could be simplified if locks were
guaranteed to be RCtso?
There have been claims that such code exists somewhere in RCU and the
scheduler. Where is it?
Alan
Not having received any responses to the question about usages of RCtso
locks, I have decided to post the newly updated version of the patch
description for commit c8c5779c854f ("tools/memory-model: Add extra
ordering for locks and remove it for ordinary release/acquire") in
Paul's LKMM branch. There are no changes to the patch itself.
Hopefully this includes all the important issues that people have
raised. (Admittedly, some parts of the discussion have seemed less
consequential than others, and some parts I didn't understand at all.)
Alan
-----------------------------------------------------------------------------
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" does not include RISC-V, which is still somewhat in
a state of flux.)
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.
Cons:
Andrea Parri and Luc Maranget feel 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) and that having different ordering
properties for different forms of acquires and releases would
be confusing and unmaintainable. Will and Linus, on the other
hand, feel that architectures should be free to implement
ordinary acquire/release using relatively weak RCpc machine
instructions. Linus points out 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 "expertss only" tool.
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). 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 in 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 long-time kernel developers such as Linus,
Peter, and Will carry more weight than those of Luc and Andrea, this
patch changes the model in accordance with the developers' wishes.
Signed-off-by: Alan Stern <[email protected]>
---
v.4: Added pros and cons discussion to the Changelog.
v.3: Rebased against the dev branch of Paul's linux-rcu tree.
Changed unlock-rf-lock-po to po-unlock-rf-lock-po, making it more
symmetrical and more in accordance with the use of fence.tso for
the release on RISC-V.
v.2: Restrict the ordering to lock operations, not general release
and acquire fences.
On Thu, Sep 13, 2018 at 01:07:39PM -0400, Alan Stern wrote:
> Not having received any responses to the question about usages of RCtso
> locks, I have decided to post the newly updated version of the patch
> description for commit c8c5779c854f ("tools/memory-model: Add extra
> ordering for locks and remove it for ordinary release/acquire") in
> Paul's LKMM branch. There are no changes to the patch itself.
>
> Hopefully this includes all the important issues that people have
> raised. (Admittedly, some parts of the discussion have seemed less
> consequential than others, and some parts I didn't understand at all.)
>
> Alan
>
> -----------------------------------------------------------------------------
> 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" does not include RISC-V, which is still somewhat in
> a state of flux.)
But "all supported architectures" does include RISC-V.
>
> 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.
Pros for "RCpc-only ordinary (and atomic) acquire/release" should go
here.
>
> Cons:
>
> Andrea Parri and Luc Maranget feel 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) and that having different ordering
> properties for different forms of acquires and releases would
> be confusing and unmaintainable.
s/unmaintainable/unneeded ("confusing" should already convey the
fragility of these changes).
>Will and Linus, on the other
> hand, feel that architectures should be free to implement
> ordinary acquire/release using relatively weak RCpc machine
> instructions. Linus points out 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 "expertss only" tool.
>
> 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
s/It is illogical/It is detrimental to the LKMM's applicability
> 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)
... w.r.t. the LKMM (same for smp_cond_load_acquire).
>. 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?
Your patch and Paul said "opinions ranking".
Andrea
>
> 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 in 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 long-time kernel developers such as Linus,
> Peter, and Will carry more weight than those of Luc and Andrea, this
> patch changes the model in accordance with the developers' wishes.
>
> Signed-off-by: Alan Stern <[email protected]>
>
> ---
>
> v.4: Added pros and cons discussion to the Changelog.
>
> v.3: Rebased against the dev branch of Paul's linux-rcu tree.
> Changed unlock-rf-lock-po to po-unlock-rf-lock-po, making it more
> symmetrical and more in accordance with the use of fence.tso for
> the release on RISC-V.
>
> v.2: Restrict the ordering to lock operations, not general release
> and acquire fences.
>
On Fri, 14 Sep 2018, Andrea Parri wrote:
> > 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" does not include RISC-V, which is still somewhat in
> > a state of flux.)
>
> But "all supported architectures" does include RISC-V.
For the next draft I have adopted a suggestion Paul made about this;
it should clarify the meaning.
> > 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.
>
> Pros for "RCpc-only ordinary (and atomic) acquire/release" should go
> here.
I have added two more paragraphs here, taking some of the material out of
the first Con entry.
> > Cons:
> >
> > Andrea Parri and Luc Maranget feel 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) and that having different ordering
> > properties for different forms of acquires and releases would
> > be confusing and unmaintainable.
>
> s/unmaintainable/unneeded ("confusing" should already convey the
> fragility of these changes).
The updated text includes all three notions explicitly.
> >Will and Linus, on the other
> > hand, feel that architectures should be free to implement
> > ordinary acquire/release using relatively weak RCpc machine
> > instructions. Linus points out 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 "expertss only" tool.
> >
> > 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
>
> s/It is illogical/It is detrimental to the LKMM's applicability
I disagree with this suggestion; not only would it be less readable,
it would lose a lot of the impact. It really is illogical to require
A to be stronger than B when A is made up from B.
> > 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)
>
> ... w.r.t. the LKMM (same for smp_cond_load_acquire).
Added. I'm not sure what you meant about smp_cond_load_acquire(), so
I didn't include it here (besides, the text already mentions
smp_cond_load_acquire() in the fourth Con entry).
> >. 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?
>
> Your patch and Paul said "opinions ranking".
What exactly are you referring to? A later part of the text includes
the phrase "opinions ... carry more weight", which means more or less
the same thing.
> Andrea
The updated Changelog draft is below.
Alan.
--------------------------------------------------------------------------
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 Peter
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 <[email protected]>
v.5: Incorporated feedback from Andrea regarding the updated Changelog.
v.4: Added pros and cons discussion to the Changelog.
v.3: Rebased against the dev branch of Paul's linux-rcu tree.
Changed unlock-rf-lock-po to po-unlock-rf-lock-po, making it more
symmetrical and more in accordance with the use of fence.tso for
the release on RISC-V.
v.2: Restrict the ordering to lock operations, not general release
and acquire fences.
On Wed, Aug 29, 2018 at 02:10:18PM -0700, Paul E. McKenney wrote:
> Hello!
>
> This series contains memory-model updates, not yet ready for inclusion:
Summarizing my current state for the week after next's planned
for-inclusion series:
ccc8b5139f65 tools/memory-model: Add litmus-test naming scheme
c8c5779c854f tools/memory-model: Add extra ordering for locks and remove it for ordinary release/acquire
a5109023cf9e tools/memory-model: Fix a README typo
abdb4ce79ba3 tools/memory-model: Add more LKMM limitations
I have these queued for the next merge window. There has
been some discussion of c8c5779c854f, and it would be
good to resolve issues. However, the patch is supported
by Peter Zijlstra (x86) and Will Deacon (ARM), so I
am OK sending it as-is if needed. We always have the
opportunity of adding other patches as needed.
The latest email from Andrea indicated some concerns about
the commit log, which cannot be changed after acceptance,
so resolving those concerns is the highest priority.
bf36a3124d04 doc: Replace smp_cond_acquire() with smp_cond_load_acquire()
Small change, needs an ack. Looks to me like is is
just aligning the documentation with the code, so
should not be controversial (famous last words).
Please take a look and consider giving feedback
and/or a review/ack.
f3625642c96d EXP tools/memory-model: Add scripts to check github litmus tests
eaaac2854b75 EXP tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
These add regression-test capability and need a review
and/or ack before they can be submitted. I do not
consider them to be particularly urgent.
Thanx, Paul
On Wed, Aug 29, 2018 at 02:10:48PM -0700, Paul E. McKenney wrote:
> From: Andrea Parri <[email protected]>
>
> Amend commit 1f03e8d2919270 ("locking/barriers: Replace smp_cond_acquire()
> with smp_cond_load_acquire()") by updating the documentation accordingly.
> Also remove some obsolete information related to the implementation.
>
> Signed-off-by: Andrea Parri <[email protected]>
> Cc: Alan Stern <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Boqun Feng <[email protected]>
> Cc: Nicholas Piggin <[email protected]>
> Cc: David Howells <[email protected]>
> Cc: Jade Alglave <[email protected]>
> Cc: Luc Maranget <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Akira Yokosawa <[email protected]>
> Cc: Daniel Lustig <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> Documentation/memory-barriers.txt | 3 +--
> 1 file changed, 1 insertion(+), 2 deletions(-)
>
> diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
> index 0d8d7ef131e9..c1d913944ad8 100644
> --- a/Documentation/memory-barriers.txt
> +++ b/Documentation/memory-barriers.txt
> @@ -471,8 +471,7 @@ And a couple of implicit varieties:
> operations after the ACQUIRE operation will appear to happen after the
> ACQUIRE operation with respect to the other components of the system.
> ACQUIRE operations include LOCK operations and both smp_load_acquire()
> - and smp_cond_acquire() operations. The later builds the necessary ACQUIRE
> - semantics from relying on a control dependency and smp_rmb().
> + and smp_cond_load_acquire() operations.
Thanks for fixing the doc:
Acked-by: Will Deacon <[email protected]>
Will
On Fri, 14 Sep 2018, Paul E. McKenney wrote:
> bf36a3124d04 doc: Replace smp_cond_acquire() with smp_cond_load_acquire()
>
> Small change, needs an ack. Looks to me like is is
> just aligning the documentation with the code, so
> should not be controversial (famous last words).
>
> Please take a look and consider giving feedback
> and/or a review/ack.
What branch is this commit in? It doesn't seem to be in the lkmm
branch.
In any case, the change is trivial and obviously correct.
Acked-by: Alan Stern <[email protected]>
Alan
On Fri, Sep 14, 2018 at 05:59:07PM +0100, Will Deacon wrote:
> On Wed, Aug 29, 2018 at 02:10:48PM -0700, Paul E. McKenney wrote:
> > From: Andrea Parri <[email protected]>
> >
> > Amend commit 1f03e8d2919270 ("locking/barriers: Replace smp_cond_acquire()
> > with smp_cond_load_acquire()") by updating the documentation accordingly.
> > Also remove some obsolete information related to the implementation.
> >
> > Signed-off-by: Andrea Parri <[email protected]>
> > Cc: Alan Stern <[email protected]>
> > Cc: Will Deacon <[email protected]>
> > Cc: Peter Zijlstra <[email protected]>
> > Cc: Boqun Feng <[email protected]>
> > Cc: Nicholas Piggin <[email protected]>
> > Cc: David Howells <[email protected]>
> > Cc: Jade Alglave <[email protected]>
> > Cc: Luc Maranget <[email protected]>
> > Cc: "Paul E. McKenney" <[email protected]>
> > Cc: Akira Yokosawa <[email protected]>
> > Cc: Daniel Lustig <[email protected]>
> > Cc: Jonathan Corbet <[email protected]>
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > Documentation/memory-barriers.txt | 3 +--
> > 1 file changed, 1 insertion(+), 2 deletions(-)
> >
> > diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
> > index 0d8d7ef131e9..c1d913944ad8 100644
> > --- a/Documentation/memory-barriers.txt
> > +++ b/Documentation/memory-barriers.txt
> > @@ -471,8 +471,7 @@ And a couple of implicit varieties:
> > operations after the ACQUIRE operation will appear to happen after the
> > ACQUIRE operation with respect to the other components of the system.
> > ACQUIRE operations include LOCK operations and both smp_load_acquire()
> > - and smp_cond_acquire() operations. The later builds the necessary ACQUIRE
> > - semantics from relying on a control dependency and smp_rmb().
> > + and smp_cond_load_acquire() operations.
>
> Thanks for fixing the doc:
>
> Acked-by: Will Deacon <[email protected]>
Applied, thank you Will!
Thanx, Paul
On Fri, Sep 14, 2018 at 01:19:37PM -0400, Alan Stern wrote:
> On Fri, 14 Sep 2018, Paul E. McKenney wrote:
>
> > bf36a3124d04 doc: Replace smp_cond_acquire() with smp_cond_load_acquire()
> >
> > Small change, needs an ack. Looks to me like is is
> > just aligning the documentation with the code, so
> > should not be controversial (famous last words).
> >
> > Please take a look and consider giving feedback
> > and/or a review/ack.
>
> What branch is this commit in? It doesn't seem to be in the lkmm
> branch.
It was in the dev branch, and was the child of the lkmm branch.
> In any case, the change is trivial and obviously correct.
>
> Acked-by: Alan Stern <[email protected]>
Thank you, applied!
And now it is in the lkmm branch. ;-)
Thanx, Paul
> The updated Changelog draft is below.
>
> Alan.
>
> --------------------------------------------------------------------------
> 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 Peter
> 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 <[email protected]>
Thank you for integrating the log.
I remain more sensitive to those Cons (and skeptical about that
po-unlock-rf-lock-po), but: (1) this doesn't make an objection,
and (2) you wore me down. ;-)
So unless new arguments are brought to light, feel free to add:
Reviewed-by: Andrea Parri <[email protected]>
Andrea
>
> v.5: Incorporated feedback from Andrea regarding the updated Changelog.
>
> v.4: Added pros and cons discussion to the Changelog.
>
> v.3: Rebased against the dev branch of Paul's linux-rcu tree.
> Changed unlock-rf-lock-po to po-unlock-rf-lock-po, making it more
> symmetrical and more in accordance with the use of fence.tso for
> the release on RISC-V.
>
> v.2: Restrict the ordering to lock operations, not general release
> and acquire fences.
>
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 <[email protected]>
Reviewed-by: Will Deacon <[email protected]>
Acked-by: Peter Zijlstra (Intel) <[email protected]>
Reviewed-by: Andrea Parri <[email protected]>
---
v.5: Incorporated feedback from Andrea regarding the updated Changelog.
v.4: Added pros and cons discussion to the Changelog.
v.3: Rebased against the dev branch of Paul's linux-rcu tree.
Changed unlock-rf-lock-po to po-unlock-rf-lock-po, making it more
symmetrical and more in accordance with the use of fence.tso for
the release on RISC-V.
v.2: Restrict the ordering to lock operations, not general release
and acquire fences.
[as1871e]
tools/memory-model/Documentation/explanation.txt | 186 +++++++---
tools/memory-model/linux-kernel.cat | 8
tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7
3 files changed, 150 insertions(+), 51 deletions(-)
Index: usb-4.x/tools/memory-model/linux-kernel.cat
===================================================================
--- usb-4.x.orig/tools/memory-model/linux-kernel.cat
+++ usb-4.x/tools/memory-model/linux-kernel.cat
@@ -38,7 +38,7 @@ let strong-fence = mb | gp
(* Release Acquire *)
let acq-po = [Acquire] ; po ; [M]
let po-rel = [M] ; po ; [Release]
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
+let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
(**********************************)
(* Fundamental coherence ordering *)
@@ -60,13 +60,13 @@ let dep = addr | data
let rwdep = (dep | ctrl) ; [W]
let overwrite = co | fr
let to-w = rwdep | (overwrite & int)
-let to-r = addr | (dep ; rfi) | rfi-rel-acq
+let to-r = addr | (dep ; rfi)
let fence = strong-fence | wmb | po-rel | rmb | acq-po
-let ppo = to-r | to-w | fence
+let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
(* Propagation: Ordering from release operations and strong fences. *)
let A-cumul(r) = rfe? ; r
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
+let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po
let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
(*
Index: usb-4.x/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
===================================================================
--- usb-4.x.orig/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
+++ usb-4.x/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
@@ -1,11 +1,10 @@
C ISA2+pooncelock+pooncelock+pombonce
(*
- * Result: Sometimes
+ * Result: Never
*
- * This test shows that the ordering provided by a lock-protected S
- * litmus test (P0() and P1()) are not visible to external process P2().
- * This is likely to change soon.
+ * This test shows that write-write ordering provided by locks
+ * (in P0() and P1()) is visible to external process P2().
*)
{}
Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
===================================================================
--- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
+++ usb-4.x/tools/memory-model/Documentation/explanation.txt
@@ -28,7 +28,8 @@ Explanation of the Linux-Kernel Memory C
20. THE HAPPENS-BEFORE RELATION: hb
21. THE PROPAGATES-BEFORE RELATION: pb
22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
- 23. ODDS AND ENDS
+ 23. LOCKING
+ 24. ODDS AND ENDS
@@ -1067,28 +1068,6 @@ allowing out-of-order writes like this t
violating the write-write coherence rule by requiring the CPU not to
send the W write to the memory subsystem at all!)
-There is one last example of preserved program order in the LKMM: when
-a load-acquire reads from an earlier store-release. For example:
-
- smp_store_release(&x, 123);
- r1 = smp_load_acquire(&x);
-
-If the smp_load_acquire() ends up obtaining the 123 value that was
-stored by the smp_store_release(), the LKMM says that the load must be
-executed after the store; the store cannot be forwarded to the load.
-This requirement does not arise from the operational model, but it
-yields correct predictions on all architectures supported by the Linux
-kernel, although for differing reasons.
-
-On some architectures, including x86 and ARMv8, it is true that the
-store cannot be forwarded to the load. On others, including PowerPC
-and ARMv7, smp_store_release() generates object code that starts with
-a fence and smp_load_acquire() generates object code that ends with a
-fence. The upshot is that even though the store may be forwarded to
-the load, it is still true that any instruction preceding the store
-will be executed before the load or any following instructions, and
-the store will be executed before any instruction following the load.
-
AND THEN THERE WAS ALPHA
------------------------
@@ -1766,6 +1745,147 @@ before it does, and the critical section
grace period does and ends after it does.
+LOCKING
+-------
+
+The LKMM includes locking. In fact, there is special code for locking
+in the formal model, added in order to make tools run faster.
+However, this special code is intended to be more or less equivalent
+to concepts we have already covered. A spinlock_t variable is treated
+the same as an int, and spin_lock(&s) is treated almost the same as:
+
+ while (cmpxchg_acquire(&s, 0, 1) != 0)
+ cpu_relax();
+
+This waits until s is equal to 0 and then atomically sets it to 1,
+and the read part of the cmpxchg operation acts as an acquire fence.
+An alternate way to express the same thing would be:
+
+ r = xchg_acquire(&s, 1);
+
+along with a requirement that at the end, r = 0. Similarly,
+spin_trylock(&s) is treated almost the same as:
+
+ return !cmpxchg_acquire(&s, 0, 1);
+
+which atomically sets s to 1 if it is currently equal to 0 and returns
+true if it succeeds (the read part of the cmpxchg operation acts as an
+acquire fence only if the operation is successful). spin_unlock(&s)
+is treated almost the same as:
+
+ smp_store_release(&s, 0);
+
+The "almost" qualifiers above need some explanation. In the LKMM, the
+store-release in a spin_unlock() and the load-acquire which forms the
+first half of the atomic rmw update in a spin_lock() or a successful
+spin_trylock() -- we can call these things lock-releases and
+lock-acquires -- have two properties beyond those of ordinary releases
+and acquires.
+
+First, when a lock-acquire reads from a lock-release, the LKMM
+requires that every instruction po-before the lock-release must
+execute before any instruction po-after the lock-acquire. This would
+naturally hold if the release and acquire operations were on different
+CPUs, but the LKMM says it holds even when they are on the same CPU.
+For example:
+
+ int x, y;
+ spinlock_t s;
+
+ P0()
+ {
+ int r1, r2;
+
+ spin_lock(&s);
+ r1 = READ_ONCE(x);
+ spin_unlock(&s);
+ spin_lock(&s);
+ r2 = READ_ONCE(y);
+ spin_unlock(&s);
+ }
+
+ P1()
+ {
+ WRITE_ONCE(y, 1);
+ smp_wmb();
+ WRITE_ONCE(x, 1);
+ }
+
+Here the second spin_lock() reads from the first spin_unlock(), and
+therefore the load of x must execute before the load of y. Thus we
+cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
+MP pattern).
+
+This requirement does not apply to ordinary release and acquire
+fences, only to lock-related operations. For instance, suppose P0()
+in the example had been written as:
+
+ P0()
+ {
+ int r1, r2, r3;
+
+ r1 = READ_ONCE(x);
+ smp_store_release(&s, 1);
+ r3 = smp_load_acquire(&s);
+ r2 = READ_ONCE(y);
+ }
+
+Then the CPU would be allowed to forward the s = 1 value from the
+smp_store_release() to the smp_load_acquire(), executing the
+instructions in the following order:
+
+ r3 = smp_load_acquire(&s); // Obtains r3 = 1
+ r2 = READ_ONCE(y);
+ r1 = READ_ONCE(x);
+ smp_store_release(&s, 1); // Value is forwarded
+
+and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
+
+Second, when a lock-acquire reads from a lock-release, and some other
+stores W and W' occur po-before the lock-release and po-after the
+lock-acquire respectively, the LKMM requires that W must propagate to
+each CPU before W' does. For example, consider:
+
+ int x, y;
+ spinlock_t x;
+
+ P0()
+ {
+ spin_lock(&s);
+ WRITE_ONCE(x, 1);
+ spin_unlock(&s);
+ }
+
+ P1()
+ {
+ int r1;
+
+ spin_lock(&s);
+ r1 = READ_ONCE(x);
+ WRITE_ONCE(y, 1);
+ spin_unlock(&s);
+ }
+
+ P2()
+ {
+ int r2, r3;
+
+ r2 = READ_ONCE(y);
+ smp_rmb();
+ r3 = READ_ONCE(x);
+ }
+
+If r1 = 1 at the end then the spin_lock() in P1 must have read from
+the spin_unlock() in P0. Hence the store to x must propagate to P2
+before the store to y does, so we cannot have r2 = 1 and r3 = 0.
+
+These two special requirements for lock-release and lock-acquire do
+not arise from the operational model. Nevertheless, kernel developers
+have come to expect and rely on them because they do hold on all
+architectures supported by the Linux kernel, albeit for various
+differing reasons.
+
+
ODDS AND ENDS
-------------
@@ -1831,26 +1951,6 @@ they behave as follows:
events and the events preceding them against all po-later
events.
-The LKMM includes locking. In fact, there is special code for locking
-in the formal model, added in order to make tools run faster.
-However, this special code is intended to be exactly equivalent to
-concepts we have already covered. A spinlock_t variable is treated
-the same as an int, and spin_lock(&s) is treated the same as:
-
- while (cmpxchg_acquire(&s, 0, 1) != 0)
- cpu_relax();
-
-which waits until s is equal to 0 and then atomically sets it to 1,
-and where the read part of the atomic update is also an acquire fence.
-An alternate way to express the same thing would be:
-
- r = xchg_acquire(&s, 1);
-
-along with a requirement that at the end, r = 0. spin_unlock(&s) is
-treated the same as:
-
- smp_store_release(&s, 0);
-
Interestingly, RCU and locking each introduce the possibility of
deadlock. When faced with code sequences such as:
On Fri, Sep 14, 2018 at 05:08:21PM -0400, Alan Stern wrote:
> 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);
Applied and pushed, thank you all!
Thanx, Paul
> 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 <[email protected]>
> Reviewed-by: Will Deacon <[email protected]>
> Acked-by: Peter Zijlstra (Intel) <[email protected]>
> Reviewed-by: Andrea Parri <[email protected]>
>
> ---
>
> v.5: Incorporated feedback from Andrea regarding the updated Changelog.
>
> v.4: Added pros and cons discussion to the Changelog.
>
> v.3: Rebased against the dev branch of Paul's linux-rcu tree.
> Changed unlock-rf-lock-po to po-unlock-rf-lock-po, making it more
> symmetrical and more in accordance with the use of fence.tso for
> the release on RISC-V.
>
> v.2: Restrict the ordering to lock operations, not general release
> and acquire fences.
>
>
> [as1871e]
>
>
> tools/memory-model/Documentation/explanation.txt | 186 +++++++---
> tools/memory-model/linux-kernel.cat | 8
> tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus | 7
> 3 files changed, 150 insertions(+), 51 deletions(-)
>
> Index: usb-4.x/tools/memory-model/linux-kernel.cat
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/linux-kernel.cat
> +++ usb-4.x/tools/memory-model/linux-kernel.cat
> @@ -38,7 +38,7 @@ let strong-fence = mb | gp
> (* Release Acquire *)
> let acq-po = [Acquire] ; po ; [M]
> let po-rel = [M] ; po ; [Release]
> -let rfi-rel-acq = [Release] ; rfi ; [Acquire]
> +let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
>
> (**********************************)
> (* Fundamental coherence ordering *)
> @@ -60,13 +60,13 @@ let dep = addr | data
> let rwdep = (dep | ctrl) ; [W]
> let overwrite = co | fr
> let to-w = rwdep | (overwrite & int)
> -let to-r = addr | (dep ; rfi) | rfi-rel-acq
> +let to-r = addr | (dep ; rfi)
> let fence = strong-fence | wmb | po-rel | rmb | acq-po
> -let ppo = to-r | to-w | fence
> +let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
>
> (* Propagation: Ordering from release operations and strong fences. *)
> let A-cumul(r) = rfe? ; r
> -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
> +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po
> let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
>
> (*
> Index: usb-4.x/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> +++ usb-4.x/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus
> @@ -1,11 +1,10 @@
> C ISA2+pooncelock+pooncelock+pombonce
>
> (*
> - * Result: Sometimes
> + * Result: Never
> *
> - * This test shows that the ordering provided by a lock-protected S
> - * litmus test (P0() and P1()) are not visible to external process P2().
> - * This is likely to change soon.
> + * This test shows that write-write ordering provided by locks
> + * (in P0() and P1()) is visible to external process P2().
> *)
>
> {}
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -28,7 +28,8 @@ Explanation of the Linux-Kernel Memory C
> 20. THE HAPPENS-BEFORE RELATION: hb
> 21. THE PROPAGATES-BEFORE RELATION: pb
> 22. RCU RELATIONS: rcu-link, gp, rscs, rcu-fence, and rb
> - 23. ODDS AND ENDS
> + 23. LOCKING
> + 24. ODDS AND ENDS
>
>
>
> @@ -1067,28 +1068,6 @@ allowing out-of-order writes like this t
> violating the write-write coherence rule by requiring the CPU not to
> send the W write to the memory subsystem at all!)
>
> -There is one last example of preserved program order in the LKMM: when
> -a load-acquire reads from an earlier store-release. For example:
> -
> - smp_store_release(&x, 123);
> - r1 = smp_load_acquire(&x);
> -
> -If the smp_load_acquire() ends up obtaining the 123 value that was
> -stored by the smp_store_release(), the LKMM says that the load must be
> -executed after the store; the store cannot be forwarded to the load.
> -This requirement does not arise from the operational model, but it
> -yields correct predictions on all architectures supported by the Linux
> -kernel, although for differing reasons.
> -
> -On some architectures, including x86 and ARMv8, it is true that the
> -store cannot be forwarded to the load. On others, including PowerPC
> -and ARMv7, smp_store_release() generates object code that starts with
> -a fence and smp_load_acquire() generates object code that ends with a
> -fence. The upshot is that even though the store may be forwarded to
> -the load, it is still true that any instruction preceding the store
> -will be executed before the load or any following instructions, and
> -the store will be executed before any instruction following the load.
> -
>
> AND THEN THERE WAS ALPHA
> ------------------------
> @@ -1766,6 +1745,147 @@ before it does, and the critical section
> grace period does and ends after it does.
>
>
> +LOCKING
> +-------
> +
> +The LKMM includes locking. In fact, there is special code for locking
> +in the formal model, added in order to make tools run faster.
> +However, this special code is intended to be more or less equivalent
> +to concepts we have already covered. A spinlock_t variable is treated
> +the same as an int, and spin_lock(&s) is treated almost the same as:
> +
> + while (cmpxchg_acquire(&s, 0, 1) != 0)
> + cpu_relax();
> +
> +This waits until s is equal to 0 and then atomically sets it to 1,
> +and the read part of the cmpxchg operation acts as an acquire fence.
> +An alternate way to express the same thing would be:
> +
> + r = xchg_acquire(&s, 1);
> +
> +along with a requirement that at the end, r = 0. Similarly,
> +spin_trylock(&s) is treated almost the same as:
> +
> + return !cmpxchg_acquire(&s, 0, 1);
> +
> +which atomically sets s to 1 if it is currently equal to 0 and returns
> +true if it succeeds (the read part of the cmpxchg operation acts as an
> +acquire fence only if the operation is successful). spin_unlock(&s)
> +is treated almost the same as:
> +
> + smp_store_release(&s, 0);
> +
> +The "almost" qualifiers above need some explanation. In the LKMM, the
> +store-release in a spin_unlock() and the load-acquire which forms the
> +first half of the atomic rmw update in a spin_lock() or a successful
> +spin_trylock() -- we can call these things lock-releases and
> +lock-acquires -- have two properties beyond those of ordinary releases
> +and acquires.
> +
> +First, when a lock-acquire reads from a lock-release, the LKMM
> +requires that every instruction po-before the lock-release must
> +execute before any instruction po-after the lock-acquire. This would
> +naturally hold if the release and acquire operations were on different
> +CPUs, but the LKMM says it holds even when they are on the same CPU.
> +For example:
> +
> + int x, y;
> + spinlock_t s;
> +
> + P0()
> + {
> + int r1, r2;
> +
> + spin_lock(&s);
> + r1 = READ_ONCE(x);
> + spin_unlock(&s);
> + spin_lock(&s);
> + r2 = READ_ONCE(y);
> + spin_unlock(&s);
> + }
> +
> + P1()
> + {
> + WRITE_ONCE(y, 1);
> + smp_wmb();
> + WRITE_ONCE(x, 1);
> + }
> +
> +Here the second spin_lock() reads from the first spin_unlock(), and
> +therefore the load of x must execute before the load of y. Thus we
> +cannot have r1 = 1 and r2 = 0 at the end (this is an instance of the
> +MP pattern).
> +
> +This requirement does not apply to ordinary release and acquire
> +fences, only to lock-related operations. For instance, suppose P0()
> +in the example had been written as:
> +
> + P0()
> + {
> + int r1, r2, r3;
> +
> + r1 = READ_ONCE(x);
> + smp_store_release(&s, 1);
> + r3 = smp_load_acquire(&s);
> + r2 = READ_ONCE(y);
> + }
> +
> +Then the CPU would be allowed to forward the s = 1 value from the
> +smp_store_release() to the smp_load_acquire(), executing the
> +instructions in the following order:
> +
> + r3 = smp_load_acquire(&s); // Obtains r3 = 1
> + r2 = READ_ONCE(y);
> + r1 = READ_ONCE(x);
> + smp_store_release(&s, 1); // Value is forwarded
> +
> +and thus it could load y before x, obtaining r2 = 0 and r1 = 1.
> +
> +Second, when a lock-acquire reads from a lock-release, and some other
> +stores W and W' occur po-before the lock-release and po-after the
> +lock-acquire respectively, the LKMM requires that W must propagate to
> +each CPU before W' does. For example, consider:
> +
> + int x, y;
> + spinlock_t x;
> +
> + P0()
> + {
> + spin_lock(&s);
> + WRITE_ONCE(x, 1);
> + spin_unlock(&s);
> + }
> +
> + P1()
> + {
> + int r1;
> +
> + spin_lock(&s);
> + r1 = READ_ONCE(x);
> + WRITE_ONCE(y, 1);
> + spin_unlock(&s);
> + }
> +
> + P2()
> + {
> + int r2, r3;
> +
> + r2 = READ_ONCE(y);
> + smp_rmb();
> + r3 = READ_ONCE(x);
> + }
> +
> +If r1 = 1 at the end then the spin_lock() in P1 must have read from
> +the spin_unlock() in P0. Hence the store to x must propagate to P2
> +before the store to y does, so we cannot have r2 = 1 and r3 = 0.
> +
> +These two special requirements for lock-release and lock-acquire do
> +not arise from the operational model. Nevertheless, kernel developers
> +have come to expect and rely on them because they do hold on all
> +architectures supported by the Linux kernel, albeit for various
> +differing reasons.
> +
> +
> ODDS AND ENDS
> -------------
>
> @@ -1831,26 +1951,6 @@ they behave as follows:
> events and the events preceding them against all po-later
> events.
>
> -The LKMM includes locking. In fact, there is special code for locking
> -in the formal model, added in order to make tools run faster.
> -However, this special code is intended to be exactly equivalent to
> -concepts we have already covered. A spinlock_t variable is treated
> -the same as an int, and spin_lock(&s) is treated the same as:
> -
> - while (cmpxchg_acquire(&s, 0, 1) != 0)
> - cpu_relax();
> -
> -which waits until s is equal to 0 and then atomically sets it to 1,
> -and where the read part of the atomic update is also an acquire fence.
> -An alternate way to express the same thing would be:
> -
> - r = xchg_acquire(&s, 1);
> -
> -along with a requirement that at the end, r = 0. spin_unlock(&s) is
> -treated the same as:
> -
> - smp_store_release(&s, 0);
> -
> Interestingly, RCU and locking each introduce the possibility of
> deadlock. When faced with code sequences such as:
>
>