From mboxrd@z Thu Jan 1 00:00:00 1970 From: Joel Fernandes Subject: Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link Date: Mon, 29 Jul 2019 08:17:45 -0400 Message-ID: <20190729121745.GA140682@google.com> References: <20190728031303.164545-1-joel@joelfernandes.org> <20190728151959.GA82871@google.com> <20190728152806.GB26905@tardis> <20190728153544.GA87531@google.com> <20190729055044.GC26905@tardis> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Return-path: Content-Disposition: inline In-Reply-To: <20190729055044.GC26905@tardis> Sender: linux-kernel-owner@vger.kernel.org To: Boqun Feng Cc: Alan Stern , linux-kernel@vger.kernel.org, kernel-team@android.com, Akira Yokosawa , Andrea Parri , Daniel Lustig , David Howells , Ingo Molnar , Jade Alglave , linux-arch@vger.kernel.org, Luc Maranget , Nicholas Piggin , "Paul E. McKenney" , Peter Zijlstra , Will Deacon List-Id: linux-arch.vger.kernel.org On Mon, Jul 29, 2019 at 01:50:44PM +0800, Boqun Feng wrote: > On Sun, Jul 28, 2019 at 11:35:44AM -0400, Joel Fernandes wrote: > [...] > > > > > > +load of y (rfe link), P2's smp_store_release() ensures that P2's load > > > > > > +of y executes before P2's store to z (second fence), which implies that > > > > > > +that stores to x and y propagate to P2 before the smp_store_release(), which > > > > > > +means that P2's smp_store_release() will propagate stores to x and y to all > > > > > > +CPUs before the store to z propagates (A-cumulative property of this fence). > > > > > > +Finally P0's load of z executes after P2's store to z has propagated to > > > > > > +P0 (rfe link). > > > > > > > > > > Again, a better change would be simply to replace the two instances of > > > > > "fence" in the original text with "cumul-fence". > > > > > > > > Ok that's fine. But I still feel the rfe is not a part of the cumul-fence. > > > > The fences have nothing to do with the rfe. Or, I am missing something quite > > > > badly. > > > > > > > > Boqun, did you understand what Alan is saying? > > > > > > > > > > I think 'cumul-fence' that Alan mentioned is not a fence, but a > > > relation, which could be the result of combining a rfe relation and a > > > A-cumulative fence relation. Please see the section "PROPAGATION ORDER > > > RELATION: cumul-fence" or the definition of cumul-fence in > > > linux-kernel.cat. > > > > > > Did I get you right, Alan? If so, your suggestion is indeed a better > > > change. > > > > To be frank, I don't think it is better if that's what Alan meant. It is > > better to be explicit about the ->rfe so that the reader walking through the > > example can clearly see the ordering and make sense of it. > > > > Just saying 'cumul-fence' and then hoping the reader sees the light is quite > > a big assumption and makes the document less readable. > > > > After a bit more rereading of the document, I still think Alan's way is > better ;-) I think I finally understood. What I was missing was this definition of cumul-fence involves an rf relation (with writes being possibly on different CPUs). E ->cumul-fence F F is a release fence and some X comes before F in program order, where either X = E or else E ->rf X; or So I think what Alan meant is there is a cumul-fence between y=1 and z=1 because fo the ->rfe of y. Thus making it not necessary to mention the rfe. Labeling E and F in the example... P1() { WRITE_ONCE(x, 2); smp_wmb(); WRITE_ONCE(y, 1); // This is E } P2() { int r2; r2 = READ_ONCE(y); // This is X smp_store_release(&z, 1); // This is F } Here, E ->rf X ->release-fence -> F implies, E ->cumul-fence F Considering that, I agree with Alan's suggestion. > > The formal definition of the prop relation involves a coe or > fre link, followed by an arbitrary number of cumul-fence links, > ending with an rfe link. > > , so using "cumul-fence" actually matches the definition of ->prop. > > For the ease of readers, I can think of two ways: > > 1. Add a backwards reference to cumul-fence section here, right > before using its name. Instead of that, a reference to the fact that the rfe causes a cumul-fence between y=1 and z=1 may be helpful. No need backward reference IMO. > 2. Use "->cumul-fence" notation rather than "cumul-fence" here, > i.e. add an arrow "->" before the name to call it out that name > "cumul-fence" here stands for links/relations rather than a > fence/barrier. Maybe it's better to convert all references to > links/relations to the "->" notations in the whole doc. No, it is a fence that causes the relation in this example. I don't think there is a distinction between ->cumul-fence and cumul-fence at least for this example. The smp_store_release() is a FENCE which in this example is really a cumul-fence between y=1 and z=1 because the release fence affects propogation order of y and z on all CPUs. For any given CPU, y propagates to that CPU before z does, even though y and z executed on different CPUs. I think what you're talking about is some other definition of cumul-fence that is not mentioned in the formal definitions. May be you can update the document with such definition then? AFAIU, cumul-fence is always a fence. thanks, - Joel From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-pf1-f196.google.com ([209.85.210.196]:43599 "EHLO mail-pf1-f196.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1727302AbfG2MRt (ORCPT ); Mon, 29 Jul 2019 08:17:49 -0400 Received: by mail-pf1-f196.google.com with SMTP id i189so27953473pfg.10 for ; Mon, 29 Jul 2019 05:17:48 -0700 (PDT) Date: Mon, 29 Jul 2019 08:17:45 -0400 From: Joel Fernandes Subject: Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link Message-ID: <20190729121745.GA140682@google.com> References: <20190728031303.164545-1-joel@joelfernandes.org> <20190728151959.GA82871@google.com> <20190728152806.GB26905@tardis> <20190728153544.GA87531@google.com> <20190729055044.GC26905@tardis> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20190729055044.GC26905@tardis> Sender: linux-arch-owner@vger.kernel.org List-ID: To: Boqun Feng Cc: Alan Stern , linux-kernel@vger.kernel.org, kernel-team@android.com, Akira Yokosawa , Andrea Parri , Daniel Lustig , David Howells , Ingo Molnar , Jade Alglave , linux-arch@vger.kernel.org, Luc Maranget , Nicholas Piggin , "Paul E. McKenney" , Peter Zijlstra , Will Deacon Message-ID: <20190729121745.tiM7aMWvpV5R5MV9_B8UC9cjvVhNDVSIAIttBcQi-ek@z> On Mon, Jul 29, 2019 at 01:50:44PM +0800, Boqun Feng wrote: > On Sun, Jul 28, 2019 at 11:35:44AM -0400, Joel Fernandes wrote: > [...] > > > > > > +load of y (rfe link), P2's smp_store_release() ensures that P2's load > > > > > > +of y executes before P2's store to z (second fence), which implies that > > > > > > +that stores to x and y propagate to P2 before the smp_store_release(), which > > > > > > +means that P2's smp_store_release() will propagate stores to x and y to all > > > > > > +CPUs before the store to z propagates (A-cumulative property of this fence). > > > > > > +Finally P0's load of z executes after P2's store to z has propagated to > > > > > > +P0 (rfe link). > > > > > > > > > > Again, a better change would be simply to replace the two instances of > > > > > "fence" in the original text with "cumul-fence". > > > > > > > > Ok that's fine. But I still feel the rfe is not a part of the cumul-fence. > > > > The fences have nothing to do with the rfe. Or, I am missing something quite > > > > badly. > > > > > > > > Boqun, did you understand what Alan is saying? > > > > > > > > > > I think 'cumul-fence' that Alan mentioned is not a fence, but a > > > relation, which could be the result of combining a rfe relation and a > > > A-cumulative fence relation. Please see the section "PROPAGATION ORDER > > > RELATION: cumul-fence" or the definition of cumul-fence in > > > linux-kernel.cat. > > > > > > Did I get you right, Alan? If so, your suggestion is indeed a better > > > change. > > > > To be frank, I don't think it is better if that's what Alan meant. It is > > better to be explicit about the ->rfe so that the reader walking through the > > example can clearly see the ordering and make sense of it. > > > > Just saying 'cumul-fence' and then hoping the reader sees the light is quite > > a big assumption and makes the document less readable. > > > > After a bit more rereading of the document, I still think Alan's way is > better ;-) I think I finally understood. What I was missing was this definition of cumul-fence involves an rf relation (with writes being possibly on different CPUs). E ->cumul-fence F F is a release fence and some X comes before F in program order, where either X = E or else E ->rf X; or So I think what Alan meant is there is a cumul-fence between y=1 and z=1 because fo the ->rfe of y. Thus making it not necessary to mention the rfe. Labeling E and F in the example... P1() { WRITE_ONCE(x, 2); smp_wmb(); WRITE_ONCE(y, 1); // This is E } P2() { int r2; r2 = READ_ONCE(y); // This is X smp_store_release(&z, 1); // This is F } Here, E ->rf X ->release-fence -> F implies, E ->cumul-fence F Considering that, I agree with Alan's suggestion. > > The formal definition of the prop relation involves a coe or > fre link, followed by an arbitrary number of cumul-fence links, > ending with an rfe link. > > , so using "cumul-fence" actually matches the definition of ->prop. > > For the ease of readers, I can think of two ways: > > 1. Add a backwards reference to cumul-fence section here, right > before using its name. Instead of that, a reference to the fact that the rfe causes a cumul-fence between y=1 and z=1 may be helpful. No need backward reference IMO. > 2. Use "->cumul-fence" notation rather than "cumul-fence" here, > i.e. add an arrow "->" before the name to call it out that name > "cumul-fence" here stands for links/relations rather than a > fence/barrier. Maybe it's better to convert all references to > links/relations to the "->" notations in the whole doc. No, it is a fence that causes the relation in this example. I don't think there is a distinction between ->cumul-fence and cumul-fence at least for this example. The smp_store_release() is a FENCE which in this example is really a cumul-fence between y=1 and z=1 because the release fence affects propogation order of y and z on all CPUs. For any given CPU, y propagates to that CPU before z does, even though y and z executed on different CPUs. I think what you're talking about is some other definition of cumul-fence that is not mentioned in the formal definitions. May be you can update the document with such definition then? AFAIU, cumul-fence is always a fence. thanks, - Joel