From: Alan Stern <stern@rowland.harvard.edu> To: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: David Goldblatt <davidtgoldblatt@gmail.com>, <mathieu.desnoyers@efficios.com>, Florian Weimer <fweimer@redhat.com>, <triegel@redhat.com>, <libc-alpha@sourceware.org>, <andrea.parri@amarulasolutions.com>, <will.deacon@arm.com>, <peterz@infradead.org>, <boqun.feng@gmail.com>, <npiggin@gmail.com>, <dhowells@redhat.com>, <j.alglave@ucl.ac.uk>, <luc.maranget@inria.fr>, <akiyks@gmail.com>, <dlustig@nvidia.com>, <linux-arch@vger.kernel.org>, <linux-kernel@vger.kernel.org> Subject: Re: [PATCH] Linux: Implement membarrier function Date: Thu, 13 Dec 2018 10:49:49 -0500 (EST) [thread overview] Message-ID: <Pine.LNX.4.44L0.1812131026570.1586-100000@iolanthe.rowland.org> (raw) In-Reply-To: <20181212224931.GD4170@linux.ibm.com> On Wed, 12 Dec 2018, Paul E. McKenney wrote: > > Well, what are you trying to accomplish? Do you want to find an > > argument similar to the one I posted for the 6-CPU test to show that > > this test should be forbidden? > > I am trying to check odd corner cases. Your sys_membarrier() model > is quite nice and certainly fits nicely with the rest of the model, > but where I come from, that is actually reason for suspicion. ;-) > > All kidding aside, your argument for the 6-CPU test was extremely > valuable, as it showed me a way to think of that test from an > implementation viewpoint. Then the question is whether or not that > viewpoint actually matches the model, which seems to be the case thus far. It should, since I formulated the reasoning behind that viewpoint directly from the model. The basic idea is this: By induction, show that whenever we have A ->rcu-fence B then anything po-before A executes before anything po-after B, and furthermore, any write which propagates to A's CPU before A executes will propagate to every CPU before B finishes (i.e., before anything po-after B executes). Using this, show that whenever X ->rb Y holds then X must execute before Y. That's what the 6-CPU argument did. In that litmus test we have mb2 ->rcu-fence mb23, Rc ->rb Re, mb1 ->rcu-fence mb14, Rb ->rb Rf, mb0 ->rcu-fence mb05, and lastly Ra ->rb Ra. The last one is what shows that the test is forbidden. > A good next step would be to automatically generate random tests along > with an automatically generated prediction, like I did for RCU a few > years back. I should be able to generalize my time-based cheat for RCU to > also cover SRCU, though sys_membarrier() will require a bit more thought. > (The time-based cheat was to have fixed duration RCU grace periods and > RCU read-side critical sections, with the grace period duration being > slightly longer than that of the critical sections. The number of > processes is of course limited by the chosen durations, but that limit > can easily be made insanely large.) Imagine that each sys_membarrier call takes a fixed duration and each other instruction takes slightly less (the idea being that each instruction is a critical section). Instructions can be reordered (although not across a sys_membarrier call), but no matter how the reordering is done, the result is disallowed. > I guess that I still haven't gotten over being a bit surprised that the > RCU counting rule also applies to sys_membarrier(). ;-) Why not? They are both synchronization mechanisms with heavy-weight write sides and light-weight read sides, and most importantly, they provide the same Guarantee. Alan
WARNING: multiple messages have this Message-ID (diff)
From: Alan Stern <stern@rowland.harvard.edu> To: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: David Goldblatt <davidtgoldblatt@gmail.com>, mathieu.desnoyers@efficios.com, Florian Weimer <fweimer@redhat.com>, triegel@redhat.com, libc-alpha@sourceware.org, andrea.parri@amarulasolutions.com, will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com, linux-arch@vger.kernel.org, linux-kernel@vger.kernel.org Subject: Re: [PATCH] Linux: Implement membarrier function Date: Thu, 13 Dec 2018 10:49:49 -0500 (EST) [thread overview] Message-ID: <Pine.LNX.4.44L0.1812131026570.1586-100000@iolanthe.rowland.org> (raw) In-Reply-To: <20181212224931.GD4170@linux.ibm.com> On Wed, 12 Dec 2018, Paul E. McKenney wrote: > > Well, what are you trying to accomplish? Do you want to find an > > argument similar to the one I posted for the 6-CPU test to show that > > this test should be forbidden? > > I am trying to check odd corner cases. Your sys_membarrier() model > is quite nice and certainly fits nicely with the rest of the model, > but where I come from, that is actually reason for suspicion. ;-) > > All kidding aside, your argument for the 6-CPU test was extremely > valuable, as it showed me a way to think of that test from an > implementation viewpoint. Then the question is whether or not that > viewpoint actually matches the model, which seems to be the case thus far. It should, since I formulated the reasoning behind that viewpoint directly from the model. The basic idea is this: By induction, show that whenever we have A ->rcu-fence B then anything po-before A executes before anything po-after B, and furthermore, any write which propagates to A's CPU before A executes will propagate to every CPU before B finishes (i.e., before anything po-after B executes). Using this, show that whenever X ->rb Y holds then X must execute before Y. That's what the 6-CPU argument did. In that litmus test we have mb2 ->rcu-fence mb23, Rc ->rb Re, mb1 ->rcu-fence mb14, Rb ->rb Rf, mb0 ->rcu-fence mb05, and lastly Ra ->rb Ra. The last one is what shows that the test is forbidden. > A good next step would be to automatically generate random tests along > with an automatically generated prediction, like I did for RCU a few > years back. I should be able to generalize my time-based cheat for RCU to > also cover SRCU, though sys_membarrier() will require a bit more thought. > (The time-based cheat was to have fixed duration RCU grace periods and > RCU read-side critical sections, with the grace period duration being > slightly longer than that of the critical sections. The number of > processes is of course limited by the chosen durations, but that limit > can easily be made insanely large.) Imagine that each sys_membarrier call takes a fixed duration and each other instruction takes slightly less (the idea being that each instruction is a critical section). Instructions can be reordered (although not across a sys_membarrier call), but no matter how the reordering is done, the result is disallowed. > I guess that I still haven't gotten over being a bit surprised that the > RCU counting rule also applies to sys_membarrier(). ;-) Why not? They are both synchronization mechanisms with heavy-weight write sides and light-weight read sides, and most importantly, they provide the same Guarantee. Alan
next prev parent reply other threads:[~2018-12-13 15:49 UTC|newest] Thread overview: 38+ messages / expand[flat|nested] mbox.gz Atom feed top [not found] <8736rldyzm.fsf@oldenburg.str.redhat.com> [not found] ` <1543444466.5493.220.camel@redhat.com> [not found] ` <87y39c2dsg.fsf@oldenburg.str.redhat.com> [not found] ` <1689938209.14804.1543502662882.JavaMail.zimbra@efficios.com> [not found] ` <20181129150433.GH4170@linux.ibm.com> [not found] ` <CAHD6eXcvx1bskbp-X+vuMYoMQiCLOt0PiCZ5FT1yFsda9Ud-yA@mail.gmail.com> 2018-12-06 21:54 ` [PATCH] Linux: Implement membarrier function Paul E. McKenney 2018-12-10 16:22 ` Alan Stern 2018-12-10 16:22 ` Alan Stern 2018-12-10 18:25 ` Paul E. McKenney 2018-12-11 16:21 ` Alan Stern 2018-12-11 16:21 ` Alan Stern 2018-12-11 19:08 ` Paul E. McKenney 2018-12-11 20:09 ` Alan Stern 2018-12-11 20:09 ` Alan Stern 2018-12-11 21:22 ` Paul E. McKenney 2018-12-12 17:07 ` Paul E. McKenney 2018-12-12 18:04 ` Alan Stern 2018-12-12 18:04 ` Alan Stern 2018-12-12 19:42 ` Paul E. McKenney 2018-12-12 21:32 ` Alan Stern 2018-12-12 21:32 ` Alan Stern 2018-12-12 21:52 ` Paul E. McKenney 2018-12-12 22:12 ` Alan Stern 2018-12-12 22:12 ` Alan Stern 2018-12-12 22:49 ` Paul E. McKenney 2018-12-13 15:49 ` Alan Stern [this message] 2018-12-13 15:49 ` Alan Stern 2018-12-14 0:20 ` Paul E. McKenney 2018-12-14 2:26 ` Alan Stern 2018-12-14 2:26 ` Alan Stern 2018-12-14 5:20 ` Paul E. McKenney 2018-12-14 15:31 ` Alan Stern 2018-12-14 15:31 ` Alan Stern 2018-12-14 18:43 ` Paul E. McKenney 2018-12-14 21:39 ` Alan Stern 2018-12-14 21:39 ` Alan Stern 2018-12-16 18:51 ` Paul E. McKenney 2018-12-17 16:02 ` Alan Stern 2018-12-17 16:02 ` Alan Stern 2018-12-17 18:32 ` Paul E. McKenney 2018-12-12 22:19 ` Paul E. McKenney 2018-12-11 6:42 ` David Goldblatt 2018-12-11 14:49 ` Paul E. McKenney
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=Pine.LNX.4.44L0.1812131026570.1586-100000@iolanthe.rowland.org \ --to=stern@rowland.harvard.edu \ --cc=akiyks@gmail.com \ --cc=andrea.parri@amarulasolutions.com \ --cc=boqun.feng@gmail.com \ --cc=davidtgoldblatt@gmail.com \ --cc=dhowells@redhat.com \ --cc=dlustig@nvidia.com \ --cc=fweimer@redhat.com \ --cc=j.alglave@ucl.ac.uk \ --cc=libc-alpha@sourceware.org \ --cc=linux-arch@vger.kernel.org \ --cc=linux-kernel@vger.kernel.org \ --cc=luc.maranget@inria.fr \ --cc=mathieu.desnoyers@efficios.com \ --cc=npiggin@gmail.com \ --cc=paulmck@linux.ibm.com \ --cc=peterz@infradead.org \ --cc=triegel@redhat.com \ --cc=will.deacon@arm.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes, see mirroring instructions on how to clone and mirror all data and code used by this external index.