Re: LKMM: Making RMW barriers explicit

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 





Am 5/23/2024 um 6:35 PM schrieb Andrea Parri:
I would phrase it more extreme: I want to get rid of the unnecessary
non-standard parts of the herd representation.

Please indulge the thought that what might appear to be "non-standard"
to one or one's community might appear differently to others.

Certainly. And of course, the formalization of the LKMM doesn't have to be optimized for the WMM community, even though I suspect that they (and possibly the tools they develop) are the main direct consumers of the formalization.

Continuing with the example above, I'm pretty sure your "standard" and
simple idea of mb-reads and mb-writes, or even "unsuccessful" mb-reads
will turn up the nose of many kernel developers...

I'm not sure how true that is. Firstly I'm not sure how many kernel developers really read the formalization and try to see what it does, rather than relying on tools to gain an intuition of what's going on.

But let's say a kernel developer wants to make sure that their intuition of how cmpxchg works is matched by the formal model, e.g., they want to double check that the formal model is correct
after they got some unexpected results in a herd7 litmus test.

How would they go about it today? The only way is to read the OCaml source code, because there's no other code that obviously defines the behavior. At best, they would read

atomic_cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W)
atomic_cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
atomic_cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W)

see the Acquire, Release, and Mb references in the model, and think "ok, so '__cmpxchg{acquire}' means I get an Acquire tag in the success case which gives acq_po ordering, '__cmpxchg{release}' means I get a Release tag in the success case which gives po_rel ordering. Therefore '__cmpxchg{mb}' must give me an Mb tag in the success case. That would give me mb ordering, but not between the store and subsequent operations, and that's just wrong."

But of course this "understanding by analogy" is broken, because there's a bunch of special OCaml match expressions in herd that look only for release or mb and just give totally different behavior for that one case. Every other tag behaves exactly the same way.

At worst they wouldn't even guess that this only is the success ordering (that's definitely what happened to us in the weak memory model community, but we don't matter for this argument).

A better situation would be to do something like this:

                                       (*success*)(*fail*)
atomic_cmpxchg_acquire(X,V,W) __cmpxchg {acquire}  {once} (X,V,W)
atomic_cmpxchg_release(X,V,W) __cmpxchg {release}  {once} (X,V,W)
atomic_cmpxchg(X,V,W)         __cmpxchg {mb}       {once} (X,V,W)

and being explicit in the model about what the Mb tag does:

| [M];fencerel(Mb);[M] (* smp_mb() and operations with Mb ordering such as cmpxchg() *) | [M];po;[R & Mb] (* reads with an Mb tag - coming from full fence rmws - are ordered as-if there was an smp_mb() right before the read *) | [W & Mb];po;[M] (* correspondingly, writes with an Mb tag are ordered as-if there was an smp_mb() right after the write *)

And suddenly you can read the model and map it 1:1 to the intuition that you can treat a successful cmpxchg() (or an xchg() etc.) as-if it was enclosed by smp_mb().

There doesn't need to be a real fence.


The current repre-
sentation for xchg() was described in the ASPLOS'18 work

Do you mean the one example in Table 3?
What about cmpxchg() or cmpxchg_acquire()?

But that's not the point, "standards" can change and certainly kernels
and tools do.  My remark was more to point out that you're not getting
rid of anything...,

We're definitely getting rid of some lines in herd7, that have been added solely for dealing with this specific case of LKMM.

For example, there's some code looking like this (for a memory ordering tag `a`)

                (match a with ["release"] -> a |  _ -> a_once)

which specifically refers to the release tag in LKMM and we can turn that into

                a

with no more reference to any LKMM tags. Of course, this is not the Linux community's problem, just the herd (and others who want to use the literal cat file of LKMM) maintainers who have to deal with it.

And imagine that at some point you want to add another tag to the linux kernel - like for example for 'accessing an atomic in initialization code, so that the compiler can do optimizations like merge a bunch of bitwise operations'. Let's call it 'init.

What will be the behavior of

WRITE_INIT(X,V) __store{init}(X,V);

with the current herd7? Honestly I have no clue, because there might be a

                (match a with ["release"] -> a |  _ -> a_once)

somewhere that will turn this 'init into 'once. We'd have to comb the herd7 codebase to know for sure (or hope that our experiments are sufficiently thorough to catch all cases).

>you're simply proposing a different representation

I wouldn't phrase it like that, since it's a representation many people familiar with WMM would expect, but admittedly that doesn't have to be the deciding factor.

asking kernel developers & maintainers to "deal with it"

Deal with what, no longer having to learn OCaml to be sure that the LKMM's formal definition matches the description in memory_barriers.txt?
Otherwise, I don't see anything that changes for the worse.
With the change, people need to think for a few seconds to see that the explicit rules in the .cat file are a formalization of "treat xchg() as if it had smp_mb() before and after". Without the change, they need to read an OCaml codebase to see that is meant by

atomic_xchg(X,V,W) __xchg{mb}(X,V,W)

So I don't see any downsides.


I would also support making the representation explicit in the .def files instead, with something like

cmp_xchg(x,e,v) = { if (*x==e) { smp_mb(); int r = __cmp_xchg{once}(x,e,v) ; smp_mb(); return r } else { __read{once}(x) } }

Then you get to keep the representation.
Without knowing herd's internals, I have no idea of how to seriously specify a meta language so that herd could effectively and efficiently deal with it in general. But one could at least envision some specific syntax for cmpxchg with a code sequence for the failure case and a code sequence for the success case.

Personally I don't prefer this option, firstly because I don't see a good reason for the Linux community to go their own way here. I don't think there's really much of a problem with saying "this is the intuition; this is how we formalize it" and for the two not to be completely identical. It happens all the time, and in this case the gap between "we formalize it by really having two smp_mb() appear in the graph if it's successful" and "we formalize it by providing the same ordering that the smp_mb() would have if it was there" isn't big. Especially for those kernel people who have enough motivation to actually deep dive into the formalization in the first place. But it makes it a lot more accessible for the WMM community, which can only benefit LKMM.

And secondly because people will probably mostly focus on the .cat file, which means that it's still a bit of a booby trap to put something so important (and perhaps surprising) into the .def file, but at least one that is in the open for people who are more careful and also read the .def file.

> I am looking forward to something more than "because we can".

- it makes it easier to maintain the LKMM in the future, because you don't have to work around hidden transformations inside herd7
- it makes implicit behavior explicit
- it makes it easier to understand that the formalization matches the intention - it makes it easier to learn the LKMM from the formalization without having to cross-reference every bit with the informal documentation to avoid misunderstandings


Have a good time,
  jonas








[Index of Archives]     [Linux Kernel]     [Kernel Newbies]     [x86 Platform Driver]     [Netdev]     [Linux Wireless]     [Netfilter]     [Bugtraq]     [Linux Filesystems]     [Yosemite Discussion]     [MIPS Linux]     [ARM Linux]     [Linux Security]     [Linux RAID]     [Samba]     [Device Mapper]

  Powered by Linux