This lkmm example 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 in P0 more clear.
Signed-off-by: Joel Fernandes (Google) <[email protected]>
---
tools/memory-model/Documentation/explanation.txt | 16 +++++++++-------
1 file changed, 9 insertions(+), 7 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 68caa9a976d0..6c0dfaac7f04 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,13 @@ 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 of z (second fence), which also would
+imply that stores to x and y happen 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 does (A-cumulative property of this fence).
+Finally P0's load executes after 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
Hi Joel,
On Sat, Jul 27, 2019 at 08:00:31PM -0400, Joel Fernandes (Google) wrote:
> This lkmm example 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 in P0 more clear.
>
> Signed-off-by: Joel Fernandes (Google) <[email protected]>
> ---
> tools/memory-model/Documentation/explanation.txt | 16 +++++++++-------
> 1 file changed, 9 insertions(+), 7 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 68caa9a976d0..6c0dfaac7f04 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:
>
This part looks good to me.
> int x, y, z;
>
> @@ -1334,11 +1334,13 @@ 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 of z (second fence), which also would
> +imply that stores to x and y happen before the smp_store_release(), which
I think it's more accurate to say:
"imply that stores to x and y progagates to P2 before the
smp_store_release()"
, because by definition the propagation ordering that
smp_store_release() guarantees only works with stores that already
propagated to the CPU executing it, not the stores that execute/happen
before.
With that, feel free to add:
Reviewed-by: Boqun Feng <[email protected]>
Regards,
Boqun
> +means that P2's smp_store_release() will propagate stores to x and y to all
> +CPUs before the store to z does (A-cumulative property of this fence).
> +Finally P0's load executes after 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
>