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

[Paul E. McKenney]

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

							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
>