On Mon, Dec 17, 2018 at 11:02:40AM -0500, Alan Stern wrote:
> On Sun, 16 Dec 2018, Paul E. McKenney wrote:
>
> > OK, so "simultaneous" IPIs could be emulated in a real implementation by
> > having sys_membarrier() send each IPI (but not wait for a response), then
> > execute a full memory barrier
On Sun, 16 Dec 2018, Paul E. McKenney wrote:
> OK, so "simultaneous" IPIs could be emulated in a real implementation by
> having sys_membarrier() send each IPI (but not wait for a response), then
> execute a full memory barrier and set a shared variable. Each IPI handler
> would spin waiting for
On Fri, Dec 14, 2018 at 04:39:34PM -0500, Alan Stern wrote:
> On Fri, 14 Dec 2018, Paul E. McKenney wrote:
>
> > I would say that sys_membarrier() has zero-sized read-side critical
> > sections, either comprising a single instruction (as is the case for
> > synchronize_sched(), actually),
On Fri, 14 Dec 2018, Paul E. McKenney wrote:
> I would say that sys_membarrier() has zero-sized read-side critical
> sections, either comprising a single instruction (as is the case for
> synchronize_sched(), actually), preempt-disable regions of code
> (which are irrelevant to userspace
On Fri, Dec 14, 2018 at 10:31:51AM -0500, Alan Stern wrote:
> On Thu, 13 Dec 2018, Paul E. McKenney wrote:
>
> > > > 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
On Thu, 13 Dec 2018, Paul E. McKenney wrote:
> > > 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
On Thu, Dec 13, 2018 at 09:26:47PM -0500, Alan Stern wrote:
> On Thu, 13 Dec 2018, Paul E. McKenney wrote:
>
> > > > 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
On Thu, 13 Dec 2018, Paul E. McKenney wrote:
> > > 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
On Thu, Dec 13, 2018 at 10:49:49AM -0500, Alan Stern wrote:
> 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?
> >
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
On Wed, Dec 12, 2018 at 05:12:18PM -0500, Alan Stern wrote:
> On Wed, 12 Dec 2018, Paul E. McKenney wrote:
>
> > > > I believe that this ordering forbids the cycle:
> > > >
> > > > Wa=1 > membs -> [m01] -> Rc=0 -> Wc=2 -> rcu_read_unlock() ->
> > > > return from
On Wed, Dec 12, 2018 at 01:52:45PM -0800, Paul E. McKenney wrote:
> On Wed, Dec 12, 2018 at 04:32:50PM -0500, Alan Stern wrote:
> > On Wed, 12 Dec 2018, Paul E. McKenney wrote:
> >
> > > OK. How about this one?
> > >
> > > P0 P1 P2 P3
> > > Wa=2
On Wed, 12 Dec 2018, Paul E. McKenney wrote:
> > > I believe that this ordering forbids the cycle:
> > >
> > > Wa=1 > membs -> [m01] -> Rc=0 -> Wc=2 -> rcu_read_unlock() ->
> > > return from synchronize_rcu() -> Ra
> > >
> > > Does this make sense, or am I missing something?
> >
>
On Wed, Dec 12, 2018 at 04:32:50PM -0500, Alan Stern wrote:
> On Wed, 12 Dec 2018, Paul E. McKenney wrote:
>
> > OK. How about this one?
> >
> > P0 P1 P2 P3
> > Wa=2rcu_read_lock()Wc=2Wd=2
> > membWb=2 Rd=0
On Wed, 12 Dec 2018, Paul E. McKenney wrote:
> OK. How about this one?
>
> P0 P1 P2 P3
> Wa=2rcu_read_lock()Wc=2Wd=2
> membWb=2 Rd=0synchronize_rcu();
> Rb=0Rc=0 Ra=0
>
On Wed, Dec 12, 2018 at 01:04:44PM -0500, Alan Stern wrote:
> On Wed, 12 Dec 2018, Paul E. McKenney wrote:
>
> > > > > Or am I still missing something here?
> > > >
> > > > You tell me...
> > >
> > > I think I am on board. ;-)
> >
> > And more to the point, here is a three-process variant
On Wed, 12 Dec 2018, Paul E. McKenney wrote:
> > > > Or am I still missing something here?
> > >
> > > You tell me...
> >
> > I think I am on board. ;-)
>
> And more to the point, here is a three-process variant showing a cycle
> that is permitted:
>
>
> P0 P1 P2
>
On Tue, Dec 11, 2018 at 01:22:04PM -0800, Paul E. McKenney wrote:
> On Tue, Dec 11, 2018 at 03:09:33PM -0500, Alan Stern wrote:
> > On Tue, 11 Dec 2018, Paul E. McKenney wrote:
> >
> > > > Rewriting the litmus test in these terms gives:
> > > >
> > > > P0 P1 P2 P3 P4
On Tue, Dec 11, 2018 at 03:09:33PM -0500, Alan Stern wrote:
> On Tue, 11 Dec 2018, Paul E. McKenney wrote:
>
> > > Rewriting the litmus test in these terms gives:
> > >
> > > P0 P1 P2 P3 P4 P5
> > > Wa=2Wb=2Wc=2[mb23] [mb14] [mb05]
> > >
On Tue, 11 Dec 2018, Paul E. McKenney wrote:
> > Rewriting the litmus test in these terms gives:
> >
> > P0 P1 P2 P3 P4 P5
> > Wa=2Wb=2Wc=2[mb23] [mb14] [mb05]
> > mb0smb1smb2sWd=2We=2Wf=2
> > mb0emb1e
On Tue, Dec 11, 2018 at 11:21:15AM -0500, Alan Stern wrote:
> On Mon, 10 Dec 2018, Paul E. McKenney wrote:
>
> > On Mon, Dec 10, 2018 at 11:22:31AM -0500, Alan Stern wrote:
> > > On Thu, 6 Dec 2018, Paul E. McKenney wrote:
> > >
> > > > Hello, David,
> > > >
> > > > I took a crack at extending
On Mon, 10 Dec 2018, Paul E. McKenney wrote:
> On Mon, Dec 10, 2018 at 11:22:31AM -0500, Alan Stern wrote:
> > On Thu, 6 Dec 2018, Paul E. McKenney wrote:
> >
> > > Hello, David,
> > >
> > > I took a crack at extending LKMM to accommodate what I think would
> > > support what you have in your
On Mon, Dec 10, 2018 at 10:42:25PM -0800, David Goldblatt wrote:
> Hi Paul, thank you for thinking about all this.
>
> I think the modelling you suggest captures most of the algorithms I
> would want to write. I think it's slightly too weak, though, to
> implement the model suggested in
Hi Paul, thank you for thinking about all this.
I think the modelling you suggest captures most of the algorithms I
would want to write. I think it's slightly too weak, though, to
implement the model suggested in P1202R0[1], which permits the SC
outcome to be recovered in C-Goldblat-memb-2[2] by
On Mon, Dec 10, 2018 at 11:22:31AM -0500, Alan Stern wrote:
> On Thu, 6 Dec 2018, Paul E. McKenney wrote:
>
> > Hello, David,
> >
> > I took a crack at extending LKMM to accommodate what I think would
> > support what you have in your paper. Please see the very end of this
> > email for a patch
On Thu, 6 Dec 2018, Paul E. McKenney wrote:
> Hello, David,
>
> I took a crack at extending LKMM to accommodate what I think would
> support what you have in your paper. Please see the very end of this
> email for a patch against the "dev" branch of my -rcu tree.
>
> This gives the expected
Hello, David,
I took a crack at extending LKMM to accommodate what I think would
support what you have in your paper. Please see the very end of this
email for a patch against the "dev" branch of my -rcu tree.
This gives the expected result for the following three litmus tests,
but is probably
Hello, David,
I took a crack at extending LKMM to accommodate what I think would
support what you have in your paper. Please see the very end of this
email for a patch against the "dev" branch of my -rcu tree.
This gives the expected result for the following three litmus tests,
but is probably
28 matches
Mail list logo
