On Thu, Jul 27, 2023 at 5:07 PM Matthew Wilcox <willy@xxxxxxxxxxxxx> wrote: > On Thu, Jul 27, 2023 at 04:39:34PM +0200, Jann Horn wrote: > > The other option is to replace the READ_ONCE() with a > > smp_load_acquire(), at which point it becomes a lot simpler to show > > that the code is correct. > > Aren't we straining at gnats here? The context of this is handling a > page fault, and we used to take an entire rwsem for read. I'm having > a hard time caring about "the extra expense" of an unnecessarily broad > barrier. > > Cost of an L3 cacheline miss is in the thousands of cycles. Cost of a > barrier is ... tens? Yeah, fair point. If it's hard to show correctness with READ_ONCE() we can just use smp_load_acquire() and call it a day.
