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

[KunWu Chan]

On Tue, Sep 15, 2026 at 4:34 PM Akira Yokosawa <akiyks@xxxxxxxxx> wrote:
>
> Hi,
>
> On 9/14/26 23:39, 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 and its smp_mb() from __srcu_read_lock(), which orders
> > the increment against subsequent critical-section access.  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   | 58 +++++++++++++++++++
> >  1 file changed, 58 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..e0492a4d8e07
> > --- /dev/null
> > +++ b/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus
> > @@ -0,0 +1,58 @@
> > +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 and its smp_mb() from __srcu_read_lock(), which orders the
> > + * increment against subsequent critical-section access.  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, int *x)
> > +{
> > +     WRITE_ONCE(*ctr, 1);
> > +     smp_mb();
> > +     WRITE_ONCE(*x, 1);
> > +}
> > +
> > +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)
>
> Another knee-jerk reaction with exaggeration  :-)
>
> Why does P1() have an access to an un-shared variable x ?
> smp_mb() in P1() can't pair with any of other thread's smp_mb().
> This doesn't make sense!
>
> Let me rephrase.
>
> Litmus tests is supposed to be minimal.
> Every memory access and memory barrier is expected to
> have some effect in the outcome of the test.

Thanks Akira, you are right.

>
> In this case,
>
> P1(int *ctr)
> {
>         WRITE_ONCE(*ctr, 1);
> }
>
> should be good enough, I guess.

I'll change in v4.

Thanks,
Kunwu

>
> (That is, IF I understand what you are testing here...)
>
> Regards, Akira
>