Hi Alan,
One minor nit. Please find inline comment below.
On Wed, 22 Feb 2023 21:36:04 -0500, Alan Stern wrote:
> Expand the discussion of SRCU and its read-side critical sections in
> the Linux Kernel Memory Model documentation file explanation.txt. The
> new material discusses recent changes to the memory model made in
> commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU
> semantics").
>
> Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Cc: Andrea Parri <andrea.parri@xxxxxxxxxxxxxxxxxxxx>
> Cc: Boqun Feng <boqun.feng@xxxxxxxxx>
> Cc: Jade Alglave <j.alglave@xxxxxxxxx>
> Cc: Luc Maranget <luc.maranget@xxxxxxxx>
> Cc: "Paul E. McKenney" <paulmck@xxxxxxxxxxxxx>
> Cc: Peter Zijlstra <peterz@xxxxxxxxxxxxx>
> Cc: Will Deacon <will.deacon@xxxxxxx>
> Cc: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxx>
>
> ---
>
> Joel, please feel free to add your Co-developed-by and Signed-off-by
> tags to this patch.
>
> tools/memory-model/Documentation/explanation.txt | 178 +++++++++++++++++++++--
> 1 file changed, 167 insertions(+), 11 deletions(-)
>
> Index: usb-devel/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-devel.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-devel/tools/memory-model/Documentation/explanation.txt
> @@ -28,9 +28,10 @@ Explanation of the Linux-Kernel Memory C
> 20. THE HAPPENS-BEFORE RELATION: hb
> 21. THE PROPAGATES-BEFORE RELATION: pb
> 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb
> - 23. LOCKING
> - 24. PLAIN ACCESSES AND DATA RACES
> - 25. ODDS AND ENDS
> + 23. SRCU READ-SIDE CRITICAL SECTIONS
> + 24. LOCKING
> + 25. PLAIN ACCESSES AND DATA RACES
> + 26. ODDS AND ENDS
>
>
>
> @@ -1848,14 +1849,169 @@ section in P0 both starts before P1's gr
> before it does, and the critical section in P2 both starts after P1's
> grace period does and ends after it does.
>
> -Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in
> -addition to normal RCU. The ideas involved are much the same as
> -above, with new relations srcu-gp and srcu-rscsi added to represent
> -SRCU grace periods and read-side critical sections. There is a
> -restriction on the srcu-gp and srcu-rscsi links that can appear in an
> -rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp
> -links having the same SRCU domain with proper nesting); the details
> -are relatively unimportant.
> +The LKMM supports SRCU (Sleepable Read-Copy-Update) in addition to
> +normal RCU. The ideas involved are much the same as above, with new
> +relations srcu-gp and srcu-rscsi added to represent SRCU grace periods
> +and read-side critical sections. However, there are some important
> +differences between RCU read-side critical sections and their SRCU
> +counterparts, as described in the next section.
> +
> +
> +SRCU READ-SIDE CRITICAL SECTIONS
> +--------------------------------
> +
> +The LKMM models uses the srcu-rscsi relation to model SRCU read-side
I think you mean either:
The LKMM models the srcu-rscsi relation ...
or:
The LKMM uses the srcu-rscsi relation ...
With this fixed,
Reviewed-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> +critical sections. They are different from RCU read-side critical
> +sections in the following respects:
> +
[...]
Thanks, Akira
