Hi, there,
I'm new to LKMM. May I ask a may-be-stupid question?
In the LKMM document, it said the pb link:
E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F
can make sure E execute before F. But the cat file define pb as follow:
let pb = prop ; strong-fence ; hb* ; [Marked]
acyclic pb as propagation
So the acyclic rule is only on pb relationshit itself. So it won't
forbid F -rfe-> E, will it? It only forgit F -pb-> E. So how can
propagation rule ensure E execute before F?
Can anyone explain this? Thank you in advance.
- Kenneth Lee
(Expanding Cc:,)
> In the LKMM document, it said the pb link:
>
> E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F
>
> can make sure E execute before F. But the cat file define pb as follow:
>
> let pb = prop ; strong-fence ; hb* ; [Marked]
> acyclic pb as propagation
>
> So the acyclic rule is only on pb relationshit itself. So it won't
> forbid F -rfe-> E, will it? It only forgit F -pb-> E. So how can
> propagation rule ensure E execute before F?
With regard to your first question, the propagation rule does indeed forbid
F ->rfe E. To see why, suppose that F ->rfe E (in particular, E is a load
and the first link in your sequence is fre instead of coe). Then
E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->rfe E.
Since any rfe-link is an hb-link (by definition of the hb-relation), the
previous expression can be written as follows:
E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->hb E,
that is, given that hb* is the reflexive transitive closure of hb,
E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* E,
contradicting the fact that pb is acyclic. An argument similar to the one
reported above can show that the propagation rule forbids F ->hb E.
To address the second question, I'd start by first remarking that the CAT
file doesn't define an "execute-before" relation currently. This file does
however include the following comment:
(*
* The happens-before, propagation, and rcu constraints are all
* expressions of temporal ordering. They could be replaced by
* a single constraint on an "executes-before" relation, xb:
*
* let xb = hb | pb | rb
* acyclic xb as executes-before
*)
In this sense, the propagation rule (like other "acyclicity"-constraints of
the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
an "execute-before"-link. The file explanation.txt can provide additional
context/information, based on the (informal) operational model described in
that file, about this matter.
Notice that, as examples in tools/memory-model/litmus-tests/ can illustrate,
none of the three components of the xb-relation is redundant. Specifically,
there do exist pb-links/cycles which are not hb-link/cycles (and viceversa).
Maintaining three distinct/separate constraints (happens-before, propagation,
and rcu) instead of a single "executes-before" constraint, although formally
unnecessary, highlights the modularity and eases the debugging of the LKMM.
On Tue, Mar 05, 2024 at 07:00:55PM +0100, Andrea Parri wrote:
> Date: Tue, 5 Mar 2024 19:00:55 +0100
> From: Andrea Parri <[email protected]>
> To: [email protected]
> Cc: [email protected], [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> (Expanding Cc:,)
>
> > In the LKMM document, it said the pb link:
> >
> > E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F
> >
> > can make sure E execute before F. But the cat file define pb as follow:
> >
> > let pb = prop ; strong-fence ; hb* ; [Marked]
> > acyclic pb as propagation
> >
> > So the acyclic rule is only on pb relationshit itself. So it won't
> > forbid F -rfe-> E, will it? It only forgit F -pb-> E. So how can
> > propagation rule ensure E execute before F?
>
> With regard to your first question, the propagation rule does indeed forbid
> F ->rfe E. To see why, suppose that F ->rfe E (in particular, E is a load
> and the first link in your sequence is fre instead of coe). Then
>
> E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->rfe E.
>
> Since any rfe-link is an hb-link (by definition of the hb-relation), the
> previous expression can be written as follows:
>
> E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->hb E,
>
> that is, given that hb* is the reflexive transitive closure of hb,
>
> E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* E,
>
> contradicting the fact that pb is acyclic. An argument similar to the one
> reported above can show that the propagation rule forbids F ->hb E.
>
Wow, my gosh, I didn't expect the last "hb*" works like this:). Very clear
explaination, thank you very much.
> To address the second question, I'd start by first remarking that the CAT
> file doesn't define an "execute-before" relation currently. This file does
> however include the following comment:
>
> (*
> * The happens-before, propagation, and rcu constraints are all
> * expressions of temporal ordering. They could be replaced by
> * a single constraint on an "executes-before" relation, xb:
> *
> * let xb = hb | pb | rb
> * acyclic xb as executes-before
> *)
>
> In this sense, the propagation rule (like other "acyclicity"-constraints of
> the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
> an "execute-before"-link. The file explanation.txt can provide additional
> context/information, based on the (informal) operational model described in
> that file, about this matter.
So it is just a rule in the sence of mathematics? I think it would be better
if there were some explaination in the explaination file. It is
descripted in nature language, the reader might not notify it is just a
mathematics rule. And you cannot say an action executes before another
because they are in the pb link. It becomes a cycling in logic...
But anyway, now I understand. Thank you very much.
>
> Notice that, as examples in tools/memory-model/litmus-tests/ can illustrate,
> none of the three components of the xb-relation is redundant. Specifically,
> there do exist pb-links/cycles which are not hb-link/cycles (and viceversa).
>
> Maintaining three distinct/separate constraints (happens-before, propagation,
> and rcu) instead of a single "executes-before" constraint, although formally
> unnecessary, highlights the modularity and eases the debugging of the LKMM.
--
-Kenneth Lee
> > In this sense, the propagation rule (like other "acyclicity"-constraints of
> > the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
> > an "execute-before"-link. The file explanation.txt can provide additional
> > context/information, based on the (informal) operational model described in
> > that file, about this matter.
>
> So it is just a rule in the sence of mathematics? I think it would be better
> if there were some explaination in the explaination file. It is
> descripted in nature language, the reader might not notify it is just a
> mathematics rule. And you cannot say an action executes before another
> because they are in the pb link. It becomes a cycling in logic...
I think you're on to something, explaining mathematical axioms or rules has
never been an easy task AFAIU. ;-) (and that's why feedback is welcome)
The remark could be to continue to consider such rules "generalizations" of
properties met by several hardware models or other specific contexts, rather
than (mere) logically-derived facts.
Andrea
On Wed, Mar 06, 2024 at 06:36:09PM +0100, Andrea Parri wrote:
> > > In this sense, the propagation rule (like other "acyclicity"-constraints of
> > > the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
> > > an "execute-before"-link. The file explanation.txt can provide additional
> > > context/information, based on the (informal) operational model described in
> > > that file, about this matter.
> >
> > So it is just a rule in the sence of mathematics? I think it would be better
> > if there were some explaination in the explaination file. It is
> > descripted in nature language, the reader might not notify it is just a
> > mathematics rule. And you cannot say an action executes before another
> > because they are in the pb link. It becomes a cycling in logic...
This _is_ described in the explanation.txt file.
The first paragraph in the section named "THE PROPAGATES-BEFORE
RELATION: pb" mentions the mathematical rule:
---------------------------------------------------------------------
The propagates-before (pb) relation capitalizes on the special
features of strong fences. It links two events E and F whenever some
store is coherence-later than E and propagates to every CPU and to RAM
before F executes. The formal definition requires that E be linked to
F via a coe or fre link, an arbitrary number of cumul-fences, an
optional rfe link, a strong fence, and an arbitrary number of hb
links. Let's see how this definition works out.
---------------------------------------------------------------------
Later on, the file includes this paragraph, which answers the question
you were asking:
---------------------------------------------------------------------
The existence of a pb link from E to F implies that E must execute
before F. To see why, suppose that F executed first. Then W would
have propagated to E's CPU before E executed. If E was a store, the
memory subsystem would then be forced to make E come after W in the
coherence order, contradicting the fact that E ->coe W. If E was a
load, the memory subsystem would then be forced to satisfy E's read
request with the value stored by W or an even later store,
contradicting the fact that E ->fre W.
---------------------------------------------------------------------
Alan Stern
> I think you're on to something, explaining mathematical axioms or rules has
> never been an easy task AFAIU. ;-) (and that's why feedback is welcome)
>
> The remark could be to continue to consider such rules "generalizations" of
> properties met by several hardware models or other specific contexts, rather
> than (mere) logically-derived facts.
>
> Andrea
> Later on, the file includes this paragraph, which answers the question
> you were asking:
>
> ---------------------------------------------------------------------
> The existence of a pb link from E to F implies that E must execute
> before F. To see why, suppose that F executed first. Then W would
> have propagated to E's CPU before E executed. If E was a store, the
> memory subsystem would then be forced to make E come after W in the
> coherence order, contradicting the fact that E ->coe W. If E was a
> load, the memory subsystem would then be forced to satisfy E's read
> request with the value stored by W or an even later store,
> contradicting the fact that E ->fre W.
> ---------------------------------------------------------------------
TBF, that just explains (not F ->xb E), or I guess that was the origin
of the question.
Andrea
On Wed, Mar 06, 2024 at 08:24:42PM +0100, Andrea Parri wrote:
> Date: Wed, 6 Mar 2024 20:24:42 +0100
> From: Andrea Parri <[email protected]>
> To: Alan Stern <[email protected]>
> Cc: [email protected], [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> > Later on, the file includes this paragraph, which answers the question
> > you were asking:
> >
> > ---------------------------------------------------------------------
> > The existence of a pb link from E to F implies that E must execute
> > before F. To see why, suppose that F executed first. Then W would
> > have propagated to E's CPU before E executed. If E was a store, the
> > memory subsystem would then be forced to make E come after W in the
> > coherence order, contradicting the fact that E ->coe W. If E was a
> > load, the memory subsystem would then be forced to satisfy E's read
> > request with the value stored by W or an even later store,
> > contradicting the fact that E ->fre W.
> > ---------------------------------------------------------------------
>
> TBF, that just explains (not F ->xb E), or I guess that was the origin
> of the question.
Yes. I thought a link was just an unconditional pattern for the
programmer to match the actual code so the other categories (of links in
the same acyclic rule) cannot route back. But now I understand the ->xx*
relation in the begining or end of the link can also add xx to the rule.
>
> Andrea
--
-Kenneth Lee
On Wed, Mar 06, 2024 at 08:24:42PM +0100, Andrea Parri wrote:
> > Later on, the file includes this paragraph, which answers the question
> > you were asking:
> >
> > ---------------------------------------------------------------------
> > The existence of a pb link from E to F implies that E must execute
> > before F. To see why, suppose that F executed first. Then W would
> > have propagated to E's CPU before E executed. If E was a store, the
> > memory subsystem would then be forced to make E come after W in the
> > coherence order, contradicting the fact that E ->coe W. If E was a
> > load, the memory subsystem would then be forced to satisfy E's read
> > request with the value stored by W or an even later store,
> > contradicting the fact that E ->fre W.
> > ---------------------------------------------------------------------
>
> TBF, that just explains (not F ->xb E), or I guess that was the origin
> of the question.
So perhaps as in the diff below. (Alan, feel free to manipulate to better
align with the current contents and style of explanation.txt.)
Andrea
From c13fd76cd62638cbe197431a16aeea001f80f6ec Mon Sep 17 00:00:00 2001
From: Andrea Parri <[email protected]>
Date: Thu, 7 Mar 2024 16:31:57 +0100
Subject: [PATCH] tools/memory-model: Amend the description of the pb relation
To convey why E ->pb F implies E ->xb F in the operational model of
explanation.txt.
Reported-by: Kenneth Lee <[email protected]>
Signed-off-by: Andrea Parri <[email protected]>
---
tools/memory-model/Documentation/explanation.txt | 12 +++++-------
1 file changed, 5 insertions(+), 7 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 6dc8b3642458e..68af5effadbbb 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -1461,13 +1461,11 @@ The case where E is a load is exactly the same, except that the first
link in the sequence is fre instead of coe.
The existence of a pb link from E to F implies that E must execute
-before F. To see why, suppose that F executed first. Then W would
-have propagated to E's CPU before E executed. If E was a store, the
-memory subsystem would then be forced to make E come after W in the
-coherence order, contradicting the fact that E ->coe W. If E was a
-load, the memory subsystem would then be forced to satisfy E's read
-request with the value stored by W or an even later store,
-contradicting the fact that E ->fre W.
+before F. To see why, let W be a store coherence-later than E and
+propagating to every CPU and to RAM before F executes. Then E must
+execute before W propagates to E's CPU (since W is coherence-later
+than E). In turn, W propagates to E's CPU (and every CPU) before F
+executes.
A good example illustrating how pb works is the SB pattern with strong
fences:
--
2.34.1
On Thu, Mar 07, 2024 at 04:52:07PM +0100, Andrea Parri wrote:
> On Wed, Mar 06, 2024 at 08:24:42PM +0100, Andrea Parri wrote:
> > > Later on, the file includes this paragraph, which answers the question
> > > you were asking:
> > >
> > > ---------------------------------------------------------------------
> > > The existence of a pb link from E to F implies that E must execute
> > > before F. To see why, suppose that F executed first. Then W would
> > > have propagated to E's CPU before E executed. If E was a store, the
> > > memory subsystem would then be forced to make E come after W in the
> > > coherence order, contradicting the fact that E ->coe W. If E was a
> > > load, the memory subsystem would then be forced to satisfy E's read
> > > request with the value stored by W or an even later store,
> > > contradicting the fact that E ->fre W.
> > > ---------------------------------------------------------------------
> >
> > TBF, that just explains (not F ->xb E), or I guess that was the origin
> > of the question.
Are we talking about the formal xb relation (as mentioned in a comment
in linux-kernel.cat), or the informal notion of "executing before" as
used in the operational model? In the first case, it's true by
definition that pb implies xb, since xb would be defined by:
let xb = hb | pb | rb
if it were in the memory model.
So I guess you're talking about the second, intuitive meaning. That's
very simple to explain. Since every instruction executes at _some_
time, and since we can safely assume that no two instructions execute at
exactly the _same_ time, if F doesn't execute before E then E must
execute before F. Or using your terms, (not F ->xb E) implies (E ->xb
F). Would that answer the original question satisfactorily?
> So perhaps as in the diff below. (Alan, feel free to manipulate to better
> align with the current contents and style of explanation.txt.)
>
> Andrea
>
> From c13fd76cd62638cbe197431a16aeea001f80f6ec Mon Sep 17 00:00:00 2001
> From: Andrea Parri <[email protected]>
> Date: Thu, 7 Mar 2024 16:31:57 +0100
> Subject: [PATCH] tools/memory-model: Amend the description of the pb relation
>
> To convey why E ->pb F implies E ->xb F in the operational model of
> explanation.txt.
>
> Reported-by: Kenneth Lee <[email protected]>
> Signed-off-by: Andrea Parri <[email protected]>
> ---
> tools/memory-model/Documentation/explanation.txt | 12 +++++-------
> 1 file changed, 5 insertions(+), 7 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 6dc8b3642458e..68af5effadbbb 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -1461,13 +1461,11 @@ The case where E is a load is exactly the same, except that the first
> link in the sequence is fre instead of coe.
>
> The existence of a pb link from E to F implies that E must execute
> -before F. To see why, suppose that F executed first. Then W would
> -have propagated to E's CPU before E executed. If E was a store, the
> -memory subsystem would then be forced to make E come after W in the
> -coherence order, contradicting the fact that E ->coe W. If E was a
> -load, the memory subsystem would then be forced to satisfy E's read
> -request with the value stored by W or an even later store,
> -contradicting the fact that E ->fre W.
> +before F. To see why, let W be a store coherence-later than E and
> +propagating to every CPU and to RAM before F executes. Then E must
> +execute before W propagates to E's CPU (since W is coherence-later
> +than E). In turn, W propagates to E's CPU (and every CPU) before F
> +executes.
The new text says the same thing as the original, just in a more
condensed way. It skips the detailed explanation of why E must execute
before W propagates to E's CPU, merely saying that it is because "W is
coherence-later than E". I'm not sure this is an improvement; the
reader might want to know exactly how this reasoning goes.
Would it suit you to instead add an extra sentence to the end of the
paragraph, something like this?
These contradictions show that E must execute before W
propagates to E's CPU, hence before W propagates to every
CPU, and hence before F executes.
Alan Stern
> So I guess you're talking about the second, intuitive meaning. That's
> very simple to explain. Since every instruction executes at _some_
> time, and since we can safely assume that no two instructions execute at
> exactly the _same_ time, if F doesn't execute before E then E must
> execute before F. Or using your terms, (not F ->xb E) implies (E ->xb
> F). Would that answer the original question satisfactorily?
I'd disagree with these premises: certain instructions can and do execute
at the same time. FWIW, in the formal model, it is not that difficult to
provide examples of "(not F ->xb E) and (not E ->xb F)".
> The new text says the same thing as the original, just in a more
> condensed way. It skips the detailed explanation of why E must execute
> before W propagates to E's CPU, merely saying that it is because "W is
> coherence-later than E". I'm not sure this is an improvement; the
> reader might want to know exactly how this reasoning goes.
The current text relies on an argument by contradiction. A contradiction
is reached by "forcing" (F ->xb E), hence all it can be concluded is that
(not F ->xb E). Again, AFAICS, this doesn't match the claim in the text.
Andrea
On Thu, Mar 07, 2024 at 07:18:46PM +0100, Andrea Parri wrote:
> > So I guess you're talking about the second, intuitive meaning. That's
> > very simple to explain. Since every instruction executes at _some_
> > time, and since we can safely assume that no two instructions execute at
> > exactly the _same_ time, if F doesn't execute before E then E must
> > execute before F. Or using your terms, (not F ->xb E) implies (E ->xb
> > F). Would that answer the original question satisfactorily?
>
> I'd disagree with these premises: certain instructions can and do execute
> at the same time.
Can you give an example?
> FWIW, in the formal model, it is not that difficult to
> provide examples of "(not F ->xb E) and (not E ->xb F)".
That's because the xb relation in the formal model does not fully
capture our intuitive notion of "executes at the same time" in the
informal operational model.
Also, it's important to distinguish between:
(1) Two instructions that are forced (say by a dependency) or known
(say by an rfe link) to execute in a particular order; versus
(2) Two instructions that may execute in either order but do execute
in some particular order during a given run of the program.
The formal xb relation corresponds more to (1), whereas the informal
notion corresponds more to (2).
> > The new text says the same thing as the original, just in a more
> > condensed way. It skips the detailed explanation of why E must execute
> > before W propagates to E's CPU, merely saying that it is because "W is
> > coherence-later than E". I'm not sure this is an improvement; the
> > reader might want to know exactly how this reasoning goes.
>
> The current text relies on an argument by contradiction. A contradiction
> is reached by "forcing" (F ->xb E), hence all it can be concluded is that
> (not F ->xb E). Again, AFAICS, this doesn't match the claim in the text.
That's why I suggested adding an extra sentence to the paragraph (which
you did not quote in your reply). That sentence gave a direct argument.
Alan
> > I'd disagree with these premises: certain instructions can and do execute
> > at the same time.
>
> Can you give an example?
I think I'm starting to see where this is going..., but to address the
question: really any example where the LKMM doesn't know better, say
C test
{}
P0(int *x)
{
*x = 1;
}
P1(int *x)
{
*x = 2;
}
> > FWIW, in the formal model, it is not that difficult to
> > provide examples of "(not F ->xb E) and (not E ->xb F)".
>
> That's because the xb relation in the formal model does not fully
> capture our intuitive notion of "executes at the same time" in the
> informal operational model.
>
> Also, it's important to distinguish between:
>
> (1) Two instructions that are forced (say by a dependency) or known
> (say by an rfe link) to execute in a particular order; versus
>
> (2) Two instructions that may execute in either order but do execute
> in some particular order during a given run of the program.
>
> The formal xb relation corresponds more to (1), whereas the informal
> notion corresponds more to (2).
This appears to be the key observation. For if, in the operational model,
(not F ->xb E) implies (E ->xb F) then I'll apologize for the noise. :-)
> > > The new text says the same thing as the original, just in a more
> > > condensed way. It skips the detailed explanation of why E must execute
> > > before W propagates to E's CPU, merely saying that it is because "W is
> > > coherence-later than E". I'm not sure this is an improvement; the
> > > reader might want to know exactly how this reasoning goes.
> >
> > The current text relies on an argument by contradiction. A contradiction
> > is reached by "forcing" (F ->xb E), hence all it can be concluded is that
> > (not F ->xb E). Again, AFAICS, this doesn't match the claim in the text.
>
> That's why I suggested adding an extra sentence to the paragraph (which
> you did not quote in your reply). That sentence gave a direct argument.
Well, I read that sentence but stopped at "These contradictions show that"
for the reason I detailed above.
Andrea
On Thu, Mar 07, 2024 at 08:08:46PM +0100, Andrea Parri wrote:
> > > I'd disagree with these premises: certain instructions can and do execute
> > > at the same time.
> >
> > Can you give an example?
>
> I think I'm starting to see where this is going..., but to address the
> question: really any example where the LKMM doesn't know better, say
>
> C test
>
> {}
>
> P0(int *x)
> {
> *x = 1;
> }
>
> P1(int *x)
> {
> *x = 2;
> }
Ah, but you see, any time you run this program one of those statements
will execute before the other. Which will go first is indeterminate,
but the chance of them executing at _exactly_ the same moment is zero.
The LKMM can't say which will execute first because it could be either
one. In other words, "I don't know which will execute first" is very
different from "They will execute at the same time".
> > > FWIW, in the formal model, it is not that difficult to
> > > provide examples of "(not F ->xb E) and (not E ->xb F)".
> >
> > That's because the xb relation in the formal model does not fully
> > capture our intuitive notion of "executes at the same time" in the
> > informal operational model.
> >
> > Also, it's important to distinguish between:
> >
> > (1) Two instructions that are forced (say by a dependency) or known
> > (say by an rfe link) to execute in a particular order; versus
> >
> > (2) Two instructions that may execute in either order but do execute
> > in some particular order during a given run of the program.
> >
> > The formal xb relation corresponds more to (1), whereas the informal
> > notion corresponds more to (2).
>
> This appears to be the key observation. For if, in the operational model,
> (not F ->xb E) implies (E ->xb F) then I'll apologize for the noise. :-)
Okay, so it looks like we're in violent agreement. :-)
> > > > The new text says the same thing as the original, just in a more
> > > > condensed way. It skips the detailed explanation of why E must execute
> > > > before W propagates to E's CPU, merely saying that it is because "W is
> > > > coherence-later than E". I'm not sure this is an improvement; the
> > > > reader might want to know exactly how this reasoning goes.
> > >
> > > The current text relies on an argument by contradiction. A contradiction
> > > is reached by "forcing" (F ->xb E), hence all it can be concluded is that
> > > (not F ->xb E). Again, AFAICS, this doesn't match the claim in the text.
> >
> > That's why I suggested adding an extra sentence to the paragraph (which
> > you did not quote in your reply). That sentence gave a direct argument.
>
> Well, I read that sentence but stopped at "These contradictions show that"
> for the reason I detailed above.
The way you put it also relies on argument by contradiction. This
just wasn't visible, because you omitted a lot of intermediate steps in
the reasoning.
If you want to see this in detail, try explaining why it is that "W is
coherence-later than E" implies "E must execute before W propagates to
E's CPU" in the operational model.
Alan
> > C test
> >
> > {}
> >
> > P0(int *x)
> > {
> > *x = 1;
> > }
> >
> > P1(int *x)
> > {
> > *x = 2;
> > }
>
> Ah, but you see, any time you run this program one of those statements
> will execute before the other. Which will go first is indeterminate,
> but the chance of them executing at _exactly_ the same moment is zero.
TBH, I don't. But I trust you know your memory controller. ;-)
> > This appears to be the key observation. For if, in the operational model,
> > (not F ->xb E) implies (E ->xb F) then I'll apologize for the noise. :-)
>
> Okay, so it looks like we're in violent agreement. :-)
Fiuu!! ;-)
> The way you put it also relies on argument by contradiction. This
> just wasn't visible, because you omitted a lot of intermediate steps in
> the reasoning.
>
> If you want to see this in detail, try explaining why it is that "W is
> coherence-later than E" implies "E must execute before W propagates to
> E's CPU" in the operational model.
But that's all over in explanation.txt?? FWIW, a quick search returned
(wrt fre):
R ->fre W means that W overwrites the value which R reads, but it
doesn't mean that W has to execute after R. All that's necessary
is for the memory subsystem not to propagate W to R's CPU until
after R has executed
I really don't see how the operational model could explain even a simple
MP without "knowing" this fact.
IAC, I'm pretty sure my "intermediate steps" wouldn't be using the same
forcing condition. :-)
Andrea
On Thu, Mar 07, 2024 at 08:08:46PM +0100, Andrea Parri wrote:
> Date: Thu, 7 Mar 2024 20:08:46 +0100
> From: Andrea Parri <[email protected]>
> To: Alan Stern <[email protected]>
> Cc: [email protected], [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> > > I'd disagree with these premises: certain instructions can and do execute
> > > at the same time.
> >
> > Can you give an example?
>
> I think I'm starting to see where this is going..., but to address the
> question: really any example where the LKMM doesn't know better, say
>
> C test
>
> {}
>
> P0(int *x)
> {
> *x = 1;
> }
>
> P1(int *x)
> {
> *x = 2;
> }
>
TBH, the concept "execute-before" gave me a lot of trouble when I read
explanation.txt at the very beginning. The name hints an absolute and
global timeline over everything. But that makes no sense because no one
can observe that order at all. So till now, I still need to translate
the concept to an order by particular observer , such as a CPU or the
memory system, for further understanding.
And speaking of example, can I ask another question?:
In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
it uses the following example to explain the prop relation:
P0()
{
int r1;
WRITE_ONCE(x, 1);
r1 = READ_ONCE(x);
}
P1()
{
WRITE_ONCE(x, 8);
}
if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
explained with the operational model. But according to the definition of
prop,
let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
The link should contain a cumul-fence, which doesn't exist in the
example.
This also makes me confuse on what explanation.txt explains: the
dependable rule/link deduced from operational model, or the physical
meaning of the concepts used in the cat definition?
Alan's discussion make feel the answer is former. If it is, my question is
closed. But I feel it should be latter. In this case, I think we cannot
just explain "it can be explained in the operational model";)
(CC Alan: I couldn't receive your previous email in this topic, I think
it is because I'm not a subscriber of lkml. I would be very grateful if
you could cc me in the follow-up email)
>
> > > FWIW, in the formal model, it is not that difficult to
> > > provide examples of "(not F ->xb E) and (not E ->xb F)".
> >
> > That's because the xb relation in the formal model does not fully
> > capture our intuitive notion of "executes at the same time" in the
> > informal operational model.
> >
> > Also, it's important to distinguish between:
> >
> > (1) Two instructions that are forced (say by a dependency) or known
> > (say by an rfe link) to execute in a particular order; versus
> >
> > (2) Two instructions that may execute in either order but do execute
> > in some particular order during a given run of the program.
> >
> > The formal xb relation corresponds more to (1), whereas the informal
> > notion corresponds more to (2).
>
> This appears to be the key observation. For if, in the operational model,
> (not F ->xb E) implies (E ->xb F) then I'll apologize for the noise. :-)
>
>
> > > > The new text says the same thing as the original, just in a more
> > > > condensed way. It skips the detailed explanation of why E must execute
> > > > before W propagates to E's CPU, merely saying that it is because "W is
> > > > coherence-later than E". I'm not sure this is an improvement; the
> > > > reader might want to know exactly how this reasoning goes.
> > >
> > > The current text relies on an argument by contradiction. A contradiction
> > > is reached by "forcing" (F ->xb E), hence all it can be concluded is that
> > > (not F ->xb E). Again, AFAICS, this doesn't match the claim in the text.
> >
> > That's why I suggested adding an extra sentence to the paragraph (which
> > you did not quote in your reply). That sentence gave a direct argument.
>
> Well, I read that sentence but stopped at "These contradictions show that"
> for the reason I detailed above.
>
> Andrea
--
-Kenneth Lee (Hisilicon)
On Thu, Mar 07, 2024 at 10:06:08PM +0100, Andrea Parri wrote:
> > > C test
> > >
> > > {}
> > >
> > > P0(int *x)
> > > {
> > > *x = 1;
> > > }
> > >
> > > P1(int *x)
> > > {
> > > *x = 2;
> > > }
> >
> > Ah, but you see, any time you run this program one of those statements
> > will execute before the other. Which will go first is indeterminate,
> > but the chance of them executing at _exactly_ the same moment is zero.
>
> TBH, I don't. But I trust you know your memory controller. ;-)
I can't tell which aspect of this bothers you more: the fact that the
text uses an argument by contradiction, or the fact that it ignores the
possibility of two instructions executing at the same time.
If it's the latter, consider this: Although the text doesn't say so,
the reasoning it gives also covers the case where F executes at the same
time as E. You can still deduce that W must have propagated to E's
CPU before E executed, because W must propagate to every CPU before F
executes.
> > The way you put it also relies on argument by contradiction. This
> > just wasn't visible, because you omitted a lot of intermediate steps in
> > the reasoning.
> >
> > If you want to see this in detail, try explaining why it is that "W is
> > coherence-later than E" implies "E must execute before W propagates to
> > E's CPU" in the operational model.
>
> But that's all over in explanation.txt?? FWIW, a quick search returned
> (wrt fre):
>
> R ->fre W means that W overwrites the value which R reads, but it
> doesn't mean that W has to execute after R. All that's necessary
> is for the memory subsystem not to propagate W to R's CPU until
> after R has executed
(In fact, that sentence isn't entirely accurate. It should say "... not
to propagate W (or a co-later store)...".)
Let's consider coe instead of fre. The description of how the
operational model manages the coherence order of stores is found in
section 13 (AN OPERATIONAL MODEL):
When CPU C executes a store instruction, it tells the memory
subsystem to store a certain value at a certain location. The
memory subsystem propagates the store to all the other CPUs as
well as to RAM. (As a special case, we say that the store
propagates to its own CPU at the time it is executed.) The
memory subsystem also determines where the store falls in the
location's coherence order. In particular, it must arrange for
the store to be co-later than (i.e., to overwrite) any other
store to the same location which has already propagated to CPU
C.
So now if E is a store and is co-before W, how do we know that W didn't
propagate to E's CPU before E executed? It's clear from the last
sentence of the text above: If W had propagated to E's CPU before E
executed then the memory subsystem would have arranged for E to be
co-later than W. That's an argument by contradiction, and there's no
way to avoid it here.
Alan
> I can't tell which aspect of this bothers you more: the fact that the
> text uses an argument by contradiction, or the fact that it ignores the
> possibility of two instructions executing at the same time.
>
> If it's the latter, consider this: Although the text doesn't say so,
> the reasoning it gives also covers the case where F executes at the same
> time as E. You can still deduce that W must have propagated to E's
> CPU before E executed, because W must propagate to every CPU before F
> executes.
Agreed. I suspect this exchange would have been much shorter if we did
say/write so, but I'll leave it up to you.
> (In fact, that sentence isn't entirely accurate. It should say "... not
> to propagate W (or a co-later store)...".)
>
> Let's consider coe instead of fre. The description of how the
> operational model manages the coherence order of stores is found in
> section 13 (AN OPERATIONAL MODEL):
>
> When CPU C executes a store instruction, it tells the memory
> subsystem to store a certain value at a certain location. The
> memory subsystem propagates the store to all the other CPUs as
> well as to RAM. (As a special case, we say that the store
> propagates to its own CPU at the time it is executed.) The
> memory subsystem also determines where the store falls in the
> location's coherence order. In particular, it must arrange for
> the store to be co-later than (i.e., to overwrite) any other
> store to the same location which has already propagated to CPU
> C.
>
> So now if E is a store and is co-before W, how do we know that W didn't
> propagate to E's CPU before E executed? It's clear from the last
> sentence of the text above: If W had propagated to E's CPU before E
> executed then the memory subsystem would have arranged for E to be
> co-later than W. That's an argument by contradiction, and there's no
> way to avoid it here.
I can live with that.
Andrea
> In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
> it uses the following example to explain the prop relation:
>
> P0()
> {
> int r1;
>
> WRITE_ONCE(x, 1);
> r1 = READ_ONCE(x);
> }
>
> P1()
> {
> WRITE_ONCE(x, 8);
> }
>
> if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
> explained with the operational model. But according to the definition of
> prop,
>
> let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
>
> The link should contain a cumul-fence, which doesn't exist in the
> example.
Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
[Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
(P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
Andrea
On Fri, Mar 08, 2024 at 10:38:09PM +0100, Andrea Parri wrote:
> Date: Fri, 8 Mar 2024 22:38:09 +0100
> From: Andrea Parri <[email protected]>
> To: [email protected]
> Cc: Alan Stern <[email protected]>, [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> > In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
> > it uses the following example to explain the prop relation:
> >
> > P0()
> > {
> > int r1;
> >
> > WRITE_ONCE(x, 1);
> > r1 = READ_ONCE(x);
> > }
> >
> > P1()
> > {
> > WRITE_ONCE(x, 8);
> > }
> >
> > if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
> > explained with the operational model. But according to the definition of
> > prop,
> >
> > let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> >
> > The link should contain a cumul-fence, which doesn't exist in the
> > example.
>
> Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
> is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
>
> The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
>
> [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> (P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
>
So the cumul-fence relation includes the same Store? This is hard to
understand, because it is defined as:
let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
po-unlock-lock-po) ; [Marked] ; rmw-sequence
There is at lease a rmw-sequence in the relation link.
I doubt we have different understanding on the effect of
reflexive operator. Let's discuss this with an example. Say we have two
relation r1 and r2. r1 have (e1, e2) while r2 have (e2, e3). Then we got
(e1, e3) for (r1;r2). The (;) operator joins r1's range to r2's domain.
If we upgrade (r1;r2) to (r1?;r2), (r1?) become {(m1, m1), (m1, m2), (m2,
m2)}, it is r1 plus all identity of all elements used in r1's relations.
So (r1?;r2) is {(m1, m3), (m2, m3)}. If we consider this link:
e1 ->r1 ->e2 ->r2 e3
A question mark on r1 means both (e1, e3) and (e2, e3) are included in
the final definition. The r1 is ignore-able in the definition. The event
before or behind the ignore-able relation both belong to the definition.
But this doesn't means r1 is optional. If r1 is empty, (r1?;r2) will
become empty, because there is no event element in r1's relations.
So I think the reflexive-transitive operation on cumul-fence cannot make
this relation optional. You should first have such link in the code.
-Kenneth
> Andrea
> > Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
> > is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
> >
> > The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
> >
> > [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> > (P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
> >
>
> So the cumul-fence relation includes the same Store? This is hard to
> understand, because it is defined as:
>
> let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> po-unlock-lock-po) ; [Marked] ; rmw-sequence
>
> There is at lease a rmw-sequence in the relation link.
>
> I doubt we have different understanding on the effect of
> reflexive operator. Let's discuss this with an example. Say we have two
> relation r1 and r2. r1 have (e1, e2) while r2 have (e2, e3). Then we got
> (e1, e3) for (r1;r2). The (;) operator joins r1's range to r2's domain.
>
> If we upgrade (r1;r2) to (r1?;r2), (r1?) become {(m1, m1), (m1, m2), (m2,
> m2)}, it is r1 plus all identity of all elements used in r1's relations.
>
> So (r1?;r2) is {(m1, m3), (m2, m3)}. If we consider this link:
>
> e1 ->r1 ->e2 ->r2 e3
>
> A question mark on r1 means both (e1, e3) and (e2, e3) are included in
> the final definition. The r1 is ignore-able in the definition. The event
> before or behind the ignore-able relation both belong to the definition.
>
> But this doesn't means r1 is optional. If r1 is empty, (r1?;r2) will
> become empty, because there is no event element in r1's relations.
>
> So I think the reflexive-transitive operation on cumul-fence cannot make
> this relation optional. You should first have such link in the code.
In Cat, r1? is better described by (following your own wording) "r1 plus
all identity of all elements (i.e. not necessarily in r1)".
As an example, in the scenario at stake, cumul-fence is empty while both
cumul-fence? and cumul-fence* match the identity relation on all events.
Here is a (relatively old, but still accurate AFAICR) article describing
these and other notions as used in Herd: (cf. table at the bottom)
https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/herd.html
Said this, I do think the best way to familiarize with these notions and
check one's understanding is to spend time using the herd tool itself.
Andrea
On Sun, Mar 10, 2024 at 03:27:10AM +0100, Andrea Parri wrote:
> Date: Sun, 10 Mar 2024 03:27:10 +0100
> From: Andrea Parri <[email protected]>
> To: [email protected]
> Cc: Alan Stern <[email protected]>, [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> > > Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
> > > is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
> > >
> > > The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
> > >
> > > [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> > > (P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
> > >
> >
> > So the cumul-fence relation includes the same Store? This is hard to
> > understand, because it is defined as:
> >
> > let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> > po-unlock-lock-po) ; [Marked] ; rmw-sequence
> >
> > There is at lease a rmw-sequence in the relation link.
> >
> > I doubt we have different understanding on the effect of
> > reflexive operator. Let's discuss this with an example. Say we have two
> > relation r1 and r2. r1 have (e1, e2) while r2 have (e2, e3). Then we got
> > (e1, e3) for (r1;r2). The (;) operator joins r1's range to r2's domain.
> >
> > If we upgrade (r1;r2) to (r1?;r2), (r1?) become {(m1, m1), (m1, m2), (m2,
> > m2)}, it is r1 plus all identity of all elements used in r1's relations.
> >
> > So (r1?;r2) is {(m1, m3), (m2, m3)}. If we consider this link:
> >
> > e1 ->r1 ->e2 ->r2 e3
> >
> > A question mark on r1 means both (e1, e3) and (e2, e3) are included in
> > the final definition. The r1 is ignore-able in the definition. The event
> > before or behind the ignore-able relation both belong to the definition.
> >
> > But this doesn't means r1 is optional. If r1 is empty, (r1?;r2) will
> > become empty, because there is no event element in r1's relations.
> >
> > So I think the reflexive-transitive operation on cumul-fence cannot make
> > this relation optional. You should first have such link in the code.
>
> In Cat, r1? is better described by (following your own wording) "r1 plus
> all identity of all elements (i.e. not necessarily in r1)".
>
> As an example, in the scenario at stake, cumul-fence is empty while both
> cumul-fence? and cumul-fence* match the identity relation on all events.
>
> Here is a (relatively old, but still accurate AFAICR) article describing
> these and other notions as used in Herd: (cf. table at the bottom)
>
> https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/herd.html
>
> Said this, I do think the best way to familiarize with these notions and
> check one's understanding is to spend time using the herd tool itself.
>
Ah, thank you very much for the link. The information is even not in the
herd7 manual. That's way I following the understanding from some mathematical
text such as: "The reflexive transitive closure of R is denoted R∗, and
is defined as the reflexive closure of the transitive closure of R".
It doesn't rely the total event set (S).
I will spend more time to try the herd itself. Thanks.
-Kenneth
> Andrea
On Sun, Mar 10, 2024 at 03:27:10AM +0100, Andrea Parri wrote:
> Date: Sun, 10 Mar 2024 03:27:10 +0100
> From: Andrea Parri <[email protected]>
> To: [email protected]
> Cc: Alan Stern <[email protected]>, [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> > > Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
> > > is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
> > >
> > > The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
> > >
> > > [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> > > (P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
> > >
> >
> > So the cumul-fence relation includes the same Store? This is hard to
> > understand, because it is defined as:
> >
> > let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> > po-unlock-lock-po) ; [Marked] ; rmw-sequence
> >
> > There is at lease a rmw-sequence in the relation link.
> >
> > I doubt we have different understanding on the effect of
> > reflexive operator. Let's discuss this with an example. Say we have two
> > relation r1 and r2. r1 have (e1, e2) while r2 have (e2, e3). Then we got
> > (e1, e3) for (r1;r2). The (;) operator joins r1's range to r2's domain.
> >
> > If we upgrade (r1;r2) to (r1?;r2), (r1?) become {(m1, m1), (m1, m2), (m2,
> > m2)}, it is r1 plus all identity of all elements used in r1's relations.
> >
> > So (r1?;r2) is {(m1, m3), (m2, m3)}. If we consider this link:
> >
> > e1 ->r1 ->e2 ->r2 e3
> >
> > A question mark on r1 means both (e1, e3) and (e2, e3) are included in
> > the final definition. The r1 is ignore-able in the definition. The event
> > before or behind the ignore-able relation both belong to the definition.
> >
> > But this doesn't means r1 is optional. If r1 is empty, (r1?;r2) will
> > become empty, because there is no event element in r1's relations.
> >
> > So I think the reflexive-transitive operation on cumul-fence cannot make
> > this relation optional. You should first have such link in the code.
>
> In Cat, r1? is better described by (following your own wording) "r1 plus
> all identity of all elements (i.e. not necessarily in r1)".
>
> As an example, in the scenario at stake, cumul-fence is empty while both
> cumul-fence? and cumul-fence* match the identity relation on all events.
>
> Here is a (relatively old, but still accurate AFAICR) article describing
> these and other notions as used in Herd: (cf. table at the bottom)
>
> https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/herd.html
>
> Said this, I do think the best way to familiarize with these notions and
> check one's understanding is to spend time using the herd tool itself.
>
Excuse me, May I ask one last question? I tried the herd tool on the
discussed example. But it seems it is not protected by the hb acyclic
rule. I can replace the linux-kernel.cat with lock.cat on the test:
P0(int *x)
{
int r1;
WRITE_ONCE(*x, 1);
r1 = READ_ONCE(*x);
}
P1(int *x)
{
WRITE_ONCE(*x, 8);
}
locations[0:r1; x]
exists (0:r1=8)
It can still ensure the P0:Wx execute before P0:Rx:
Test test Allowed
States 3
0:r1=1; [x]=1;
0:r1=1; [x]=8;
0:r1=8; [x]=8;
Ok
Witnesses
Positive: 1 Negative: 2
Condition exists (0:r1=8)
Observation test Sometimes 1 2
The example doesn't prove the hb rule is necessary. Is this
understanding correct? Thanks.
> Andrea
--
-Kenneth Lee
On Mon, Mar 11, 2024 at 11:41:27AM +0800, [email protected] wrote:
> Date: Mon, 11 Mar 2024 11:41:27 +0800
> From: [email protected]
> To: Andrea Parri <[email protected]>
> Cc: Alan Stern <[email protected]>, [email protected],
> [email protected]
> Subject: Re: Question about PB rule of LKMM
>
> On Sun, Mar 10, 2024 at 03:27:10AM +0100, Andrea Parri wrote:
> > Date: Sun, 10 Mar 2024 03:27:10 +0100
> > From: Andrea Parri <[email protected]>
> > To: [email protected]
> > Cc: Alan Stern <[email protected]>, [email protected],
> > [email protected]
> > Subject: Re: Question about PB rule of LKMM
> >
> > > > Remark that, in the CAT language, the identity relation ({(e, e) : each event e})
> > > > is a subset of R* (the _reflexive_-transitive closure of R) for any relation R.
> > > >
> > > > The link at stake, (P0:Wx1, P0:Rx), is the result of the following composition:
> > > >
> > > > [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]
> > > > (P0:Wx1, P0:Wx1) (P0:Wx1, P1:Wx8) (P1:Wx8, P1:Wx8) (P1:Wx8, P1:Wx8)) (P1:Wx8, P0:Rx) (P0:Rx, P0:Rx)
> > > >
> > >
> > > So the cumul-fence relation includes the same Store? This is hard to
> > > understand, because it is defined as:
> > >
> > > let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> > > po-unlock-lock-po) ; [Marked] ; rmw-sequence
> > >
> > > There is at lease a rmw-sequence in the relation link.
> > >
> > > I doubt we have different understanding on the effect of
> > > reflexive operator. Let's discuss this with an example. Say we have two
> > > relation r1 and r2. r1 have (e1, e2) while r2 have (e2, e3). Then we got
> > > (e1, e3) for (r1;r2). The (;) operator joins r1's range to r2's domain.
> > >
> > > If we upgrade (r1;r2) to (r1?;r2), (r1?) become {(m1, m1), (m1, m2), (m2,
> > > m2)}, it is r1 plus all identity of all elements used in r1's relations.
> > >
> > > So (r1?;r2) is {(m1, m3), (m2, m3)}. If we consider this link:
> > >
> > > e1 ->r1 ->e2 ->r2 e3
> > >
> > > A question mark on r1 means both (e1, e3) and (e2, e3) are included in
> > > the final definition. The r1 is ignore-able in the definition. The event
> > > before or behind the ignore-able relation both belong to the definition.
> > >
> > > But this doesn't means r1 is optional. If r1 is empty, (r1?;r2) will
> > > become empty, because there is no event element in r1's relations.
> > >
> > > So I think the reflexive-transitive operation on cumul-fence cannot make
> > > this relation optional. You should first have such link in the code.
> >
> > In Cat, r1? is better described by (following your own wording) "r1 plus
> > all identity of all elements (i.e. not necessarily in r1)".
> >
> > As an example, in the scenario at stake, cumul-fence is empty while both
> > cumul-fence? and cumul-fence* match the identity relation on all events.
> >
> > Here is a (relatively old, but still accurate AFAICR) article describing
> > these and other notions as used in Herd: (cf. table at the bottom)
> >
> > https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/herd.html
> >
> > Said this, I do think the best way to familiarize with these notions and
> > check one's understanding is to spend time using the herd tool itself.
> >
>
> Excuse me, May I ask one last question? I tried the herd tool on the
> discussed example. But it seems it is not protected by the hb acyclic
> rule. I can replace the linux-kernel.cat with lock.cat on the test:
>
> P0(int *x)
> {
> int r1;
> WRITE_ONCE(*x, 1);
> r1 = READ_ONCE(*x);
> }
> P1(int *x)
> {
> WRITE_ONCE(*x, 8);
> }
> locations[0:r1; x]
> exists (0:r1=8)
>
> It can still ensure the P0:Wx execute before P0:Rx:
>
> Test test Allowed
> States 3
> 0:r1=1; [x]=1;
> 0:r1=1; [x]=8;
> 0:r1=8; [x]=8;
> Ok
> Witnesses
> Positive: 1 Negative: 2
> Condition exists (0:r1=8)
> Observation test Sometimes 1 2
>
> The example doesn't prove the hb rule is necessary. Is this
> understanding correct? Thanks.
Sorry for disturb, please ignore this. I think the context just to
explain what is prop, not mean to say it can ensure the order.
>
> > Andrea
>
> --
> -Kenneth Lee