Re: seqcount usage in xt_replace_table()

[Andrea Parri]

On Thu, Jan 10, 2019 at 01:38:11PM +0100, Dmitry Vyukov wrote:
> On Thu, Jan 10, 2019 at 1:30 PM Andrea Parri
> <andrea.parri@xxxxxxxxxxxxxxxxxxxx> wrote:
> >
> > > For seqcounts we currently simply ignore all accesses within the read
> > > section (thus the requirement to dynamically track read sections).
> > > What does LKMM say about seqlocks?
> >
> > LKMM does not currently model seqlocks, if that's what you're asking;
> > c.f., tools/memory-model/linux-kernel.def for a list of the currently
> > supported synchronization primitives.
> >
> > LKMM has also no notion of "data race", it insists that the code must
> > contain no unmarked accesses; we have been discussing such extensions
> > since at least Dec'17 (we're not quite there!, as mentioned by Paul).
> 
> How does it call cases that do contain unmarked accesses then? :)

"work-in-progress" ;), or "limitation" (see tools/memory-model/README)


> 
> > My opinion is that ignoring all accesses within a given read section
> > _can_ lead to false negatives
> 
> Absolutely. But this is a deliberate decision.
> For our tools we consider priority 1: no false positives. Period.
> Priority 2: also report some true positives in best effort manner.

This sound reasonable to me.  But please don't overlook the fact that
to be able to talk about "false positive" and "false negative" (for a
data race detector) we need to agree about "what a data race is".

(The hope, of course, is that the LKMM will have a say soon here ...)

  Andrea


> 
> > (in every possible definition of "data
> > race" and "read sections" I can think of at the moment ;D):
> >
> >         P0                              P1
> >         read_seqbegin()                 x = 1;
> >         r0 = x;
> >         read_seqretry() // =0
> >
> > ought to be "racy"..., right?  (I didn't audit all the callsites for
> > read_{seqbegin,seqretry}(), but I wouldn't be surprised to find such
> > pattern ;D ... "legacy", as you recalled).
> >
> >   Andrea