Re: [PATCH v2] tools: memory-model: Make plain accesses carry dependencies

[Boqun Feng]

On Mon, Dec 05, 2022 at 01:42:46PM +0000, Jonas Oberhauser wrote:
> > Without it, I guess the rationale of this patch is "plain accesses
> > shouldn't be weaker than registers" or "This (plain accesses don't
> > provide dependencies) is too conservative", and these don't seem
> > very strong without a bigger motivation behind it.
> 
> Good points, thanks.
> 
> 
> -----Original Message-----
> From: Boqun Feng [mailto:boqun.feng@xxxxxxxxx] 
> Sent: Sunday, December 4, 2022 9:33 AM
> >
> >  a real world code usage that needs this fix
> 
> Note that in the standard C world, 'int a' (and even 'register int a')
> declares an object, i.e., a memory location that is accessed with
> plain accesses. In my opinion, that 'int a' is a "register" in herd7
> is an implementation artifact that hides the current weakness
> addressed by this patch. So if you would actually analyze pretty much
> any code that looks like
> 
>    int a = <some atomic load>
>    if (a == ...) { <some atomic store> }
> 
> then under the standard interpretation of that code, a is a memory
> location, and there is (in current LKMM) no control dependency, and
> the code would be considered broken by LKMM.
> 
> Or in another view, whether something that is (provably) never
> accessed externally is to be considered a 'register' or a 'memory
> location' should be an implementation detail of the compiler etc.
> (with the possibility to freely do reg2mem/mem2reg), and not have any
> effect on the ordering guarantees. Notably most tools (GenMC for sure
> and I think also Dat3M) use such compiler transformations (especially
> mem2reg) because they live under the assumption that it doesn't change
> anything, but of course with current LKMM that renders all of these
> tools unsound; if you would carefully avoid to do any such
> transformations, then these tools would also report bugs in a lot more
> linux code.
> 

Thanks! This is exactly what I want to see ;-) Now I understand more
about the rationale of this change:

First, Linux kernel developers expect and use dependencies ordering.

Second, herd modeling has the concept of "registers" that carries the
dependency because herd also models asm code where "registers" do exist.

Third, for C standard or other models' viewpoint, LKMM has some
inconsistency since both "int a" and "*z" are "memory locations",
however LKMM currently respects dependencies carried by the first but
not those carried by the latter.

Finally, to close the gap with LKMM+herd with other model tools and C
standard, all dependencies that carried by "memory locations" should be
enforced in LKMM.

I must say I didn't get the "Third" part from your patch at first, now
re-read your patch, I think you did mention that in some degree. I guess
the reason I did get it first is because my mind is herded ;-)

How about adding some comments before "carry-dep", for example:

(* Redefine dependencies to include those carried through plain
accesses, since herd by default only generates dependencies via
"registers", while LKMM enforces dependencies carried by "memory
location" of C standard *)

I guess Alan and Paul can do better job on wording, so that just
expresses my idea. Maybe instead of saying "Make plain accesses carry
dependencies", we say "Make memory location carry dependencies" or
"Extend dependency carrying from registers to memory locations".

Thoughts?

> 
> 
> 
> > Also I'm in the impression that people love to put
> > READ_ONCE()/WRITE_ONCE() when they have some ordering issues (in
> > real world or with LKMM). 
> 
> Note that this would require to do 
> 
>   int a; WRITE_ONCE(&a, <some_atomic_load>); if (READ_ONCE(&a) == ...)
>   { <some_atomic_store>; }
> 
> to get a control dependency, and imho violate the point of relaxed
> marked accesses -- to point out where races are, but no (additional)
> ordering is required.
> 
> > Although I don't like this
> 
> I like this and I have forwarded Paul's email to some friends who like

"So you are these guys" ;-) I guess I shouldn't say "I don't like this",
I'm OK with either way since I also understand the benefit you mentioned
below.

> not to put relaxed marked/atomic accesses in their code "because it
> makes the code less readable". I completely disagree -- marking racy
> accesses makes the code more readable because it lets us know when
> something is subject to concurrent access, and modifying the logic may
> break code of other threads.
> 
> What I don't like is relying on dependencies in the first place, since
> they are hard to maintain -- some innocuous optimizations that people
> might want to do (like adding some read in front of a bunch of writes
> to see if they're really necessary) bypass the ordering imposed by the
> dependency. So I generally advise to use acq loads instead, unless
> there is a measurable performance impact. But that's a completely
> separate discussion...
> 

True. I actually agree with the "acq loads first, unless performance
benefit" approach.

[I will reply the ctrl/addr in a separate mail]

Regards,
Boqun