* Question about PB rule of LKMM @ 2024-03-01 3:18 Kenneth-Lee-2012 2024-03-05 18:00 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-01 3:18 UTC (permalink / raw) To: linux-kernel 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-01 3:18 Question about PB rule of LKMM Kenneth-Lee-2012 @ 2024-03-05 18:00 ` Andrea Parri 2024-03-06 9:53 ` Kenneth-Lee-2012 0 siblings, 1 reply; 23+ messages in thread From: Andrea Parri @ 2024-03-05 18:00 UTC (permalink / raw) To: Kenneth-Lee-2012; +Cc: linux-kernel, stern, paulmck (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. ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-05 18:00 ` Andrea Parri @ 2024-03-06 9:53 ` Kenneth-Lee-2012 2024-03-06 17:36 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-06 9:53 UTC (permalink / raw) To: Andrea Parri; +Cc: linux-kernel, stern, paulmck 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 <parri.andrea@gmail.com> > To: Kenneth-Lee-2012@foxmail.com > Cc: linux-kernel@vger.kernel.org, stern@rowland.harvard.edu, > paulmck@kernel.org > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-06 9:53 ` Kenneth-Lee-2012 @ 2024-03-06 17:36 ` Andrea Parri 2024-03-06 18:29 ` Alan Stern 0 siblings, 1 reply; 23+ messages in thread From: Andrea Parri @ 2024-03-06 17:36 UTC (permalink / raw) To: Kenneth-Lee-2012; +Cc: linux-kernel, stern, paulmck > > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-06 17:36 ` Andrea Parri @ 2024-03-06 18:29 ` Alan Stern 2024-03-06 19:24 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Alan Stern @ 2024-03-06 18:29 UTC (permalink / raw) To: Andrea Parri; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-06 18:29 ` Alan Stern @ 2024-03-06 19:24 ` Andrea Parri 2024-03-07 0:45 ` Kenneth-Lee-2012 2024-03-07 15:52 ` Andrea Parri 0 siblings, 2 replies; 23+ messages in thread From: Andrea Parri @ 2024-03-06 19:24 UTC (permalink / raw) To: Alan Stern; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-06 19:24 ` Andrea Parri @ 2024-03-07 0:45 ` Kenneth-Lee-2012 2024-03-07 15:52 ` Andrea Parri 1 sibling, 0 replies; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-07 0:45 UTC (permalink / raw) To: Andrea Parri; +Cc: Alan Stern, linux-kernel, paulmck 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 <parri.andrea@gmail.com> > To: Alan Stern <stern@rowland.harvard.edu> > Cc: Kenneth-Lee-2012@foxmail.com, linux-kernel@vger.kernel.org, > paulmck@kernel.org > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-06 19:24 ` Andrea Parri 2024-03-07 0:45 ` Kenneth-Lee-2012 @ 2024-03-07 15:52 ` Andrea Parri 2024-03-07 17:25 ` Alan Stern 1 sibling, 1 reply; 23+ messages in thread From: Andrea Parri @ 2024-03-07 15:52 UTC (permalink / raw) To: Alan Stern; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck 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 <parri.andrea@gmail.com> 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 <Kenneth-Lee-2012@foxmail.com> Signed-off-by: Andrea Parri <parri.andrea@gmail.com> --- 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 ^ permalink raw reply related [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 15:52 ` Andrea Parri @ 2024-03-07 17:25 ` Alan Stern 2024-03-07 18:18 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Alan Stern @ 2024-03-07 17:25 UTC (permalink / raw) To: Andrea Parri; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck 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 <parri.andrea@gmail.com> > 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 <Kenneth-Lee-2012@foxmail.com> > Signed-off-by: Andrea Parri <parri.andrea@gmail.com> > --- > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 17:25 ` Alan Stern @ 2024-03-07 18:18 ` Andrea Parri 2024-03-07 18:30 ` Alan Stern 0 siblings, 1 reply; 23+ messages in thread From: Andrea Parri @ 2024-03-07 18:18 UTC (permalink / raw) To: Alan Stern; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 18:18 ` Andrea Parri @ 2024-03-07 18:30 ` Alan Stern 2024-03-07 19:08 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Alan Stern @ 2024-03-07 18:30 UTC (permalink / raw) To: Andrea Parri; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 18:30 ` Alan Stern @ 2024-03-07 19:08 ` Andrea Parri 2024-03-07 19:46 ` Alan Stern 2024-03-08 3:10 ` Kenneth-Lee-2012 0 siblings, 2 replies; 23+ messages in thread From: Andrea Parri @ 2024-03-07 19:08 UTC (permalink / raw) To: Alan Stern; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck > > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 19:08 ` Andrea Parri @ 2024-03-07 19:46 ` Alan Stern 2024-03-07 21:06 ` Andrea Parri 2024-03-08 3:10 ` Kenneth-Lee-2012 1 sibling, 1 reply; 23+ messages in thread From: Alan Stern @ 2024-03-07 19:46 UTC (permalink / raw) To: Andrea Parri; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 19:46 ` Alan Stern @ 2024-03-07 21:06 ` Andrea Parri 2024-03-08 17:54 ` Alan Stern 0 siblings, 1 reply; 23+ messages in thread From: Andrea Parri @ 2024-03-07 21:06 UTC (permalink / raw) To: Alan Stern; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck > > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 21:06 ` Andrea Parri @ 2024-03-08 17:54 ` Alan Stern 2024-03-08 21:29 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Alan Stern @ 2024-03-08 17:54 UTC (permalink / raw) To: Andrea Parri; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-08 17:54 ` Alan Stern @ 2024-03-08 21:29 ` Andrea Parri 0 siblings, 0 replies; 23+ messages in thread From: Andrea Parri @ 2024-03-08 21:29 UTC (permalink / raw) To: Alan Stern; +Cc: Kenneth-Lee-2012, linux-kernel, paulmck > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-07 19:08 ` Andrea Parri 2024-03-07 19:46 ` Alan Stern @ 2024-03-08 3:10 ` Kenneth-Lee-2012 2024-03-08 21:38 ` Andrea Parri 1 sibling, 1 reply; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-08 3:10 UTC (permalink / raw) To: Andrea Parri; +Cc: Alan Stern, linux-kernel, paulmck 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 <parri.andrea@gmail.com> > To: Alan Stern <stern@rowland.harvard.edu> > Cc: Kenneth-Lee-2012@foxmail.com, linux-kernel@vger.kernel.org, > paulmck@kernel.org > 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) ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-08 3:10 ` Kenneth-Lee-2012 @ 2024-03-08 21:38 ` Andrea Parri 2024-03-09 5:43 ` Kenneth-Lee-2012 0 siblings, 1 reply; 23+ messages in thread From: Andrea Parri @ 2024-03-08 21:38 UTC (permalink / raw) To: Kenneth-Lee-2012; +Cc: Alan Stern, linux-kernel, paulmck > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-08 21:38 ` Andrea Parri @ 2024-03-09 5:43 ` Kenneth-Lee-2012 2024-03-10 2:27 ` Andrea Parri 0 siblings, 1 reply; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-09 5:43 UTC (permalink / raw) To: Andrea Parri; +Cc: Alan Stern, linux-kernel, paulmck 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 <parri.andrea@gmail.com> > To: Kenneth-Lee-2012@foxmail.com > Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org, > paulmck@kernel.org > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-09 5:43 ` Kenneth-Lee-2012 @ 2024-03-10 2:27 ` Andrea Parri 2024-03-10 2:52 ` Kenneth-Lee-2012 ` (2 more replies) 0 siblings, 3 replies; 23+ messages in thread From: Andrea Parri @ 2024-03-10 2:27 UTC (permalink / raw) To: Kenneth-Lee-2012; +Cc: Alan Stern, linux-kernel, paulmck > > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-10 2:27 ` Andrea Parri @ 2024-03-10 2:52 ` Kenneth-Lee-2012 2024-03-11 3:41 ` Kenneth-Lee-2012 [not found] ` <20240311034104.7iffcia4k5rxvgog@kllt01> 2 siblings, 0 replies; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-10 2:52 UTC (permalink / raw) To: Andrea Parri; +Cc: Alan Stern, linux-kernel, paulmck 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 <parri.andrea@gmail.com> > To: Kenneth-Lee-2012@foxmail.com > Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org, > paulmck@kernel.org > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: Question about PB rule of LKMM 2024-03-10 2:27 ` Andrea Parri 2024-03-10 2:52 ` Kenneth-Lee-2012 @ 2024-03-11 3:41 ` Kenneth-Lee-2012 [not found] ` <20240311034104.7iffcia4k5rxvgog@kllt01> 2 siblings, 0 replies; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-11 3:41 UTC (permalink / raw) To: Andrea Parri; +Cc: Alan Stern, linux-kernel, paulmck 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 <parri.andrea@gmail.com> > To: Kenneth-Lee-2012@foxmail.com > Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org, > paulmck@kernel.org > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
[parent not found: <20240311034104.7iffcia4k5rxvgog@kllt01>]
* Re: Question about PB rule of LKMM [not found] ` <20240311034104.7iffcia4k5rxvgog@kllt01> @ 2024-03-11 8:20 ` Kenneth-Lee-2012 0 siblings, 0 replies; 23+ messages in thread From: Kenneth-Lee-2012 @ 2024-03-11 8:20 UTC (permalink / raw) To: Andrea Parri; +Cc: Alan Stern, linux-kernel, paulmck On Mon, Mar 11, 2024 at 11:41:27AM +0800, Kenneth-Lee-2012@foxmail.com wrote: > Date: Mon, 11 Mar 2024 11:41:27 +0800 > From: Kenneth-Lee-2012@foxmail.com > To: Andrea Parri <parri.andrea@gmail.com> > Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org, > paulmck@kernel.org > 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 <parri.andrea@gmail.com> > > To: Kenneth-Lee-2012@foxmail.com > > Cc: Alan Stern <stern@rowland.harvard.edu>, linux-kernel@vger.kernel.org, > > paulmck@kernel.org > > 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 ^ permalink raw reply [flat|nested] 23+ messages in thread
end of thread, other threads:[~2024-03-11 8:21 UTC | newest] Thread overview: 23+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2024-03-01 3:18 Question about PB rule of LKMM Kenneth-Lee-2012 2024-03-05 18:00 ` Andrea Parri 2024-03-06 9:53 ` Kenneth-Lee-2012 2024-03-06 17:36 ` Andrea Parri 2024-03-06 18:29 ` Alan Stern 2024-03-06 19:24 ` Andrea Parri 2024-03-07 0:45 ` Kenneth-Lee-2012 2024-03-07 15:52 ` Andrea Parri 2024-03-07 17:25 ` Alan Stern 2024-03-07 18:18 ` Andrea Parri 2024-03-07 18:30 ` Alan Stern 2024-03-07 19:08 ` Andrea Parri 2024-03-07 19:46 ` Alan Stern 2024-03-07 21:06 ` Andrea Parri 2024-03-08 17:54 ` Alan Stern 2024-03-08 21:29 ` Andrea Parri 2024-03-08 3:10 ` Kenneth-Lee-2012 2024-03-08 21:38 ` Andrea Parri 2024-03-09 5:43 ` Kenneth-Lee-2012 2024-03-10 2:27 ` Andrea Parri 2024-03-10 2:52 ` Kenneth-Lee-2012 2024-03-11 3:41 ` Kenneth-Lee-2012 [not found] ` <20240311034104.7iffcia4k5rxvgog@kllt01> 2024-03-11 8:20 ` Kenneth-Lee-2012
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).