[PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Joel Fernandes (Google)]

The lkmm example about ->prop relation should describe an additional rfe
link between P1's store to y and P2's load of y, which should be
critical to establishing the ordering resulting in the ->prop ordering
on P0. IOW, there are 2 rfe links, not one.

Correct these in the docs to make the ->prop ordering on P0 more clear.

Cc: kernel-team@android.com
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
---
 .../memory-model/Documentation/explanation.txt  | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 68caa9a976d0..aa84fce854cc 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -1302,8 +1302,8 @@ followed by an arbitrary number of cumul-fence links, ending with an
 rfe link.  You can concoct more exotic examples, containing more than
 one fence, although this quickly leads to diminishing returns in terms
 of complexity.  For instance, here's an example containing a coe link
-followed by two fences and an rfe link, utilizing the fact that
-release fences are A-cumulative:
+followed by a fence, an rfe link, another fence and and a final rfe link,
+utilizing the fact that release fences are A-cumulative:
 
 	int x, y, z;
 
@@ -1334,11 +1334,14 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
 link from P0's store to its load.  This is because P0's store gets
 overwritten by P1's store since x = 2 at the end (a coe link), the
 smp_wmb() ensures that P1's store to x propagates to P2 before the
-store to y does (the first fence), the store to y propagates to P2
-before P2's load and store execute, P2's smp_store_release()
-guarantees that the stores to x and y both propagate to P0 before the
-store to z does (the second fence), and P0's load executes after the
-store to z has propagated to P0 (an rfe link).
+store to y does (the first fence), P2's store to y happens before P2's
+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).
 
 In summary, the fact that the hb relation links memory access events
 in the order they execute means that it must not have cycles.  This
-- 
2.22.0.709.g102302147b-goog

Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Alan Stern]

On Sat, 27 Jul 2019, Joel Fernandes (Google) wrote:

> The lkmm example about ->prop relation should describe an additional rfe
> link between P1's store to y and P2's load of y, which should be
> critical to establishing the ordering resulting in the ->prop ordering
> on P0. IOW, there are 2 rfe links, not one.
> 
> Correct these in the docs to make the ->prop ordering on P0 more clear.
> 
> Cc: kernel-team@android.com
> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
> Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> ---

This is not a good update.  See below...

>  .../memory-model/Documentation/explanation.txt  | 17 ++++++++++-------
>  1 file changed, 10 insertions(+), 7 deletions(-)
> 
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 68caa9a976d0..aa84fce854cc 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -1302,8 +1302,8 @@ followed by an arbitrary number of cumul-fence links, ending with an
>  rfe link.  You can concoct more exotic examples, containing more than
>  one fence, although this quickly leads to diminishing returns in terms
>  of complexity.  For instance, here's an example containing a coe link
> -followed by two fences and an rfe link, utilizing the fact that
> -release fences are A-cumulative:
> +followed by a fence, an rfe link, another fence and and a final rfe link,
                                                   ^---^
> +utilizing the fact that release fences are A-cumulative:

I don't like this, for two reasons.  First is the repeated "and" typo.  
More importantly, it's not necessary to go into this level of detail; a
better revision would be:

+followed by two cumul-fences and an rfe link, utilizing the fact that

This is appropriate because the cumul-fence relation is defined to 
contain the rfe link which you noticed wasn't mentioned explicitly.

>  	int x, y, z;
>  
> @@ -1334,11 +1334,14 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
>  link from P0's store to its load.  This is because P0's store gets
>  overwritten by P1's store since x = 2 at the end (a coe link), the
>  smp_wmb() ensures that P1's store to x propagates to P2 before the
> -store to y does (the first fence), the store to y propagates to P2
> -before P2's load and store execute, P2's smp_store_release()
> -guarantees that the stores to x and y both propagate to P0 before the
> -store to z does (the second fence), and P0's load executes after the
> -store to z has propagated to P0 (an rfe link).
> +store to y does (the first fence), P2's store to y happens before P2's
---------------------------------------^

This makes no sense, since P2 doesn't store to y.  You meant P1's store
to y.  Also, the use of "happens before" is here unnecessarily
ambiguous (is it an informal usage or does it refer to the formal
happens-before relation?).  The original "propagates to" is better.

> +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".

Alan

Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Joel Fernandes]

On Sun, Jul 28, 2019 at 10:48:51AM -0400, Alan Stern wrote:
> On Sat, 27 Jul 2019, Joel Fernandes (Google) wrote:
> 
> > The lkmm example about ->prop relation should describe an additional rfe
> > link between P1's store to y and P2's load of y, which should be
> > critical to establishing the ordering resulting in the ->prop ordering
> > on P0. IOW, there are 2 rfe links, not one.
> > 
> > Correct these in the docs to make the ->prop ordering on P0 more clear.
> > 
> > Cc: kernel-team@android.com
> > Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
> > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > ---
> 
> This is not a good update.  See below...

No problem, thanks for the feedback. I am new to the LKMM so please bear
with me.. I should have tagged this RFC.

> >  .../memory-model/Documentation/explanation.txt  | 17 ++++++++++-------
> >  1 file changed, 10 insertions(+), 7 deletions(-)
> > 
> > diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> > index 68caa9a976d0..aa84fce854cc 100644
> > --- a/tools/memory-model/Documentation/explanation.txt
> > +++ b/tools/memory-model/Documentation/explanation.txt
> > @@ -1302,8 +1302,8 @@ followed by an arbitrary number of cumul-fence links, ending with an
> >  rfe link.  You can concoct more exotic examples, containing more than
> >  one fence, although this quickly leads to diminishing returns in terms
> >  of complexity.  For instance, here's an example containing a coe link
> > -followed by two fences and an rfe link, utilizing the fact that
> > -release fences are A-cumulative:
> > +followed by a fence, an rfe link, another fence and and a final rfe link,
>                                                    ^---^
> > +utilizing the fact that release fences are A-cumulative:
> 
> I don't like this, for two reasons.  First is the repeated "and" typo.

Will fix the trivial typo, sorry about that.

> More importantly, it's not necessary to go into this level of detail; a
> better revision would be:
> 
> +followed by two cumul-fences and an rfe link, utilizing the fact that
> 
> This is appropriate because the cumul-fence relation is defined to 
> contain the rfe link which you noticed wasn't mentioned explicitly.

No, I am talking about the P1's store to Y and P2's load of Y. That is not
through a cumul-fence so I don't understand what you meant? That _is_ missing
the rfe link I am referring to, that is left out.

The example says r2 = 1 and then we work backwards from that. r2 could very
well have been 0, there's no fence or anything involved, it just happens to
be the executation pattern causing r2 = 1 and hence the rfe link. Right?

> >  	int x, y, z;
> >  
> > @@ -1334,11 +1334,14 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
> >  link from P0's store to its load.  This is because P0's store gets
> >  overwritten by P1's store since x = 2 at the end (a coe link), the
> >  smp_wmb() ensures that P1's store to x propagates to P2 before the
> > -store to y does (the first fence), the store to y propagates to P2
> > -before P2's load and store execute, P2's smp_store_release()
> > -guarantees that the stores to x and y both propagate to P0 before the
> > -store to z does (the second fence), and P0's load executes after the
> > -store to z has propagated to P0 (an rfe link).
> > +store to y does (the first fence), P2's store to y happens before P2's
> ---------------------------------------^
> 
> This makes no sense, since P2 doesn't store to y.  You meant P1's store
> to y.  Also, the use of "happens before" is here unnecessarily
> ambiguous (is it an informal usage or does it refer to the formal
> happens-before relation?).  The original "propagates to" is better.

Will reword this.

> > +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?

thanks,

 - Joel

Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Boqun Feng]

[-- Attachment #1: Type: text/plain, Size: 5409 bytes --]

On Sun, Jul 28, 2019 at 11:19:59AM -0400, Joel Fernandes wrote:
> On Sun, Jul 28, 2019 at 10:48:51AM -0400, Alan Stern wrote:
> > On Sat, 27 Jul 2019, Joel Fernandes (Google) wrote:
> > 
> > > The lkmm example about ->prop relation should describe an additional rfe
> > > link between P1's store to y and P2's load of y, which should be
> > > critical to establishing the ordering resulting in the ->prop ordering
> > > on P0. IOW, there are 2 rfe links, not one.
> > > 
> > > Correct these in the docs to make the ->prop ordering on P0 more clear.
> > > 
> > > Cc: kernel-team@android.com
> > > Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
> > > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > > ---
> > 
> > This is not a good update.  See below...
> 
> No problem, thanks for the feedback. I am new to the LKMM so please bear
> with me.. I should have tagged this RFC.
> 
> > >  .../memory-model/Documentation/explanation.txt  | 17 ++++++++++-------
> > >  1 file changed, 10 insertions(+), 7 deletions(-)
> > > 
> > > diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> > > index 68caa9a976d0..aa84fce854cc 100644
> > > --- a/tools/memory-model/Documentation/explanation.txt
> > > +++ b/tools/memory-model/Documentation/explanation.txt
> > > @@ -1302,8 +1302,8 @@ followed by an arbitrary number of cumul-fence links, ending with an
> > >  rfe link.  You can concoct more exotic examples, containing more than
> > >  one fence, although this quickly leads to diminishing returns in terms
> > >  of complexity.  For instance, here's an example containing a coe link
> > > -followed by two fences and an rfe link, utilizing the fact that
> > > -release fences are A-cumulative:
> > > +followed by a fence, an rfe link, another fence and and a final rfe link,
> >                                                    ^---^
> > > +utilizing the fact that release fences are A-cumulative:
> > 
> > I don't like this, for two reasons.  First is the repeated "and" typo.
> 
> Will fix the trivial typo, sorry about that.
> 
> > More importantly, it's not necessary to go into this level of detail; a
> > better revision would be:
> > 
> > +followed by two cumul-fences and an rfe link, utilizing the fact that
> > 
> > This is appropriate because the cumul-fence relation is defined to 
> > contain the rfe link which you noticed wasn't mentioned explicitly.
> 
> No, I am talking about the P1's store to Y and P2's load of Y. That is not
> through a cumul-fence so I don't understand what you meant? That _is_ missing
> the rfe link I am referring to, that is left out.
> 
> The example says r2 = 1 and then we work backwards from that. r2 could very
> well have been 0, there's no fence or anything involved, it just happens to
> be the executation pattern causing r2 = 1 and hence the rfe link. Right?
> 
> > >  	int x, y, z;
> > >  
> > > @@ -1334,11 +1334,14 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
> > >  link from P0's store to its load.  This is because P0's store gets
> > >  overwritten by P1's store since x = 2 at the end (a coe link), the
> > >  smp_wmb() ensures that P1's store to x propagates to P2 before the
> > > -store to y does (the first fence), the store to y propagates to P2
> > > -before P2's load and store execute, P2's smp_store_release()
> > > -guarantees that the stores to x and y both propagate to P0 before the
> > > -store to z does (the second fence), and P0's load executes after the
> > > -store to z has propagated to P0 (an rfe link).
> > > +store to y does (the first fence), P2's store to y happens before P2's
> > ---------------------------------------^
> > 
> > This makes no sense, since P2 doesn't store to y.  You meant P1's store
> > to y.  Also, the use of "happens before" is here unnecessarily
> > ambiguous (is it an informal usage or does it refer to the formal
> > happens-before relation?).  The original "propagates to" is better.
> 
> Will reword this.
> 
> > > +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.

Regards,
Boqun

> thanks,
> 
>  - Joel
> 

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Joel Fernandes]

On Sun, Jul 28, 2019 at 11:28:06PM +0800, Boqun Feng wrote:
> On Sun, Jul 28, 2019 at 11:19:59AM -0400, Joel Fernandes wrote:
> > On Sun, Jul 28, 2019 at 10:48:51AM -0400, Alan Stern wrote:
> > > On Sat, 27 Jul 2019, Joel Fernandes (Google) wrote:
> > > 
> > > > The lkmm example about ->prop relation should describe an additional rfe
> > > > link between P1's store to y and P2's load of y, which should be
> > > > critical to establishing the ordering resulting in the ->prop ordering
> > > > on P0. IOW, there are 2 rfe links, not one.
> > > > 
> > > > Correct these in the docs to make the ->prop ordering on P0 more clear.
> > > > 
> > > > Cc: kernel-team@android.com
> > > > Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
> > > > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
> > > > ---
> > > 
> > > This is not a good update.  See below...
> > 
> > No problem, thanks for the feedback. I am new to the LKMM so please bear
> > with me.. I should have tagged this RFC.
> > 
> > > >  .../memory-model/Documentation/explanation.txt  | 17 ++++++++++-------
> > > >  1 file changed, 10 insertions(+), 7 deletions(-)
> > > > 
> > > > diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> > > > index 68caa9a976d0..aa84fce854cc 100644
> > > > --- a/tools/memory-model/Documentation/explanation.txt
> > > > +++ b/tools/memory-model/Documentation/explanation.txt
> > > > @@ -1302,8 +1302,8 @@ followed by an arbitrary number of cumul-fence links, ending with an
> > > >  rfe link.  You can concoct more exotic examples, containing more than
> > > >  one fence, although this quickly leads to diminishing returns in terms
> > > >  of complexity.  For instance, here's an example containing a coe link
> > > > -followed by two fences and an rfe link, utilizing the fact that
> > > > -release fences are A-cumulative:
> > > > +followed by a fence, an rfe link, another fence and and a final rfe link,
> > >                                                    ^---^
> > > > +utilizing the fact that release fences are A-cumulative:
> > > 
> > > I don't like this, for two reasons.  First is the repeated "and" typo.
> > 
> > Will fix the trivial typo, sorry about that.
> > 
> > > More importantly, it's not necessary to go into this level of detail; a
> > > better revision would be:
> > > 
> > > +followed by two cumul-fences and an rfe link, utilizing the fact that
> > > 
> > > This is appropriate because the cumul-fence relation is defined to 
> > > contain the rfe link which you noticed wasn't mentioned explicitly.
> > 
> > No, I am talking about the P1's store to Y and P2's load of Y. That is not
> > through a cumul-fence so I don't understand what you meant? That _is_ missing
> > the rfe link I am referring to, that is left out.
> > 
> > The example says r2 = 1 and then we work backwards from that. r2 could very
> > well have been 0, there's no fence or anything involved, it just happens to
> > be the executation pattern causing r2 = 1 and hence the rfe link. Right?
> > 
> > > >  	int x, y, z;
> > > >  
> > > > @@ -1334,11 +1334,14 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
> > > >  link from P0's store to its load.  This is because P0's store gets
> > > >  overwritten by P1's store since x = 2 at the end (a coe link), the
> > > >  smp_wmb() ensures that P1's store to x propagates to P2 before the
> > > > -store to y does (the first fence), the store to y propagates to P2
> > > > -before P2's load and store execute, P2's smp_store_release()
> > > > -guarantees that the stores to x and y both propagate to P0 before the
> > > > -store to z does (the second fence), and P0's load executes after the
> > > > -store to z has propagated to P0 (an rfe link).
> > > > +store to y does (the first fence), P2's store to y happens before P2's
> > > ---------------------------------------^
> > > 
> > > This makes no sense, since P2 doesn't store to y.  You meant P1's store
> > > to y.  Also, the use of "happens before" is here unnecessarily
> > > ambiguous (is it an informal usage or does it refer to the formal
> > > happens-before relation?).  The original "propagates to" is better.
> > 
> > Will reword this.
> > 
> > > > +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.

I mean the fact that you are asking Alan for clarification, means that it is
not that obvious ;)

thanks,

 - Joel

Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Boqun Feng]

[-- Attachment #1: Type: text/plain, Size: 2871 bytes --]

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 ;-)

Please consider the context of paragraph, this is an explanation of an
example, which is about the previous sentence:

	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.

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.

Thoughts?

Regards,
Boqun

> I mean the fact that you are asking Alan for clarification, means that it is
> not that obvious ;)
> 
> thanks,
> 
>  - Joel
> 
> 

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

[Joel Fernandes]

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