Re: [PATCH 01/13] litmus: Add SRCU fastpath anchor-before-scan test

[Kunwu Chan]

On Tue, 8 Sep 2026 16:58:31 -0700 "Paul E. McKenney" <paulmck@xxxxxxxxxx> wrote:

> On Mon, Sep 07, 2026 at 03:58:17PM +0800, Kunwu Chan wrote:
> > From: Kunwu Chan <kunwu.chan@xxxxxxxxx>
> > 
> > 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>
> 
> Litmus tests!  Very nice!!!  
> 
> Could you please put both of these in Documentation/litmus-tests, in a
> new "srcu" subdirectory?
> 
> One thing for your consideration is use of the "filter" clause for the
> first term of your "exists" clause.  Not a big deal at all for this small
> of a litmus test, but the idea is that this litmus test only cares about
> the 0:r2=0 case:  If that condition does not hold, then P0() and P1()
> aren't the beginning and end of a valid SRCU read-side critical section.
> 
> Use of the "filter" allows herd7 to abandon a given execution early,
> so it is a big deal for larger litmus tests.
> 
> Again, what you have is fine (or will be when moved to the other
> directory), just pointing out the additional feature.
> 
> If you would like to see a use case, please see:
> 
> Documentation/litmus-tests/locking/RM-fixed.litmus

Thanks, Paul.
I’ll move both tests to Documentation/litmus-tests/srcu/ and use a "filter" 
clause for the first test as suggested.

I’ll send the two litmus tests as a separate follow-up series, so this won’t 
hold up the current atomic SRCU series.
I’d also like to continue maintaining the SRCU litmus tests as they evolve. 
If you think a MAINTAINERS entry for the SRCU litmus tests would be appropriate, 
I’d be happy to prepare that as well.

Thanks,
KunWu

> 
> 							Thanx, Paul
> 
> > ---
> >  .../SRCU-fastpath-anchor-before-scan.litmus   | 56 +++++++++++++++++++
> >  1 file changed, 56 insertions(+)
> >  create mode 100644 tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus
> > 
> > diff --git a/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus b/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus
> > new file mode 100644
> > index 000000000000..8200a75e15ef
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus
> > @@ -0,0 +1,56 @@
> > +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();
> > +}
> > +
> > +P2(int *seq, int *ctr)
> > +{
> > +	int r3;
> > +	int r4;
> > +
> > +	r3 = READ_ONCE(*ctr);
> > +	smp_mb();
> > +	r4 = READ_ONCE(*seq);
> > +}
> > +
> > +exists (0:r2 = 0 /\ 2:r3 = 1 /\ 2:r4 = 0)
> > -- 
> > 2.43.0
> > 
> 

Sent using hkml (https://github.com/sjp38/hackermail)