Re: [PATCH 0/3] tools/memory-model: Add SRCU support

[Andrea Parri <andrea.parri@amarulasolutions.com>]

On Thu, Nov 15, 2018 at 11:19:24AM -0500, Alan Stern wrote:
> Paul and other LKMM maintainers:
> 
> The following series of patches adds support for SRCU to the Linux
> Kernel Memory Model.  That is, it adds the srcu_read_lock(),
> srcu_read_unlock(), and synchronize_srcu() primitives to the model.
> 
> 	Patch 1/3 does some renaming of the RCU parts of the
> 	memory model's existing CAT code, to help distinguish them
> 	from the upcoming SRCU parts.
> 
> 	Patch 2/3 refactors the definitions of some RCU relations
> 	in the CAT code, in a way that the SRCU portions will need.
> 
> 	Patch 3/3 actually adds the SRCU support.
> 
> This new code requires herd7 version 7.51+4(dev) or later (now 
> available in the herdtools7 github repository) to run.  Thanks to Luc 
> for making the necessary changes to support SRCU.

Thank you Alan, Luc.

My only suggestion is to integrate changes to explanation.txt (in part.,
Sect. 22), which the above renaming and refactoring make out-of-date.

For this version,

Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>

  Andrea


> 
> The code does not check that the index argument passed to 
> srcu_read_unlock() is the same as the value returned by the 
> corresponding srcu_read_lock() call.  This is deemed to be a semantic 
> issue, not directly relevant to the memory model.
> 
> Alan
>