Message-ID: <44749eab-90b0-489d-a409-c6a5cc7b8e04@rowland.harvard.edu>
Date: Sat, 11 Jan 2025 16:19:45 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: paulmck@...nel.org, parri.andrea@...il.com, will@...nel.org,
	peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
	dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
	akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
	urezki@...il.com, quic_neeraju@...cinc.com, frederic@...nel.org,
	linux-kernel@...r.kernel.org, lkmm@...ts.linux.dev,
	hernan.poncedeleon@...weicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA

On Sat, Jan 11, 2025 at 01:46:21PM +0100, Jonas Oberhauser wrote:
> What I want is to change the interpretation of ctrl,data,addr in LKMM from
> saying "it is intended to be a syntactic dependency, which causes LKMM to be
> inaccurate" to "it is intended to be a semantic dependency, but because
> there is no formal defn. and tooling we *use* syntactic dependencies, which
> causes the current implementations to be inaccurate", without formally
> defining what a semantic dependency is.

I guess you could take that point of view.  We have never tried to make 
it explicit.

> E.g., in "A WARNING", I would change
> -------------
> The protections provided by READ_ONCE(), WRITE_ONCE(), and others are
> not perfect; and under some circumstances it is possible for the
> compiler to undermine the memory model.
> -------------
> into something like
> -------------
> The current tooling around LKMM does not model semantic dependencies, and
> instead uses syntactic dependencies to specify the protections provided by
> READ_ONCE(), WRITE_ONCE(), and others. The compiler can undermine these
> syntactic dependencies under some circumstances.
> As a consequence, the tooling may write checks that LKMM and the compiler
> can not cash.
> -------------
> 
> etc.

I doubt the ordinary reader would appreciate the difference.

How would you feel about changing the existing text this way instead?

	... it is possible for the compiler to undermine the memory
	model (because the LKMM and the software tools associated with 
	it do not understand the somewhat vague concept of "semantic 
	dependency" -- see below).

> This is under my assumption that if we had let's say gcc's "semantic
> dependencies" or an under-approximation of it (by that I mean allow less
> things to be dependent than gcc can see), that these cases would be
> resolved, in the sense that gcc can not undermine [R & Marked] ; gcc-dep
> where gcc-dep is the dependencies detected by gcc.

That seems circular.  Basically, you're saying the gcc will not break 
any dependencies that gcc classifies as not-breakable!

> But I would be interested to see any cases where this assumption is not
> true.
> 
> 
> Note that this still results in a fully formal definition of LKMM, because
> just like now, addr,ctrl,and data are simply uninterpreted relations. We
> don't need to formalize their meaning at that level.

> > > > Perhaps so.  LKMM does include other features which the compiler can
> > > > defeat if the programmer isn't sufficiently careful.
> > > 
> > > How many of these are due to herd7's limitations vs. in the cat file?
> > 
> > Important limitations are present in both.
> 
> I am genuinely asking. Do we have a list of the limitations?
> Maybe it would be good to collect it in the "A WARNING" section of
> explanation.txt if it doesn't exist elsewhere.

There are a few listed already at various spots in explanation.txt -- 
search for "undermine".  And yes, many or most of these limitations do 
arise from LKMM's failure to recognize when a dependency isn't semantic.  
Maybe some are also related to undefined behavior, which LKMM is not 
aware of.

There is one other weakness I know of, however -- something totally 
different.  It's an instance in which the formal model in the .cat file 
fails to capture the intent of the informal operational model.

As I recall, it goes like this: The operational model asserts that an 
A-cumulative fence (like a release fence) on a CPU ensures ordering for 
all stores that propagate to that CPU before the fence is executed.  But 
the .cat code says only that this ordering applies to stores which the 
CPU reads from before the fence is executed.  I believe you can make up 
litmus tests where you can prove that a store must have propagated to 
the CPU before an A-cumulative fence occurs, even though the CPU doesn't 
read from that store; for such examples the LKMM may accept executions 
that shouldn't be allowed.

There may even be an instance of this somewhere in the various litmus 
test archives; I don't remember.

> > An execution of the corresponding machine code would then be compatible
> > with an abstract execution of the source code in which both r0 and r1
> > get set to 42 (OOTA).  But it would also be compatible with an abstract
> > execution in which both r0 and r1 are 0, so it doesn't make sense to say
> > that the hardware execution is, or might be, an instance of OOTA.
> 
> Yes, but this does not require the definition you expressed before. This is
> already not observable according to the definition that there is no read R
> from an OOTA-cycle store, where some observable side effect semantically
> depends on R.

Yes.  This was not meant to be an exact analogy.  It was merely an 
observation of a concept closely related to something you said.

> What I was trying to say is that your definition is almost a
> no-true-scotsman (sorry Paul) definition:

(I would use the term "tautology" -- although I don't believe it was a 
tautology in its original context, which referred specifically to cases 
where the compiler had removed all the accesses in an OOTA cycle.)

>  every program with an OOTA
> execution where you could potentially not find an "equivalent" execution
> without OOTA, is simply labeled a "no-true-unobserved OOTA".
> 
> > > But it does make the proof of your claim totally trivial. If there is no
> > > other OOTA-free execution with the same observable behavior, then it is
> > > proof that the OOTA happened, so the OOTA was observed.
> > > So by contraposition any non-observed OOTA has an OOTA-free execution with
> > > the same observable behavior.
> > > 
> > > The sense in which I would define observed is more along the lines of "there
> > > is an observable side effect (such as store to volatile location) which has
> > > a semantic dependency on a load that reads from one of the stores in the
> > > OOTA cycle".

Agreed.  But maybe this indicates that your sense is too weak a 
criterion, that an indirect observation should count just as much as a 
direct one.

Alan

Powered by blists - more mailing lists