Re: [PATCH v2 1/2] Documentation/litmus-tests: Add SRCU fastpath anchor-before-scan test

[KunWu Chan]

On Sun, Sep 13, 2026 at 5:48 PM Akira Yokosawa <akiyks@xxxxxxxxx> wrote:
>
> Hi,
>
> This is more of a knee-jerk reaction, but
>
> On Sat, 12 Sep 2026 10:42:24 +0800, Kunwu Chan wrote:
> > synchronize_srcu_atomic() may end its grace period immediately when
> > its scan of the per-CPU lock counters finds no readers.  Correctness
> > requires the grace-period anchor written by srcu_gp_start() to precede
> > the smp_mb() ordering the lock scan.  This ordering ensures that any
> > reader whose lock increment is missed by the scan cannot have
> > incremented its lock counter before the grace-period anchor, and
> > therefore cannot be a pre-existing reader of this grace period.
> >
> > This litmus test models the key ordering between the grace-period
> > anchor and the lock counter scan, where "seq" models the
> > grace-period anchor in ->srcu_gp_seq and "ctr" models the per-CPU
> > ->srcu_ctrs[].srcu_locks counter.  P0 writes the anchor before the
> > smp_mb() and the lock scan.  P1 models the reader-side counter
> > increment, with the smp_mb() of __srcu_read_lock() following the
> > increment.  P2 models an observer that sees the reader's increment
> > before seeing the anchor.
> >
> > The outcome is forbidden by LKMM, and herd7 reports "Never".  See
> > SRCU-fastpath-scan-before-anchor.litmus for the reversed ordering,
> > which permits this outcome.
> >
> > Tested with herd7 7.58 using linux-kernel.cfg.
> >
> > Signed-off-by: Kunwu Chan <kunwu.chan@xxxxxxxxx>
> > ---
> >  .../SRCU-fastpath-anchor-before-scan.litmus   | 57 +++++++++++++++++++
> >  1 file changed, 57 insertions(+)
> >  create mode 100644 Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus
> >
> > diff --git a/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus b/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus
> > new file mode 100644
> > index 000000000000..efa9c0c4e047
> > --- /dev/null
> > +++ b/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus
> > @@ -0,0 +1,57 @@
> > +C SRCU-fastpath-anchor-before-scan
> > +
> > +(*
> > + * Result: Never
> > + *
> > + * The synchronize_srcu_atomic() fastpath may end its grace period
> > + * immediately when its scan of the per-CPU lock counters finds no
> > + * readers.  Correctness requires the grace-period anchor written by
> > + * srcu_gp_start() to precede the smp_mb() ordering the lock scan.
> > + * This ordering ensures that any reader whose lock increment is missed
> > + * by the scan cannot have incremented its lock counter before the
> > + * grace-period anchor, and therefore cannot be a pre-existing reader
> > + * of this grace period.
> > + *
> > + * This litmus test models the key ordering between the grace-period
> > + * anchor and the lock counter scan, where "seq" models the
> > + * grace-period anchor in ->srcu_gp_seq and "ctr" models the per-CPU
> > + * ->srcu_ctrs[].srcu_locks counter.  P0 writes the anchor before the
> > + * smp_mb() and the lock scan.  P1 models the reader-side counter
> > + * increment, with the smp_mb() of __srcu_read_lock() following the
> > + * increment.  P2 models an observer that sees the reader's increment
> > + * before seeing the anchor.
> > + *
> > + * The outcome is forbidden by LKMM, and herd7 reports "Never".  See
> > + * SRCU-fastpath-scan-before-anchor.litmus for the reversed ordering,
> > + * which permits this outcome.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *seq, int *ctr)
> > +{
> > +     int r2;
> > +
> > +     WRITE_ONCE(*seq, 1);
> > +     smp_mb();
> > +     r2 = READ_ONCE(*ctr);
> > +}
> > +
> > +P1(int *ctr)
> > +{
> > +     WRITE_ONCE(*ctr, 1);
> > +     smp_mb();
> > +}
>
> As P1() has a single memory access, this smp_mb() can't have any
> effect on the outcome.
>
> The one you see in "__srcu_read_lock() following the increment" is
> there for other ordering requirements, I guess.
>
> Ditto smp_mb() in P1() of 2/2.

Hi Akira,

Good catch — P1's smp_mb() is indeed vacuous as written.  I'll add a
critical-section access after it to match __srcu_read_lock()'s
semantics.  The verdicts don't change, but the barrier now has
something to order.

Will include the fix in v3.

Thanks,
KunWu

>
> Thanks, Akira
>
> > +
> > +P2(int *seq, int *ctr)
> > +{
> > +     int r3;
> > +     int r4;
> > +
> > +     r3 = READ_ONCE(*ctr);
> > +     smp_mb();
> > +     r4 = READ_ONCE(*seq);
> > +}
> > +
> > +filter (0:r2 = 0)
> > +exists (2:r3 = 1 /\ 2:r4 = 0)
> > --
> > 2.43.0