tools/memory-model Flag suspicious use of srcu cookies

  The herd model of LKMM deviates from actual implementations in the
range of cookies that might be returned by srcu_lock() and similar
functions.  As a consequence, code that relies on srcu_lock()
returning specific values might pass on the herd model but fail in
the real world.

This patch flags any code that looks at the value of a cookie
without passing it on to an srcu_unlock().  This indicates that the
cookie value might be being used in ways that can lead herd to
produce incorrect results, as in the following (contrived) case:

P0(struct srcu_struct *ss)
{
	int r = srcu_read_lock(ss);
	if (r==0)
		srcu_read_unlock(ss, r);
}

Without this patch, the code passes herd7 without any warnings.

With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
indicating that a cookie is used to compute a control condition.
Such scenarios potentially lead to other branches of the code that
are possible in real usage not being evaluated by herd7.  In this
example, this affects the branch where r!=0, which would lead to
an unmatched read side critical section and thus to hangs of
synchronize_srcu() calls.

Besides use of cookies in control conditions, the patch also flags
use in address computation and any time a cookie is inspected but
not later passed to srcu_read_unlock().

Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
---
 tools/memory-model/linux-kernel.bell | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)
  

On Tue, Jan 24, 2023 at 03:39:51PM +0100, Jonas Oberhauser wrote:
> The herd model of LKMM deviates from actual implementations in the
> range of cookies that might be returned by srcu_lock() and similar
> functions.  As a consequence, code that relies on srcu_lock()
> returning specific values might pass on the herd model but fail in
> the real world.
> 
> This patch flags any code that looks at the value of a cookie
> without passing it on to an srcu_unlock().  This indicates that the
> cookie value might be being used in ways that can lead herd to
> produce incorrect results, as in the following (contrived) case:
> 
> P0(struct srcu_struct *ss)
> {
> 	int r = srcu_read_lock(ss);
> 	if (r==0)
> 		srcu_read_unlock(ss, r);
> }
> 
> Without this patch, the code passes herd7 without any warnings.
> 
> With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
> indicating that a cookie is used to compute a control condition.
> Such scenarios potentially lead to other branches of the code that
> are possible in real usage not being evaluated by herd7.  In this
> example, this affects the branch where r!=0, which would lead to
> an unmatched read side critical section and thus to hangs of
> synchronize_srcu() calls.
> 
> Besides use of cookies in control conditions, the patch also flags
> use in address computation and any time a cookie is inspected but
> not later passed to srcu_read_unlock().
> 
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> ---

Acked-by: Alan Stern <stern@rowland.harvard.edu>

>  tools/memory-model/linux-kernel.bell | 12 +++++++++++-
>  1 file changed, 11 insertions(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 6e702cda15e1..db5993acc241 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -58,7 +58,8 @@ flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-unlock
>  
>  (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
>  let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
> -let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc
> +let pass-cookie = carry-srcu-data ; data
> +let srcu-rscs = ([Srcu-lock] ; pass-cookie ; [Srcu-unlock]) & loc
>  
>  (* Validate nesting *)
>  flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-lock
> @@ -71,6 +72,15 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
>  (* Validate SRCU dynamic match *)
>  flag ~empty different-values(srcu-rscs) as bad-srcu-value-match
>  
> +(*
> + * Check that srcu cookies are only used for passing to srcu_unlock()
> + * Note: this check is only approximate
> + *)
> +flag ~empty [Srcu-lock] ; pass-cookie ; rf ;
> +	[~ domain(pass-cookie ; [Srcu-unlock])] as suspicious-srcu-cookie-use
> +flag ~empty [Srcu-lock] ; carry-srcu-data ; ctrl as illegal-srcu-cookie-ctrl
> +flag ~empty [Srcu-lock] ; carry-srcu-data ; addr as illegal-srcu-cookie-addr
> +
>  (* Compute marked and plain memory accesses *)
>  let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
>  		LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
> -- 
> 2.17.1
>
  

On Tue, Jan 24, 2023 at 12:19:24PM -0500, Alan Stern wrote:
> On Tue, Jan 24, 2023 at 03:39:51PM +0100, Jonas Oberhauser wrote:
> > The herd model of LKMM deviates from actual implementations in the
> > range of cookies that might be returned by srcu_lock() and similar
> > functions.  As a consequence, code that relies on srcu_lock()
> > returning specific values might pass on the herd model but fail in
> > the real world.
> > 
> > This patch flags any code that looks at the value of a cookie
> > without passing it on to an srcu_unlock().  This indicates that the
> > cookie value might be being used in ways that can lead herd to
> > produce incorrect results, as in the following (contrived) case:
> > 
> > P0(struct srcu_struct *ss)
> > {
> > 	int r = srcu_read_lock(ss);
> > 	if (r==0)
> > 		srcu_read_unlock(ss, r);
> > }
> > 
> > Without this patch, the code passes herd7 without any warnings.
> > 
> > With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
> > indicating that a cookie is used to compute a control condition.
> > Such scenarios potentially lead to other branches of the code that
> > are possible in real usage not being evaluated by herd7.  In this
> > example, this affects the branch where r!=0, which would lead to
> > an unmatched read side critical section and thus to hangs of
> > synchronize_srcu() calls.
> > 
> > Besides use of cookies in control conditions, the patch also flags
> > use in address computation and any time a cookie is inspected but
> > not later passed to srcu_read_unlock().
> > 
> > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> > ---
> 
> Acked-by: Alan Stern <stern@rowland.harvard.edu>

Thank you both!

I wordsmithed the commit log as follows, but then realized that this
depends on Alan's earlier patch.

Did I miss the official version?  The latest one I have is
message-id Y8q9zjxA620GAFu2@rowland.harvard.edu.

							Thanx, Paul

------------------------------------------------------------------------

From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: paulmck@kernel.org
Cc: stern@rowland.harvard.edu,
	parri.andrea@gmail.com,
	will@kernel.org,
	peterz@infradead.org,
	boqun.feng@gmail.com,
	npiggin@gmail.com,
	dhowells@redhat.com,
	j.alglave@ucl.ac.uk,
	luc.maranget@inria.fr,
	akiyks@gmail.com,
	dlustig@nvidia.com,
	joel@joelfernandes.org,
	urezki@gmail.com,
	quic_neeraju@quicinc.com,
	frederic@kernel.org,
	linux-kernel@vger.kernel.org,
	Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Subject: [PATCH] tools/memory-model Flag suspicious use of srcu cookies
Date: Tue, 24 Jan 2023 15:39:51 +0100

The herd model of LKMM deviates from actual implementations in the
range of cookies that might be returned by srcu_read_lock() and
similar functions.  As a consequence, code that makes special use of
values returned by srcu_read_lock() might pass in herd but fail in the
real world.

This patch flags any code that looks at the value of a cookie
without passing it on to an srcu_unlock().  This indicates that the
cookie value might be being used in ways that can lead herd to
produce incorrect results, as in the following (contrived) case:

P0(struct srcu_struct *ss)
{
	int r = srcu_read_lock(ss);
	if (r==0)
		srcu_read_unlock(ss, r);
}

Without this patch, the above code passes herd7 without any warnings.
However, real-world use of this code could result in SRCU grace-period
hangs.

With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
indicating that a cookie is used to compute a control condition.
Real-world use of such code can result in executions that herd7 does
not evaluate.  In this example, when srcu_read_lock() returns a non-zero
value, there is no matching srcu_read_unlock(), which (as noted above)
would result in calls to synchronize_srcu() never returning.

Besides use of cookies in control conditions, the patch also flags use
in address computation and any time a cookie is inspected but not later
passed to srcu_read_unlock().

Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
---
 tools/memory-model/linux-kernel.bell | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 6e702cda15e1..db5993acc241 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -58,7 +58,8 @@ flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-unlock
 
 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
 let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
-let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc
+let pass-cookie = carry-srcu-data ; data
+let srcu-rscs = ([Srcu-lock] ; pass-cookie ; [Srcu-unlock]) & loc
 
 (* Validate nesting *)
 flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-lock
@@ -71,6 +72,15 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
 (* Validate SRCU dynamic match *)
 flag ~empty different-values(srcu-rscs) as bad-srcu-value-match
 
+(*
+ * Check that srcu cookies are only used for passing to srcu_unlock()
+ * Note: this check is only approximate
+ *)
+flag ~empty [Srcu-lock] ; pass-cookie ; rf ;
+	[~ domain(pass-cookie ; [Srcu-unlock])] as suspicious-srcu-cookie-use
+flag ~empty [Srcu-lock] ; carry-srcu-data ; ctrl as illegal-srcu-cookie-ctrl
+flag ~empty [Srcu-lock] ; carry-srcu-data ; addr as illegal-srcu-cookie-addr
+
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
 		LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
  

On 1/24/2023 8:15 PM, Paul E. McKenney wrote:
> On Tue, Jan 24, 2023 at 12:19:24PM -0500, Alan Stern wrote:
>> On Tue, Jan 24, 2023 at 03:39:51PM +0100, Jonas Oberhauser wrote:
>>> The herd model of LKMM deviates from actual implementations in the
>>> range of cookies that might be returned by srcu_lock() and similar
>>> functions.  As a consequence, code that relies on srcu_lock()
>>> returning specific values might pass on the herd model but fail in
>>> the real world.
>>>
>>> This patch flags any code that looks at the value of a cookie
>>> without passing it on to an srcu_unlock().  This indicates that the
>>> cookie value might be being used in ways that can lead herd to
>>> produce incorrect results, as in the following (contrived) case:
>>>
>>> P0(struct srcu_struct *ss)
>>> {
>>> 	int r = srcu_read_lock(ss);
>>> 	if (r==0)
>>> 		srcu_read_unlock(ss, r);
>>> }
>>>
>>> Without this patch, the code passes herd7 without any warnings.
>>>
>>> With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
>>> indicating that a cookie is used to compute a control condition.
>>> Such scenarios potentially lead to other branches of the code that
>>> are possible in real usage not being evaluated by herd7.  In this
>>> example, this affects the branch where r!=0, which would lead to
>>> an unmatched read side critical section and thus to hangs of
>>> synchronize_srcu() calls.
>>>
>>> Besides use of cookies in control conditions, the patch also flags
>>> use in address computation and any time a cookie is inspected but
>>> not later passed to srcu_read_unlock().
>>>
>>> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
>>> ---
>> Acked-by: Alan Stern <stern@rowland.harvard.edu>
> Thank you both!
>
> I wordsmithed the commit log as follows, but then realized that this
> depends on Alan's earlier patch.

Yeah, I don't know if I did this correctly. I based it on the 
lkmm-srcu.2023.01.20a branch.
Let me know if I should have done this differently.

Looking through your changes to learn for future submissions:

> [...]
>
> This patch flags any code that looks at the value of a cookie
> without passing it on to an srcu_unlock().

You missed this one : )

Have fun, jonas
  

On Tue, Jan 24, 2023 at 11:15:35AM -0800, Paul E. McKenney wrote:
> Thank you both!
> 
> I wordsmithed the commit log as follows, but then realized that this
> depends on Alan's earlier patch.
> 
> Did I miss the official version?  The latest one I have is
> message-id Y8q9zjxA620GAFu2@rowland.harvard.edu.

I wanted to update the patch description before submitting it 
officially, but I haven't gotten around to it yet.

Alan
  

On Tue, Jan 24, 2023 at 08:36:53PM +0100, Jonas Oberhauser wrote:
> 
> 
> On 1/24/2023 8:15 PM, Paul E. McKenney wrote:
> > On Tue, Jan 24, 2023 at 12:19:24PM -0500, Alan Stern wrote:
> > > On Tue, Jan 24, 2023 at 03:39:51PM +0100, Jonas Oberhauser wrote:
> > > > The herd model of LKMM deviates from actual implementations in the
> > > > range of cookies that might be returned by srcu_lock() and similar
> > > > functions.  As a consequence, code that relies on srcu_lock()
> > > > returning specific values might pass on the herd model but fail in
> > > > the real world.
> > > > 
> > > > This patch flags any code that looks at the value of a cookie
> > > > without passing it on to an srcu_unlock().  This indicates that the
> > > > cookie value might be being used in ways that can lead herd to
> > > > produce incorrect results, as in the following (contrived) case:
> > > > 
> > > > P0(struct srcu_struct *ss)
> > > > {
> > > > 	int r = srcu_read_lock(ss);
> > > > 	if (r==0)
> > > > 		srcu_read_unlock(ss, r);
> > > > }
> > > > 
> > > > Without this patch, the code passes herd7 without any warnings.
> > > > 
> > > > With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
> > > > indicating that a cookie is used to compute a control condition.
> > > > Such scenarios potentially lead to other branches of the code that
> > > > are possible in real usage not being evaluated by herd7.  In this
> > > > example, this affects the branch where r!=0, which would lead to
> > > > an unmatched read side critical section and thus to hangs of
> > > > synchronize_srcu() calls.
> > > > 
> > > > Besides use of cookies in control conditions, the patch also flags
> > > > use in address computation and any time a cookie is inspected but
> > > > not later passed to srcu_read_unlock().
> > > > 
> > > > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> > > > ---
> > > Acked-by: Alan Stern <stern@rowland.harvard.edu>
> > Thank you both!
> > 
> > I wordsmithed the commit log as follows, but then realized that this
> > depends on Alan's earlier patch.
> 
> Yeah, I don't know if I did this correctly. I based it on the
> lkmm-srcu.2023.01.20a branch.
> Let me know if I should have done this differently.

You got it right.

> Looking through your changes to learn for future submissions:
> 
> > [...]
> > 
> > This patch flags any code that looks at the value of a cookie
> > without passing it on to an srcu_unlock().
> 
> You missed this one : )

No I didn't!  I missed *two*!  ;-)

Though that comment could be Srcu-unlock, I suppose.  But making it
srcu_read_unlock() seems more straightforward.  Update below!

							Thanx, Paul

------------------------------------------------------------------------

From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: paulmck@kernel.org
Cc: stern@rowland.harvard.edu,
	parri.andrea@gmail.com,
	will@kernel.org,
	peterz@infradead.org,
	boqun.feng@gmail.com,
	npiggin@gmail.com,
	dhowells@redhat.com,
	j.alglave@ucl.ac.uk,
	luc.maranget@inria.fr,
	akiyks@gmail.com,
	dlustig@nvidia.com,
	joel@joelfernandes.org,
	urezki@gmail.com,
	quic_neeraju@quicinc.com,
	frederic@kernel.org,
	linux-kernel@vger.kernel.org,
	Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Subject: [PATCH] tools/memory-model Flag suspicious use of srcu cookies
Date: Tue, 24 Jan 2023 15:39:51 +0100

The herd model of LKMM deviates from actual implementations in the
range of cookies that might be returned by srcu_read_lock() and
similar functions.  As a consequence, code that makes special use of
values returned by srcu_read_lock() might pass in herd but fail in the
real world.

This patch flags any code that looks at the value of a cookie without
passing it on to an srcu_read_unlock().  This indicates that the cookie
value might be being used in ways that can lead herd to produce incorrect
results, as in the following (contrived) case:

P0(struct srcu_struct *ss)
{
	int r = srcu_read_lock(ss);
	if (r==0)
		srcu_read_unlock(ss, r);
}

Without this patch, the above code passes herd7 without any warnings.
However, real-world use of this code could result in SRCU grace-period
hangs.

With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
indicating that a cookie is used to compute a control condition.
Real-world use of such code can result in executions that herd7 does
not evaluate.  In this example, when srcu_read_lock() returns a non-zero
value, there is no matching srcu_read_unlock(), which (as noted above)
would result in calls to synchronize_srcu() never returning.

Besides use of cookies in control conditions, the patch also flags use
in address computation and any time a cookie is inspected but not later
passed to srcu_read_unlock().

Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
---
 tools/memory-model/linux-kernel.bell | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 6e702cda15e1..db5993acc241 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -58,7 +58,8 @@ flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-unlock
 
 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
 let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
-let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc
+let pass-cookie = carry-srcu-data ; data
+let srcu-rscs = ([Srcu-lock] ; pass-cookie ; [Srcu-unlock]) & loc
 
 (* Validate nesting *)
 flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-lock
@@ -71,6 +72,15 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
 (* Validate SRCU dynamic match *)
 flag ~empty different-values(srcu-rscs) as bad-srcu-value-match
 
+(*
+ * Check that srcu cookies are only used for passing to srcu_read_unlock()
+ * Note: this check is only approximate
+ *)
+flag ~empty [Srcu-lock] ; pass-cookie ; rf ;
+	[~ domain(pass-cookie ; [Srcu-unlock])] as suspicious-srcu-cookie-use
+flag ~empty [Srcu-lock] ; carry-srcu-data ; ctrl as illegal-srcu-cookie-ctrl
+flag ~empty [Srcu-lock] ; carry-srcu-data ; addr as illegal-srcu-cookie-addr
+
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
 		LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
  

On Tue, Jan 24, 2023 at 03:52:29PM -0500, Alan Stern wrote:
> On Tue, Jan 24, 2023 at 11:15:35AM -0800, Paul E. McKenney wrote:
> > Thank you both!
> > 
> > I wordsmithed the commit log as follows, but then realized that this
> > depends on Alan's earlier patch.
> > 
> > Did I miss the official version?  The latest one I have is
> > message-id Y8q9zjxA620GAFu2@rowland.harvard.edu.
> 
> I wanted to update the patch description before submitting it 
> officially, but I haven't gotten around to it yet.

Would you like to queue Jonas's patch in the meantime?

Either way works for me, give or take forgetfulness.

							Thanx, Paul
  

On Tue, Jan 24, 2023 at 02:19:15PM -0800, Paul E. McKenney wrote:
> On Tue, Jan 24, 2023 at 08:36:53PM +0100, Jonas Oberhauser wrote:
> > 
> > 
> > On 1/24/2023 8:15 PM, Paul E. McKenney wrote:
> > > On Tue, Jan 24, 2023 at 12:19:24PM -0500, Alan Stern wrote:
> > > > On Tue, Jan 24, 2023 at 03:39:51PM +0100, Jonas Oberhauser wrote:
> > > > > The herd model of LKMM deviates from actual implementations in the
> > > > > range of cookies that might be returned by srcu_lock() and similar
> > > > > functions.  As a consequence, code that relies on srcu_lock()
> > > > > returning specific values might pass on the herd model but fail in
> > > > > the real world.
> > > > > 
> > > > > This patch flags any code that looks at the value of a cookie
> > > > > without passing it on to an srcu_unlock().  This indicates that the
> > > > > cookie value might be being used in ways that can lead herd to
> > > > > produce incorrect results, as in the following (contrived) case:
> > > > > 
> > > > > P0(struct srcu_struct *ss)
> > > > > {
> > > > > 	int r = srcu_read_lock(ss);
> > > > > 	if (r==0)
> > > > > 		srcu_read_unlock(ss, r);
> > > > > }
> > > > > 
> > > > > Without this patch, the code passes herd7 without any warnings.
> > > > > 
> > > > > With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
> > > > > indicating that a cookie is used to compute a control condition.
> > > > > Such scenarios potentially lead to other branches of the code that
> > > > > are possible in real usage not being evaluated by herd7.  In this
> > > > > example, this affects the branch where r!=0, which would lead to
> > > > > an unmatched read side critical section and thus to hangs of
> > > > > synchronize_srcu() calls.
> > > > > 
> > > > > Besides use of cookies in control conditions, the patch also flags
> > > > > use in address computation and any time a cookie is inspected but
> > > > > not later passed to srcu_read_unlock().
> > > > > 
> > > > > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> > > > > ---
> > > > Acked-by: Alan Stern <stern@rowland.harvard.edu>
> > > Thank you both!
> > > 
> > > I wordsmithed the commit log as follows, but then realized that this
> > > depends on Alan's earlier patch.
> > 
> > Yeah, I don't know if I did this correctly. I based it on the
> > lkmm-srcu.2023.01.20a branch.
> > Let me know if I should have done this differently.
> 
> You got it right.
> 
> > Looking through your changes to learn for future submissions:
> > 
> > > [...]
> > > 
> > > This patch flags any code that looks at the value of a cookie
> > > without passing it on to an srcu_unlock().
> > 
> > You missed this one : )
> 
> No I didn't!  I missed *two*!  ;-)
> 
> Though that comment could be Srcu-unlock, I suppose.  But making it
> srcu_read_unlock() seems more straightforward.  Update below!

And I also added this to the lkmm-srcu.2023.01.20a branch just for
experimental purposes.

							Thanx, Paul