2018-02-21 08:25:01 +09:00
|
|
|
=====================================
|
|
|
|
|
LINUX KERNEL MEMORY CONSISTENCY MODEL
|
|
|
|
|
=====================================
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
============
|
|
|
|
|
INTRODUCTION
|
|
|
|
|
============
|
|
|
|
|
|
2018-02-21 08:25:01 +09:00
|
|
|
This directory contains the memory consistency model (memory model, for
|
|
|
|
|
short) of the Linux kernel, written in the "cat" language and executable
|
|
|
|
|
by the externally provided "herd7" simulator, which exhaustively explores
|
|
|
|
|
the state space of small litmus tests.
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
In addition, the "klitmus7" tool (also externally provided) may be used
|
|
|
|
|
to convert a litmus test to a Linux kernel module, which in turn allows
|
|
|
|
|
that litmus test to be exercised within the Linux kernel.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
============
|
|
|
|
|
REQUIREMENTS
|
|
|
|
|
============
|
|
|
|
|
|
2019-02-01 01:08:40 +09:00
|
|
|
Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
|
|
|
|
|
downloaded separately:
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
https://github.com/herd/herdtools7
|
|
|
|
|
|
|
|
|
|
See "herdtools7/INSTALL.md" for installation instructions.
|
|
|
|
|
|
2019-02-01 01:08:40 +09:00
|
|
|
Note that although these tools usually provide backwards compatibility,
|
|
|
|
|
this is not absolutely guaranteed. Therefore, if a later version does
|
|
|
|
|
not work, please try using the exact version called out above.
|
|
|
|
|
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
==================
|
|
|
|
|
BASIC USAGE: HERD7
|
|
|
|
|
==================
|
|
|
|
|
|
|
|
|
|
The memory model is used, in conjunction with "herd7", to exhaustively
|
|
|
|
|
explore the state space of small litmus tests.
|
|
|
|
|
|
2018-07-17 03:06:05 +09:00
|
|
|
For example, to run SB+fencembonceonces.litmus against the memory model:
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
2018-07-17 03:06:05 +09:00
|
|
|
$ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
Here is the corresponding output:
|
|
|
|
|
|
2018-07-17 03:06:05 +09:00
|
|
|
Test SB+fencembonceonces Allowed
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
States 3
|
|
|
|
|
0:r0=0; 1:r0=1;
|
|
|
|
|
0:r0=1; 1:r0=0;
|
|
|
|
|
0:r0=1; 1:r0=1;
|
|
|
|
|
No
|
|
|
|
|
Witnesses
|
|
|
|
|
Positive: 0 Negative: 3
|
|
|
|
|
Condition exists (0:r0=0 /\ 1:r0=0)
|
2018-07-17 03:06:05 +09:00
|
|
|
Observation SB+fencembonceonces Never 0 3
|
|
|
|
|
Time SB+fencembonceonces 0.01
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
Hash=d66d99523e2cac6b06e66f4c995ebb48
|
|
|
|
|
|
|
|
|
|
The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
|
|
|
|
|
this litmus test's "exists" clause can not be satisfied.
|
|
|
|
|
|
|
|
|
|
See "herd7 -help" or "herdtools7/doc/" for more information.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
=====================
|
|
|
|
|
BASIC USAGE: KLITMUS7
|
|
|
|
|
=====================
|
|
|
|
|
|
|
|
|
|
The "klitmus7" tool converts a litmus test into a Linux kernel module,
|
|
|
|
|
which may then be loaded and run.
|
|
|
|
|
|
2018-07-17 03:06:05 +09:00
|
|
|
For example, to run SB+fencembonceonces.litmus against hardware:
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
$ mkdir mymodules
|
2018-07-17 03:06:05 +09:00
|
|
|
$ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
$ cd mymodules ; make
|
|
|
|
|
$ sudo sh run.sh
|
|
|
|
|
|
|
|
|
|
The corresponding output includes:
|
|
|
|
|
|
2018-07-17 03:06:05 +09:00
|
|
|
Test SB+fencembonceonces Allowed
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
Histogram (3 states)
|
|
|
|
|
644580 :>0:r0=1; 1:r0=0;
|
|
|
|
|
644328 :>0:r0=0; 1:r0=1;
|
|
|
|
|
711092 :>0:r0=1; 1:r0=1;
|
|
|
|
|
No
|
|
|
|
|
Witnesses
|
|
|
|
|
Positive: 0, Negative: 2000000
|
|
|
|
|
Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
|
|
|
|
|
Hash=d66d99523e2cac6b06e66f4c995ebb48
|
2018-07-17 03:06:05 +09:00
|
|
|
Observation SB+fencembonceonces Never 0 2000000
|
|
|
|
|
Time SB+fencembonceonces 0.16
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
|
|
|
|
|
that during two million trials, the state specified in this litmus
|
|
|
|
|
test's "exists" clause was not reached.
|
|
|
|
|
|
|
|
|
|
And, as with "herd7", please see "klitmus7 -help" or "herdtools7/doc/"
|
|
|
|
|
for more information.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
====================
|
|
|
|
|
DESCRIPTION OF FILES
|
|
|
|
|
====================
|
|
|
|
|
|
|
|
|
|
Documentation/cheatsheet.txt
|
|
|
|
|
Quick-reference guide to the Linux-kernel memory model.
|
|
|
|
|
|
|
|
|
|
Documentation/explanation.txt
|
|
|
|
|
Describes the memory model in detail.
|
|
|
|
|
|
|
|
|
|
Documentation/recipes.txt
|
|
|
|
|
Lists common memory-ordering patterns.
|
|
|
|
|
|
|
|
|
|
Documentation/references.txt
|
|
|
|
|
Provides background reading.
|
|
|
|
|
|
|
|
|
|
linux-kernel.bell
|
|
|
|
|
Categorizes the relevant instructions, including memory
|
|
|
|
|
references, memory barriers, atomic read-modify-write operations,
|
|
|
|
|
lock acquisition/release, and RCU operations.
|
|
|
|
|
|
|
|
|
|
More formally, this file (1) lists the subtypes of the various
|
|
|
|
|
event types used by the memory model and (2) performs RCU
|
|
|
|
|
read-side critical section nesting analysis.
|
|
|
|
|
|
|
|
|
|
linux-kernel.cat
|
|
|
|
|
Specifies what reorderings are forbidden by memory references,
|
|
|
|
|
memory barriers, atomic read-modify-write operations, and RCU.
|
|
|
|
|
|
|
|
|
|
More formally, this file specifies what executions are forbidden
|
|
|
|
|
by the memory model. Allowed executions are those which
|
|
|
|
|
satisfy the model's "coherence", "atomic", "happens-before",
|
|
|
|
|
"propagation", and "rcu" axioms, which are defined in the file.
|
|
|
|
|
|
|
|
|
|
linux-kernel.cfg
|
|
|
|
|
Convenience file that gathers the common-case herd7 command-line
|
|
|
|
|
arguments.
|
|
|
|
|
|
|
|
|
|
linux-kernel.def
|
|
|
|
|
Maps from C-like syntax to herd7's internal litmus-test
|
|
|
|
|
instruction-set architecture.
|
|
|
|
|
|
|
|
|
|
litmus-tests
|
|
|
|
|
Directory containing a few representative litmus tests, which
|
|
|
|
|
are listed in litmus-tests/README. A great deal more litmus
|
|
|
|
|
tests are available at https://github.com/paulmckrcu/litmus.
|
|
|
|
|
|
|
|
|
|
lock.cat
|
|
|
|
|
Provides a front-end analysis of lock acquisition and release,
|
|
|
|
|
for example, associating a lock acquisition with the preceding
|
|
|
|
|
and following releases and checking for self-deadlock.
|
|
|
|
|
|
|
|
|
|
More formally, this file defines a performance-enhanced scheme
|
|
|
|
|
for generation of the possible reads-from and coherence order
|
|
|
|
|
relations on the locking primitives.
|
|
|
|
|
|
|
|
|
|
README
|
|
|
|
|
This file.
|
|
|
|
|
|
tools/memory-model: Add scripts to check github litmus tests
The https://github.com/paulmckrcu/litmus repository contains a large
number of C-language litmus tests that include "Result:" comments
predicting the verification result. This commit adds a number of scripts
that run tests on these litmus tests:
checkghlitmus.sh:
Runs all litmus tests in the https://github.com/paulmckrcu/litmus
archive that are C-language and that have "Result:" comment lines
documenting expected results, comparing the actual results to
those expected. Clones the repository if it has not already
been cloned into the "tools/memory-model/litmus" directory.
initlitmushist.sh
Run all litmus tests having no more than the specified number
of processes given a specified timeout, recording the results in
.litmus.out files. Clones the repository if it has not already
been cloned into the "tools/memory-model/litmus" directory.
newlitmushist.sh
For all new or updated litmus tests having no more than the
specified number of processes given a specified timeout, run
and record the results in .litmus.out files.
checklitmushist.sh
Run all litmus tests having .litmus.out files from previous
initlitmushist.sh or newlitmushist.sh runs, comparing the
herd output to that of the original runs.
The above scripts will run litmus tests concurrently, by default with
one job per available CPU. Giving any of these scripts the --help
argument will cause them to print usage information.
This commit also adds a number of helper scripts that are not intended
to be invoked from the command line:
cmplitmushist.sh: Compare the output of two different runs of the same
litmus test.
judgelitmus.sh: Compare the output of a litmus test to its "Result:"
comment line.
parseargs.sh: Parse command-line arguments.
runlitmushist.sh: Run the litmus tests whose pathnames are provided one
per line on standard input.
While in the area, this commit also makes the existing checklitmus.sh
and checkalllitmus.sh scripts use parseargs.sh in order to provide a
bit of uniformity. In addition, per-litmus-test status output is directed
to stdout, while end-of-test summary information is directed to stderr.
Finally, the error flag standardizes on "!!!" to assist those familiar
with rcutorture output.
The defaults for the parseargs.sh arguments may be overridden by using
environment variables: LKMM_DESTDIR for --destdir, LKMM_HERD_OPTIONS
for --herdoptions, LKMM_JOBS for --jobs, LKMM_PROCS for --procs, and
LKMM_TIMEOUT for --timeout.
[ paulmck: History-check summary-line changes per Alan Stern feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Cc: will.deacon@arm.com
Link: http://lkml.kernel.org/r/20181203230451.28921-2-paulmck@linux.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-12-04 08:04:50 +09:00
|
|
|
scripts Various scripts, see scripts/README.
|
|
|
|
|
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
|
|
|
|
===========
|
|
|
|
|
LIMITATIONS
|
|
|
|
|
===========
|
|
|
|
|
|
2019-06-30 06:10:44 +09:00
|
|
|
The Linux-kernel memory model (LKMM) has the following limitations:
|
|
|
|
|
|
|
|
|
|
1. Compiler optimizations are not accurately modeled. Of course,
|
|
|
|
|
the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
|
|
|
|
|
ability to optimize, but under some circumstances it is possible
|
|
|
|
|
for the compiler to undermine the memory model. For more
|
|
|
|
|
information, see Documentation/explanation.txt (in particular,
|
|
|
|
|
the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
|
|
|
|
|
sections).
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
|
2018-09-27 03:29:19 +09:00
|
|
|
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.
|
|
|
|
|
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
2. Multiple access sizes for a single variable are not supported,
|
|
|
|
|
and neither are misaligned or partially overlapping accesses.
|
|
|
|
|
|
|
|
|
|
3. Exceptions and interrupts are not modeled. In some cases,
|
|
|
|
|
this limitation can be overcome by modeling the interrupt or
|
|
|
|
|
exception with an additional process.
|
|
|
|
|
|
|
|
|
|
4. I/O such as MMIO or DMA is not supported.
|
|
|
|
|
|
|
|
|
|
5. Self-modifying code (such as that found in the kernel's
|
|
|
|
|
alternatives mechanism, function tracer, Berkeley Packet Filter
|
|
|
|
|
JIT compiler, and module loader) is not supported.
|
|
|
|
|
|
|
|
|
|
6. Complete modeling of all variants of atomic read-modify-write
|
|
|
|
|
operations, locking primitives, and RCU is not provided.
|
|
|
|
|
For example, call_rcu() and rcu_barrier() are not supported.
|
|
|
|
|
However, a substantial amount of support is provided for these
|
|
|
|
|
operations, as shown in the linux-kernel.def file.
|
|
|
|
|
|
2018-09-27 03:29:19 +09:00
|
|
|
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().
|
|
|
|
|
|
2018-11-27 07:26:43 +09:00
|
|
|
e. Although sleepable RCU (SRCU) is now modeled, there
|
|
|
|
|
are some subtle differences between its semantics and
|
|
|
|
|
those in the Linux kernel. For example, the kernel
|
|
|
|
|
might interpret the following sequence as two partially
|
|
|
|
|
overlapping SRCU read-side critical sections:
|
|
|
|
|
|
|
|
|
|
1 r1 = srcu_read_lock(&my_srcu);
|
|
|
|
|
2 do_something_1();
|
|
|
|
|
3 r2 = srcu_read_lock(&my_srcu);
|
|
|
|
|
4 do_something_2();
|
|
|
|
|
5 srcu_read_unlock(&my_srcu, r1);
|
|
|
|
|
6 do_something_3();
|
|
|
|
|
7 srcu_read_unlock(&my_srcu, r2);
|
|
|
|
|
|
|
|
|
|
In contrast, LKMM will interpret this as a nested pair of
|
|
|
|
|
SRCU read-side critical sections, with the outer critical
|
|
|
|
|
section spanning lines 1-7 and the inner critical section
|
|
|
|
|
spanning lines 3-5.
|
|
|
|
|
|
|
|
|
|
This difference would be more of a concern had anyone
|
|
|
|
|
identified a reasonable use case for partially overlapping
|
|
|
|
|
SRCU read-side critical sections. For more information,
|
|
|
|
|
please see: https://paulmck.livejournal.com/40593.html
|
2018-09-27 03:29:19 +09:00
|
|
|
|
|
|
|
|
f. Reader-writer locking is not modeled. It can be
|
|
|
|
|
emulated in litmus tests using atomic read-modify-write
|
|
|
|
|
operations.
|
|
|
|
|
|
Automate memory-barriers.txt; provide Linux-kernel memory model
There is some reason to believe that Documentation/memory-barriers.txt
could use some help, and a major purpose of this patch is to provide
that help in the form of a design-time tool that can produce all valid
executions of a small fragment of concurrent Linux-kernel code, which is
called a "litmus test". This tool's functionality is roughly similar to
a full state-space search. Please note that this is a design-time tool,
not useful for regression testing. However, we hope that the underlying
Linux-kernel memory model will be incorporated into other tools capable
of analyzing large bodies of code for regression-testing purposes.
The main tool is herd7, together with the linux-kernel.bell,
linux-kernel.cat, linux-kernel.cfg, linux-kernel.def, and lock.cat files
added by this patch. The herd7 executable takes the other files as input,
and all of these files collectively define the Linux-kernel memory memory
model. A brief description of each of these other files is provided
in the README file. Although this tool does have its limitations,
which are documented in the README file, it does improve on the version
reported on in the LWN series (https://lwn.net/Articles/718628/ and
https://lwn.net/Articles/720550/) by supporting locking and arithmetic,
including a much wider variety of read-modify-write atomic operations.
Please note that herd7 is not part of this submission, but is freely
available from http://diy.inria.fr/sources/index.html (and via "git"
at https://github.com/herd/herdtools7).
A second tool is klitmus7, which converts litmus tests to loadable
kernel modules for direct testing. As with herd7, the klitmus7
code is freely available from http://diy.inria.fr/sources/index.html
(and via "git" at https://github.com/herd/herdtools7).
Of course, litmus tests are not always the best way to fully understand a
memory model, so this patch also includes Documentation/explanation.txt,
which describes the memory model in detail. In addition,
Documentation/recipes.txt provides example known-good and known-bad use
cases for those who prefer working by example.
This patch also includes a few sample litmus tests, and a great many
more litmus tests are available at https://github.com/paulmckrcu/litmus.
This patch was the result of a most excellent collaboration founded
by Jade Alglave and also including Alan Stern, Andrea Parri, and Luc
Maranget. For more details on the history of this collaboration, please
refer to the Linux-kernel memory model presentations at 2016 LinuxCon EU,
2016 Kernel Summit, 2016 Linux Plumbers Conference, 2017 linux.conf.au,
or 2017 Linux Plumbers Conference microconference. However, one aspect
of the history does bear repeating due to weak copyright tracking earlier
in this project, which extends back to early 2015. This weakness came
to light in late 2017 after an LKMM presentation by Paul in which an
audience member noted the similarity of some LKMM code to code in early
published papers. This prompted a copyright review.
From Alan Stern:
To say that the model was mine is not entirely accurate.
Pieces of it (especially the Scpv and Atomic axioms) were taken
directly from Jade's models. And of course the Happens-before
and Propagation relations and axioms were heavily based on
Jade and Luc's work, even though they weren't identical to the
earlier versions. Only the RCU portion was completely original.
. . .
One can make a much better case that I wrote the bulk of lock.cat.
However, it was inspired by Luc's earlier version (and still
shares some elements in common), and of course it benefited from
feedback and testing from all members of our group.
The model prior to Alan's was Luc Maranget's. From Luc:
I totally agree on Alan Stern's account of the linux kernel model
genesis. I thank him for his acknowledgments of my participation
to previous model drafts. I'd like to complete Alan Stern's
statement: any bell cat code I have written has its roots in
discussions with Jade Alglave and Paul McKenney. Moreover I
have borrowed cat and bell code written by Jade Alglave freely.
This copyright review therefore resulted in late adds to the copyright
statements of several files.
Discussion of v1 has raised several issues, which we do not believe should
block acceptance given that this level of change will be ongoing, just
as it has been with memory-barriers.txt:
o Under what conditions should ordering provided by pure locking
be seen by CPUs not holding the relevant lock(s)? In particular,
should the message-passing pattern be forbidden?
o Should examples involving C11 release sequences be forbidden?
Note that this C11 is still a moving target for this issue:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0735r0.html
o Some details of the handling of internal dependencies for atomic
read-modify-write atomic operations are still subject to debate.
o Changes recently accepted into mainline greatly reduce the need
to handle DEC Alpha as a special case. These changes add an
smp_read_barrier_depends() to READ_ONCE(), thus causing Alpha
to respect ordering of dependent reads. If these changes stick,
the memory model can be simplified accordingly.
o Will changes be required to accommodate RISC-V?
Differences from v1:
(http://lkml.kernel.org/r/20171113184031.GA26302@linux.vnet.ibm.com)
o Add SPDX notations to .bell and .cat files, replacing
textual license statements.
o Add reference to upcoming ASPLOS paper to .bell and .cat files.
o Updated identifier names in .bell and .cat files to match those
used in the ASPLOS paper.
o Updates to READMEs and other documentation based on review
feedback.
o Added a memory-ordering cheatsheet.
o Update sigs to new Co-Developed-by and add acks and
reviewed-bys.
o Simplify rules detecting nested RCU read-side critical sections.
o Update copyright statements as noted above.
Co-Developed-by: Alan Stern <stern@rowland.harvard.edu>
Co-Developed-by: Andrea Parri <parri.andrea@gmail.com>
Co-Developed-by: Jade Alglave <j.alglave@ucl.ac.uk>
Co-Developed-by: Luc Maranget <luc.maranget@inria.fr>
Co-Developed-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Jade Alglave <j.alglave@ucl.ac.uk>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Acked-by: Will Deacon <will.deacon@arm.com>
Acked-by: Peter Zijlstra <peterz@infradead.org>
Acked-by: Nicholas Piggin <npiggin@gmail.com>
Acked-by: David Howells <dhowells@redhat.com>
Acked-by: "Reshetova, Elena" <elena.reshetova@intel.com>
Acked-by: Michal Hocko <mhocko@suse.com>
Acked-by: Akira Yokosawa <akiyks@gmail.com>
Cc: <linux-arch@vger.kernel.org>
2018-01-19 12:58:55 +09:00
|
|
|
The "herd7" tool has some additional limitations of its own, apart from
|
|
|
|
|
the memory model:
|
|
|
|
|
|
|
|
|
|
1. Non-trivial data structures such as arrays or structures are
|
|
|
|
|
not supported. However, pointers are supported, allowing trivial
|
|
|
|
|
linked lists to be constructed.
|
|
|
|
|
|
|
|
|
|
2. Dynamic memory allocation is not supported, although this can
|
|
|
|
|
be worked around in some cases by supplying multiple statically
|
|
|
|
|
allocated variables.
|
|
|
|
|
|
|
|
|
|
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.
|
2018-09-27 03:29:19 +09:00
|
|
|
|
|
|
|
|
Finally, please note that LKMM is subject to change as hardware, use cases,
|
|
|
|
|
and compilers evolve.
|