Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Wed, Nov 28, 2018 at 07:34:14AM +0900, Akira Yokosawa wrote: > On 2018/11/27 09:17:46 -0800, Paul E. McKenney wrote: > > On Tue, Nov 27, 2018 at 01:26:42AM +0100, Andrea Parri wrote: > >>> commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 > >>> Author: Paul E. McKenney > >>> Date: Mon Nov 26 14:26:43 2018 -0800 > >>> > >>> tools/memory-model: Update README for addition of SRCU > >>> > >>> This commit updates the section on LKMM limitations to no longer say > >>> that SRCU is not modeled, but instead describe how LKMM's modeling of > >>> SRCU departs from the Linux-kernel implementation. > >>> > >>> TL;DR: There is no known valid use case that cares about the Linux > >>> kernel's ability to have partially overlapping SRCU read-side critical > >>> sections. > >>> > >>> Signed-off-by: Paul E. McKenney > >> > >> Indeed!, > >> > >> Acked-by: Andrea Parri > > > > Thank you, applied! > > > > I moved this commit and Alan's three SRCU commits to the branch destined > > for the upcoming merge window. > > We need to bump the version of herdtools7 in "REQUIREMENTS". Would it be > 7.52? Good catch! And I am currently using 7.51+2(dev), so I suspect that you are right. But 7.52 appears to still be in the future. > Removing the explicit version number might be a better idea. Just > say "The latest version of ...". > > Thoughts? That approach would be easier for us, but might be painful for someone (say) five years from now trying to run the v4.20 kernel's memory model. Thanx, Paul > Thanks, Akira > > > > Thanx, Paul > > > >> Andrea > >> > >> > >>> > >>> diff --git a/tools/memory-model/README b/tools/memory-model/README > >>> index 0f2c366518c6..9d7d4f23503f 100644 > >>> --- a/tools/memory-model/README > >>> +++ b/tools/memory-model/README > >>> @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following > >>> limitations: > >>> additional call_rcu() process to the site of the > >>> emulated rcu-barrier(). > >>> > >>> - e. Sleepable RCU (SRCU) is not modeled. It can be > >>> - emulated, but perhaps not simply. > >>> + 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(_srcu); > >>> + 2 do_something_1(); > >>> + 3 r2 = srcu_read_lock(_srcu); > >>> + 4 do_something_2(); > >>> + 5 srcu_read_unlock(_srcu, r1); > >>> + 6 do_something_3(); > >>> + 7 srcu_read_unlock(_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 > >>> > >>> f. Reader-writer locking is not modeled. It can be > >>> emulated in litmus tests using atomic read-modify-write > >>> > >> > > >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Wed, Nov 28, 2018 at 07:34:14AM +0900, Akira Yokosawa wrote: > On 2018/11/27 09:17:46 -0800, Paul E. McKenney wrote: > > On Tue, Nov 27, 2018 at 01:26:42AM +0100, Andrea Parri wrote: > >>> commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 > >>> Author: Paul E. McKenney > >>> Date: Mon Nov 26 14:26:43 2018 -0800 > >>> > >>> tools/memory-model: Update README for addition of SRCU > >>> > >>> This commit updates the section on LKMM limitations to no longer say > >>> that SRCU is not modeled, but instead describe how LKMM's modeling of > >>> SRCU departs from the Linux-kernel implementation. > >>> > >>> TL;DR: There is no known valid use case that cares about the Linux > >>> kernel's ability to have partially overlapping SRCU read-side critical > >>> sections. > >>> > >>> Signed-off-by: Paul E. McKenney > >> > >> Indeed!, > >> > >> Acked-by: Andrea Parri > > > > Thank you, applied! > > > > I moved this commit and Alan's three SRCU commits to the branch destined > > for the upcoming merge window. > > We need to bump the version of herdtools7 in "REQUIREMENTS". Would it be > 7.52? Good catch! And I am currently using 7.51+2(dev), so I suspect that you are right. But 7.52 appears to still be in the future. > Removing the explicit version number might be a better idea. Just > say "The latest version of ...". > > Thoughts? That approach would be easier for us, but might be painful for someone (say) five years from now trying to run the v4.20 kernel's memory model. Thanx, Paul > Thanks, Akira > > > > Thanx, Paul > > > >> Andrea > >> > >> > >>> > >>> diff --git a/tools/memory-model/README b/tools/memory-model/README > >>> index 0f2c366518c6..9d7d4f23503f 100644 > >>> --- a/tools/memory-model/README > >>> +++ b/tools/memory-model/README > >>> @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following > >>> limitations: > >>> additional call_rcu() process to the site of the > >>> emulated rcu-barrier(). > >>> > >>> - e. Sleepable RCU (SRCU) is not modeled. It can be > >>> - emulated, but perhaps not simply. > >>> + 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(_srcu); > >>> + 2 do_something_1(); > >>> + 3 r2 = srcu_read_lock(_srcu); > >>> + 4 do_something_2(); > >>> + 5 srcu_read_unlock(_srcu, r1); > >>> + 6 do_something_3(); > >>> + 7 srcu_read_unlock(_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 > >>> > >>> f. Reader-writer locking is not modeled. It can be > >>> emulated in litmus tests using atomic read-modify-write > >>> > >> > > >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On 2018/11/27 09:17:46 -0800, Paul E. McKenney wrote: > On Tue, Nov 27, 2018 at 01:26:42AM +0100, Andrea Parri wrote: >>> commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 >>> Author: Paul E. McKenney >>> Date: Mon Nov 26 14:26:43 2018 -0800 >>> >>> tools/memory-model: Update README for addition of SRCU >>> >>> This commit updates the section on LKMM limitations to no longer say >>> that SRCU is not modeled, but instead describe how LKMM's modeling of >>> SRCU departs from the Linux-kernel implementation. >>> >>> TL;DR: There is no known valid use case that cares about the Linux >>> kernel's ability to have partially overlapping SRCU read-side critical >>> sections. >>> >>> Signed-off-by: Paul E. McKenney >> >> Indeed!, >> >> Acked-by: Andrea Parri > > Thank you, applied! > > I moved this commit and Alan's three SRCU commits to the branch destined > for the upcoming merge window. We need to bump the version of herdtools7 in "REQUIREMENTS". Would it be 7.52? Removing the explicit version number might be a better idea. Just say "The latest version of ...". Thoughts? Thanks, Akira > > Thanx, Paul > >> Andrea >> >> >>> >>> diff --git a/tools/memory-model/README b/tools/memory-model/README >>> index 0f2c366518c6..9d7d4f23503f 100644 >>> --- a/tools/memory-model/README >>> +++ b/tools/memory-model/README >>> @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following >>> limitations: >>> additional call_rcu() process to the site of the >>> emulated rcu-barrier(). >>> >>> - e. Sleepable RCU (SRCU) is not modeled. It can be >>> - emulated, but perhaps not simply. >>> + 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(_srcu); >>> +2 do_something_1(); >>> +3 r2 = srcu_read_lock(_srcu); >>> +4 do_something_2(); >>> +5 srcu_read_unlock(_srcu, r1); >>> +6 do_something_3(); >>> +7 srcu_read_unlock(_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 >>> >>> f. Reader-writer locking is not modeled. It can be >>> emulated in litmus tests using atomic read-modify-write >>> >> >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On 2018/11/27 09:17:46 -0800, Paul E. McKenney wrote: > On Tue, Nov 27, 2018 at 01:26:42AM +0100, Andrea Parri wrote: >>> commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 >>> Author: Paul E. McKenney >>> Date: Mon Nov 26 14:26:43 2018 -0800 >>> >>> tools/memory-model: Update README for addition of SRCU >>> >>> This commit updates the section on LKMM limitations to no longer say >>> that SRCU is not modeled, but instead describe how LKMM's modeling of >>> SRCU departs from the Linux-kernel implementation. >>> >>> TL;DR: There is no known valid use case that cares about the Linux >>> kernel's ability to have partially overlapping SRCU read-side critical >>> sections. >>> >>> Signed-off-by: Paul E. McKenney >> >> Indeed!, >> >> Acked-by: Andrea Parri > > Thank you, applied! > > I moved this commit and Alan's three SRCU commits to the branch destined > for the upcoming merge window. We need to bump the version of herdtools7 in "REQUIREMENTS". Would it be 7.52? Removing the explicit version number might be a better idea. Just say "The latest version of ...". Thoughts? Thanks, Akira > > Thanx, Paul > >> Andrea >> >> >>> >>> diff --git a/tools/memory-model/README b/tools/memory-model/README >>> index 0f2c366518c6..9d7d4f23503f 100644 >>> --- a/tools/memory-model/README >>> +++ b/tools/memory-model/README >>> @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following >>> limitations: >>> additional call_rcu() process to the site of the >>> emulated rcu-barrier(). >>> >>> - e. Sleepable RCU (SRCU) is not modeled. It can be >>> - emulated, but perhaps not simply. >>> + 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(_srcu); >>> +2 do_something_1(); >>> +3 r2 = srcu_read_lock(_srcu); >>> +4 do_something_2(); >>> +5 srcu_read_unlock(_srcu, r1); >>> +6 do_something_3(); >>> +7 srcu_read_unlock(_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 >>> >>> f. Reader-writer locking is not modeled. It can be >>> emulated in litmus tests using atomic read-modify-write >>> >> >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Tue, Nov 27, 2018 at 01:26:42AM +0100, Andrea Parri wrote: > > commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 > > Author: Paul E. McKenney > > Date: Mon Nov 26 14:26:43 2018 -0800 > > > > tools/memory-model: Update README for addition of SRCU > > > > This commit updates the section on LKMM limitations to no longer say > > that SRCU is not modeled, but instead describe how LKMM's modeling of > > SRCU departs from the Linux-kernel implementation. > > > > TL;DR: There is no known valid use case that cares about the Linux > > kernel's ability to have partially overlapping SRCU read-side critical > > sections. > > > > Signed-off-by: Paul E. McKenney > > Indeed!, > > Acked-by: Andrea Parri Thank you, applied! I moved this commit and Alan's three SRCU commits to the branch destined for the upcoming merge window. Thanx, Paul > Andrea > > > > > > diff --git a/tools/memory-model/README b/tools/memory-model/README > > index 0f2c366518c6..9d7d4f23503f 100644 > > --- a/tools/memory-model/README > > +++ b/tools/memory-model/README > > @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following > > limitations: > > additional call_rcu() process to the site of the > > emulated rcu-barrier(). > > > > - e. Sleepable RCU (SRCU) is not modeled. It can be > > - emulated, but perhaps not simply. > > + 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(_srcu); > > +2 do_something_1(); > > +3 r2 = srcu_read_lock(_srcu); > > +4 do_something_2(); > > +5 srcu_read_unlock(_srcu, r1); > > +6 do_something_3(); > > +7 srcu_read_unlock(_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 > > > > f. Reader-writer locking is not modeled. It can be > > emulated in litmus tests using atomic read-modify-write > > >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Tue, Nov 27, 2018 at 01:26:42AM +0100, Andrea Parri wrote: > > commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 > > Author: Paul E. McKenney > > Date: Mon Nov 26 14:26:43 2018 -0800 > > > > tools/memory-model: Update README for addition of SRCU > > > > This commit updates the section on LKMM limitations to no longer say > > that SRCU is not modeled, but instead describe how LKMM's modeling of > > SRCU departs from the Linux-kernel implementation. > > > > TL;DR: There is no known valid use case that cares about the Linux > > kernel's ability to have partially overlapping SRCU read-side critical > > sections. > > > > Signed-off-by: Paul E. McKenney > > Indeed!, > > Acked-by: Andrea Parri Thank you, applied! I moved this commit and Alan's three SRCU commits to the branch destined for the upcoming merge window. Thanx, Paul > Andrea > > > > > > diff --git a/tools/memory-model/README b/tools/memory-model/README > > index 0f2c366518c6..9d7d4f23503f 100644 > > --- a/tools/memory-model/README > > +++ b/tools/memory-model/README > > @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following > > limitations: > > additional call_rcu() process to the site of the > > emulated rcu-barrier(). > > > > - e. Sleepable RCU (SRCU) is not modeled. It can be > > - emulated, but perhaps not simply. > > + 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(_srcu); > > +2 do_something_1(); > > +3 r2 = srcu_read_lock(_srcu); > > +4 do_something_2(); > > +5 srcu_read_unlock(_srcu, r1); > > +6 do_something_3(); > > +7 srcu_read_unlock(_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 > > > > f. Reader-writer locking is not modeled. It can be > > emulated in litmus tests using atomic read-modify-write > > >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
> commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 > Author: Paul E. McKenney > Date: Mon Nov 26 14:26:43 2018 -0800 > > tools/memory-model: Update README for addition of SRCU > > This commit updates the section on LKMM limitations to no longer say > that SRCU is not modeled, but instead describe how LKMM's modeling of > SRCU departs from the Linux-kernel implementation. > > TL;DR: There is no known valid use case that cares about the Linux > kernel's ability to have partially overlapping SRCU read-side critical > sections. > > Signed-off-by: Paul E. McKenney Indeed!, Acked-by: Andrea Parri Andrea > > diff --git a/tools/memory-model/README b/tools/memory-model/README > index 0f2c366518c6..9d7d4f23503f 100644 > --- a/tools/memory-model/README > +++ b/tools/memory-model/README > @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following > limitations: > additional call_rcu() process to the site of the > emulated rcu-barrier(). > > - e. Sleepable RCU (SRCU) is not modeled. It can be > - emulated, but perhaps not simply. > + 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(_srcu); > + 2 do_something_1(); > + 3 r2 = srcu_read_lock(_srcu); > + 4 do_something_2(); > + 5 srcu_read_unlock(_srcu, r1); > + 6 do_something_3(); > + 7 srcu_read_unlock(_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 > > f. Reader-writer locking is not modeled. It can be > emulated in litmus tests using atomic read-modify-write >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
> commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 > Author: Paul E. McKenney > Date: Mon Nov 26 14:26:43 2018 -0800 > > tools/memory-model: Update README for addition of SRCU > > This commit updates the section on LKMM limitations to no longer say > that SRCU is not modeled, but instead describe how LKMM's modeling of > SRCU departs from the Linux-kernel implementation. > > TL;DR: There is no known valid use case that cares about the Linux > kernel's ability to have partially overlapping SRCU read-side critical > sections. > > Signed-off-by: Paul E. McKenney Indeed!, Acked-by: Andrea Parri Andrea > > diff --git a/tools/memory-model/README b/tools/memory-model/README > index 0f2c366518c6..9d7d4f23503f 100644 > --- a/tools/memory-model/README > +++ b/tools/memory-model/README > @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following > limitations: > additional call_rcu() process to the site of the > emulated rcu-barrier(). > > - e. Sleepable RCU (SRCU) is not modeled. It can be > - emulated, but perhaps not simply. > + 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(_srcu); > + 2 do_something_1(); > + 3 r2 = srcu_read_lock(_srcu); > + 4 do_something_2(); > + 5 srcu_read_unlock(_srcu, r1); > + 6 do_something_3(); > + 7 srcu_read_unlock(_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 > > f. Reader-writer locking is not modeled. It can be > emulated in litmus tests using atomic read-modify-write >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Mon, Nov 19, 2018 at 01:01:20PM +0100, Andrea Parri wrote: > On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > > Paul and other LKMM maintainers: > > > > The following series of patches adds support for SRCU to the Linux > > Kernel Memory Model. That is, it adds the srcu_read_lock(), > > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > > > Patch 1/3 does some renaming of the RCU parts of the > > memory model's existing CAT code, to help distinguish them > > from the upcoming SRCU parts. > > > > Patch 2/3 refactors the definitions of some RCU relations > > in the CAT code, in a way that the SRCU portions will need. > > > > Patch 3/3 actually adds the SRCU support. > > > > This new code requires herd7 version 7.51+4(dev) or later (now > > available in the herdtools7 github repository) to run. Thanks to Luc > > for making the necessary changes to support SRCU. > > Thank you Alan, Luc. > > My only suggestion is to integrate changes to explanation.txt (in part., > Sect. 22), which the above renaming and refactoring make out-of-date. Also tools/memory-model/README, but please see below. > For this version, > > Tested-by: Andrea Parri Applied to all three, thank you! Thanx, Paul > Andrea > > > > > > The code does not check that the index argument passed to > > srcu_read_unlock() is the same as the value returned by the > > corresponding srcu_read_lock() call. This is deemed to be a semantic > > issue, not directly relevant to the memory model. > > > > Alan commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 Author: Paul E. McKenney Date: Mon Nov 26 14:26:43 2018 -0800 tools/memory-model: Update README for addition of SRCU This commit updates the section on LKMM limitations to no longer say that SRCU is not modeled, but instead describe how LKMM's modeling of SRCU departs from the Linux-kernel implementation. TL;DR: There is no known valid use case that cares about the Linux kernel's ability to have partially overlapping SRCU read-side critical sections. Signed-off-by: Paul E. McKenney diff --git a/tools/memory-model/README b/tools/memory-model/README index 0f2c366518c6..9d7d4f23503f 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following limitations: additional call_rcu() process to the site of the emulated rcu-barrier(). - e. Sleepable RCU (SRCU) is not modeled. It can be - emulated, but perhaps not simply. + 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(_srcu); +2 do_something_1(); +3 r2 = srcu_read_lock(_srcu); +4 do_something_2(); +5 srcu_read_unlock(_srcu, r1); +6 do_something_3(); +7 srcu_read_unlock(_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 f. Reader-writer locking is not modeled. It can be emulated in litmus tests using atomic read-modify-write
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Mon, Nov 19, 2018 at 01:01:20PM +0100, Andrea Parri wrote: > On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > > Paul and other LKMM maintainers: > > > > The following series of patches adds support for SRCU to the Linux > > Kernel Memory Model. That is, it adds the srcu_read_lock(), > > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > > > Patch 1/3 does some renaming of the RCU parts of the > > memory model's existing CAT code, to help distinguish them > > from the upcoming SRCU parts. > > > > Patch 2/3 refactors the definitions of some RCU relations > > in the CAT code, in a way that the SRCU portions will need. > > > > Patch 3/3 actually adds the SRCU support. > > > > This new code requires herd7 version 7.51+4(dev) or later (now > > available in the herdtools7 github repository) to run. Thanks to Luc > > for making the necessary changes to support SRCU. > > Thank you Alan, Luc. > > My only suggestion is to integrate changes to explanation.txt (in part., > Sect. 22), which the above renaming and refactoring make out-of-date. Also tools/memory-model/README, but please see below. > For this version, > > Tested-by: Andrea Parri Applied to all three, thank you! Thanx, Paul > Andrea > > > > > > The code does not check that the index argument passed to > > srcu_read_unlock() is the same as the value returned by the > > corresponding srcu_read_lock() call. This is deemed to be a semantic > > issue, not directly relevant to the memory model. > > > > Alan commit 72f61917f12236514a70017d1ebafb9b8d34a9b6 Author: Paul E. McKenney Date: Mon Nov 26 14:26:43 2018 -0800 tools/memory-model: Update README for addition of SRCU This commit updates the section on LKMM limitations to no longer say that SRCU is not modeled, but instead describe how LKMM's modeling of SRCU departs from the Linux-kernel implementation. TL;DR: There is no known valid use case that cares about the Linux kernel's ability to have partially overlapping SRCU read-side critical sections. Signed-off-by: Paul E. McKenney diff --git a/tools/memory-model/README b/tools/memory-model/README index 0f2c366518c6..9d7d4f23503f 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -221,8 +221,29 @@ The Linux-kernel memory model has the following limitations: additional call_rcu() process to the site of the emulated rcu-barrier(). - e. Sleepable RCU (SRCU) is not modeled. It can be - emulated, but perhaps not simply. + 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(_srcu); +2 do_something_1(); +3 r2 = srcu_read_lock(_srcu); +4 do_something_2(); +5 srcu_read_unlock(_srcu, r1); +6 do_something_3(); +7 srcu_read_unlock(_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 f. Reader-writer locking is not modeled. It can be emulated in litmus tests using atomic read-modify-write
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > Paul and other LKMM maintainers: > > The following series of patches adds support for SRCU to the Linux > Kernel Memory Model. That is, it adds the srcu_read_lock(), > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > Patch 1/3 does some renaming of the RCU parts of the > memory model's existing CAT code, to help distinguish them > from the upcoming SRCU parts. > > Patch 2/3 refactors the definitions of some RCU relations > in the CAT code, in a way that the SRCU portions will need. > > Patch 3/3 actually adds the SRCU support. > > This new code requires herd7 version 7.51+4(dev) or later (now > available in the herdtools7 github repository) to run. Thanks to Luc > for making the necessary changes to support SRCU. Thank you Alan, Luc. My only suggestion is to integrate changes to explanation.txt (in part., Sect. 22), which the above renaming and refactoring make out-of-date. For this version, Tested-by: Andrea Parri Andrea > > The code does not check that the index argument passed to > srcu_read_unlock() is the same as the value returned by the > corresponding srcu_read_lock() call. This is deemed to be a semantic > issue, not directly relevant to the memory model. > > Alan >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > Paul and other LKMM maintainers: > > The following series of patches adds support for SRCU to the Linux > Kernel Memory Model. That is, it adds the srcu_read_lock(), > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > Patch 1/3 does some renaming of the RCU parts of the > memory model's existing CAT code, to help distinguish them > from the upcoming SRCU parts. > > Patch 2/3 refactors the definitions of some RCU relations > in the CAT code, in a way that the SRCU portions will need. > > Patch 3/3 actually adds the SRCU support. > > This new code requires herd7 version 7.51+4(dev) or later (now > available in the herdtools7 github repository) to run. Thanks to Luc > for making the necessary changes to support SRCU. Thank you Alan, Luc. My only suggestion is to integrate changes to explanation.txt (in part., Sect. 22), which the above renaming and refactoring make out-of-date. For this version, Tested-by: Andrea Parri Andrea > > The code does not check that the index argument passed to > srcu_read_unlock() is the same as the value returned by the > corresponding srcu_read_lock() call. This is deemed to be a semantic > issue, not directly relevant to the memory model. > > Alan >
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Thu, 15 Nov 2018, Paul E. McKenney wrote: > On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > > Paul and other LKMM maintainers: > > > > The following series of patches adds support for SRCU to the Linux > > Kernel Memory Model. That is, it adds the srcu_read_lock(), > > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > > > Patch 1/3 does some renaming of the RCU parts of the > > memory model's existing CAT code, to help distinguish them > > from the upcoming SRCU parts. > > > > Patch 2/3 refactors the definitions of some RCU relations > > in the CAT code, in a way that the SRCU portions will need. > > > > Patch 3/3 actually adds the SRCU support. > > > > This new code requires herd7 version 7.51+4(dev) or later (now > > available in the herdtools7 github repository) to run. Thanks to Luc > > for making the necessary changes to support SRCU. > > These patches pass the tests that I have constructed, and also regression > tests, very nice! Applied and pushed, thank you. > > > The code does not check that the index argument passed to > > srcu_read_unlock() is the same as the value returned by the > > corresponding srcu_read_lock() call. This is deemed to be a semantic > > issue, not directly relevant to the memory model. > > Agreed. > > If I understand correctly, there are in theory some use cases that these > patches do not support, for example: > > r1 = srcu_read_lock(a); > do_1(); > r2 = srcu_read_lock(a); > do_2(); > srcu_read_unlock(a, r1); > do_3(); > srcu_read_unlock(a, r2); Yes, this sort of thing will be misinterpreted as two nested critical sections rather than two overlapping critical sections. > In practice, I would be more worried about this had I ever managed to > find a non-bogus use case for this pattern. ;-) The example is also a little difficult for humans to follow, at least without an explanatory comment. Alan
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Thu, 15 Nov 2018, Paul E. McKenney wrote: > On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > > Paul and other LKMM maintainers: > > > > The following series of patches adds support for SRCU to the Linux > > Kernel Memory Model. That is, it adds the srcu_read_lock(), > > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > > > Patch 1/3 does some renaming of the RCU parts of the > > memory model's existing CAT code, to help distinguish them > > from the upcoming SRCU parts. > > > > Patch 2/3 refactors the definitions of some RCU relations > > in the CAT code, in a way that the SRCU portions will need. > > > > Patch 3/3 actually adds the SRCU support. > > > > This new code requires herd7 version 7.51+4(dev) or later (now > > available in the herdtools7 github repository) to run. Thanks to Luc > > for making the necessary changes to support SRCU. > > These patches pass the tests that I have constructed, and also regression > tests, very nice! Applied and pushed, thank you. > > > The code does not check that the index argument passed to > > srcu_read_unlock() is the same as the value returned by the > > corresponding srcu_read_lock() call. This is deemed to be a semantic > > issue, not directly relevant to the memory model. > > Agreed. > > If I understand correctly, there are in theory some use cases that these > patches do not support, for example: > > r1 = srcu_read_lock(a); > do_1(); > r2 = srcu_read_lock(a); > do_2(); > srcu_read_unlock(a, r1); > do_3(); > srcu_read_unlock(a, r2); Yes, this sort of thing will be misinterpreted as two nested critical sections rather than two overlapping critical sections. > In practice, I would be more worried about this had I ever managed to > find a non-bogus use case for this pattern. ;-) The example is also a little difficult for humans to follow, at least without an explanatory comment. Alan
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > Paul and other LKMM maintainers: > > The following series of patches adds support for SRCU to the Linux > Kernel Memory Model. That is, it adds the srcu_read_lock(), > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > Patch 1/3 does some renaming of the RCU parts of the > memory model's existing CAT code, to help distinguish them > from the upcoming SRCU parts. > > Patch 2/3 refactors the definitions of some RCU relations > in the CAT code, in a way that the SRCU portions will need. > > Patch 3/3 actually adds the SRCU support. > > This new code requires herd7 version 7.51+4(dev) or later (now > available in the herdtools7 github repository) to run. Thanks to Luc > for making the necessary changes to support SRCU. These patches pass the tests that I have constructed, and also regression tests, very nice! Applied and pushed, thank you. > The code does not check that the index argument passed to > srcu_read_unlock() is the same as the value returned by the > corresponding srcu_read_lock() call. This is deemed to be a semantic > issue, not directly relevant to the memory model. Agreed. If I understand correctly, there are in theory some use cases that these patches do not support, for example: r1 = srcu_read_lock(a); do_1(); r2 = srcu_read_lock(a); do_2(); srcu_read_unlock(a, r1); do_3(); srcu_read_unlock(a, r2); In practice, I would be more worried about this had I ever managed to find a non-bogus use case for this pattern. ;-) Thanx, Paul
Re: [PATCH 0/3] tools/memory-model: Add SRCU support
On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote: > Paul and other LKMM maintainers: > > The following series of patches adds support for SRCU to the Linux > Kernel Memory Model. That is, it adds the srcu_read_lock(), > srcu_read_unlock(), and synchronize_srcu() primitives to the model. > > Patch 1/3 does some renaming of the RCU parts of the > memory model's existing CAT code, to help distinguish them > from the upcoming SRCU parts. > > Patch 2/3 refactors the definitions of some RCU relations > in the CAT code, in a way that the SRCU portions will need. > > Patch 3/3 actually adds the SRCU support. > > This new code requires herd7 version 7.51+4(dev) or later (now > available in the herdtools7 github repository) to run. Thanks to Luc > for making the necessary changes to support SRCU. These patches pass the tests that I have constructed, and also regression tests, very nice! Applied and pushed, thank you. > The code does not check that the index argument passed to > srcu_read_unlock() is the same as the value returned by the > corresponding srcu_read_lock() call. This is deemed to be a semantic > issue, not directly relevant to the memory model. Agreed. If I understand correctly, there are in theory some use cases that these patches do not support, for example: r1 = srcu_read_lock(a); do_1(); r2 = srcu_read_lock(a); do_2(); srcu_read_unlock(a, r1); do_3(); srcu_read_unlock(a, r2); In practice, I would be more worried about this had I ever managed to find a non-bogus use case for this pattern. ;-) Thanx, Paul
