[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <e05fa6a9-c810-46cb-b033-b91ae7a5c382@rowland.harvard.edu>
Date: Wed, 6 Mar 2024 13:29:12 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Andrea Parri <parri.andrea@...il.com>
Cc: Kenneth-Lee-2012@...mail.com, linux-kernel@...r.kernel.org,
paulmck@...nel.org
Subject: Re: Question about PB rule of LKMM
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
Powered by blists - more mailing lists