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

[Linus Torvalds]

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".

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?

               Linus