Re: LKMM litmus test for Roman Penyaev's rcu-rr

[Paul E. McKenney]

On Thu, Jun 07, 2018 at 08:06:51AM -0700, Linus Torvalds wrote:
> On Thu, Jun 7, 2018 at 2:41 AM Paul E. McKenney
> <paulmck@xxxxxxxxxxxxxxxxxx> wrote:
> >
> > We are considering adding unmarked accesses, for example, accesses
> > protected by locks.  One possible litmus test (not yet supported!)
> > might look like this:
> 
> Fair enough - you do want to have the distinction between "marked" and
> "unmarked".
> 
> And it does make sense, although at that point I think you do hit the
> "what can a compiler do" issue more. Right now, I think the things you
> check are all pretty much "compiler can't do a lot of movement".

Agreed, and the added freedom unmarked accesses give the compiler is
one reason why this is something being thought about as opposed to
something already done.  The approach that looks most feasible is to
make LKMM complain if there is a data race involving unmarked accesses.
This is a bit annoying given the Linux kernel's large number of unmarked
accesses to shared variable that do involve data races, however, my
belief is that developers and maintainers of such code are under the
obligation to make sure that the compiler cannot mess them up.  One
way that they could do this is to list the transformations that the
compiler could carry out, and make a separate litmus test for each,
substituting READ_ONCE() and WRITE_ONCE() for the unmarked accesses.

Then unmarked accesses would be for code protected by locks or that
used dependencies to avoid data races.

Thoughts?

> But I suspect that the markings you do have are going to be fairly
> limited. Things like "READ_ONCE()" vs "smp_read_acquire()" are still
> fairly simple from a compiler standpoint, at least when it comes to
> control flow - they have "side effects". So I guess that's the only
> real difference there - a regular read doesn't have side effects, so
> it could be moved up past a conditional, and/or duplicated for each
> use. That sounds much more complex to the checker than the existing
> things it supports, no?

Indeed!

And those sorts of compiler transformations are one of the things that
has pushed us to the "no data races" model.  If there are no data races,
then those compiler transformations don't affect the outcome, given that
C11 and later compilers are not allowed to introduce data races.

							Thanx, Paul