Re: [PATCH memory-model 0/19] Updates to the formal memory model

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Tue, May 15, 2018 at 08:15:45AM +0200, Ingo Molnar wrote:
> 
> Hi,
> 
> * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> 
> > Hello!
> > 
> > This series contains updates to the Linux kernel's formal memory model in
> > tools/memory-model.  These are ready for inclusion into -tip.
> > 
> > 1.	Rename LKMM's "link" and "rcu-path" relations to "rcu-link"
> > 	and "rb", respectively, courtesy of Alan Stern.
> > 
> > 2.	Redefine LKMM's "rb" relation in terms of rcu-fence in order
> > 	to match the structure of LKMM's other strong fences, courtesy
> > 	of Alan Stern.
> > 
> > 3.	Update required version of herdtools7, courtesy of Akira Yokosawa.
> > 
> > 4.	 Fix cheat sheet typo: "RWM" should be "RMW", courtesy of Paolo Bonzini.
> > 
> > 5.	Improve cheatsheet.txt key for SELF and SV.
> > 
> > 6.	Fix cheatsheet.txt to note that smp_mb__after_atomic() orders
> > 	later RMW operations.
> > 
> > 7.	Model smp_store_mb(), courtesy of Andrea Parri.
> > 
> > 8.	Fix coding style in 'linux-kernel.def', courtesy of Andrea Parri.
> > 
> > 9.	Add scripts to test the memory model.
> > 
> > 10.	Add model support for spin_is_locked(), courtesy of Luc Maranget.
> > 
> > 11.	Flag the tests that exercise "cumulativity" and "propagation".
> > 
> > 12.	Remove duplicated code from lock.cat, courtesy of Alan Stern.
> > 
> > 13.	Improve comments in lock.cat, courtesy of Alan Stern.
> > 
> > 14.	Improve mixed-access checking in lock.cat, courtesy of Alan Stern.
> > 
> > 15.	Remove out-of-date comments and code from lock.cat, which have
> > 	been obsoleted by the settled-upon spin_is_locked() semantics,
> > 	courtesy of Alan Stern.
> > 
> > 16.	Fix coding style in 'lock.cat', bringing the indentation to
> > 	Linux-kernel standard, courtesy of Andrea Parri.
> > 
> > 17.	Update Andrea Parri's email address in the MAINTAINERS file,
> > 	oddly enough courtesy of Andrea Parri.  ;-)
> > 
> > 18.	Update ASPLOS information now that ASPLOS has come and gone,
> > 	courtesy of Andrea Parri.
> > 
> > 19.	Add reference for 'Simplifying ARM concurrency', courtesy
> > 	of Andrea Parri.
> > 
> > 								Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> >  MAINTAINERS                                                               |    2 
> >  tools/memory-model/Documentation/cheatsheet.txt                           |    7 
> >  tools/memory-model/Documentation/explanation.txt                          |  261 +++++-----
> >  tools/memory-model/Documentation/references.txt                           |   17 
> >  tools/memory-model/README                                                 |    2 
> >  tools/memory-model/linux-kernel.bell                                      |    4 
> >  tools/memory-model/linux-kernel.cat                                       |   53 +-
> >  tools/memory-model/linux-kernel.def                                       |   34 -
> >  tools/memory-model/litmus-tests/.gitignore                                |    1 
> >  tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus          |    2 
> >  tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus    |   35 +
> >  tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus      |   34 +
> >  tools/memory-model/litmus-tests/README                                    |   19 
> >  tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus |    4 
> >  tools/memory-model/lock.cat                                               |  197 ++++---
> >  tools/memory-model/scripts/checkalllitmus.sh                              |   73 ++
> >  tools/memory-model/scripts/checklitmus.sh                                 |   86 +++
> >  17 files changed, 595 insertions(+), 236 deletions(-)
> 
> Applied this and the other two series to the locking tree, thanks Paul!
> 
> I ended up editing some of the changelogs and titles, to better organize them:
> 
> 99c12749b172: tools/memory-model: Add reference for 'Simplifying ARM concurrency'
> 1a00b4554d47: tools/memory-model: Update ASPLOS information
> 5ccdb7536ebe: MAINTAINERS, tools/memory-model: Update e-mail address for Andrea Parri
> 05604e7e3adb: tools/memory-model: Fix coding style in 'lock.cat'
> cee0321a404f: tools/memory-model: Remove out-of-date comments and code from lock.cat
> 30b795df11a1: tools/memory-model: Improve mixed-access checking in lock.cat
> fd0359dbac3d: tools/memory-model: Improve comments in lock.cat
> 8559183ccaec: tools/memory-model: Remove duplicated code from lock.cat
> 1bd3742043fa: tools/memory-model: Flag "cumulativity" and "propagation" tests
> 15553dcbca06: tools/memory-model: Add model support for spin_is_locked()
> 2fb6ae162f25: tools/memory-model: Add scripts to test memory model
> d17013e0bac6: tools/memory-model: Fix coding style in 'linux-kernel.def'
> bf8c6d963d16: tools/memory-model: Model 'smp_store_mb()'
> bfd403bb3617: tools/memory-order: Update the cheat-sheet to show that smp_mb__after_atomic() orders later RMW operations
> 35bb6ee67906: tools/memory-order: Improve key for SELF and SV
> a839195186a2: tools/memory-model: Fix cheat sheet typo
> 5b62832c1e52: tools/memory-model: Update required version of herdtools7
> 9d036883a179: tools/memory-model: Redefine rb in terms of rcu-fence
> 1ee2da5f9b5a: tools/memory-model: Rename link and rcu-path to rcu-link and rb
> 1362ae43c503: locking/spinlocks: Clean up comment and #ifndef for {,queued_}spin_is_locked()
> c6f5d02b6a0f: locking/spinlocks/arm64: Remove smp_mb() from arch_spin_is_locked()
> b7e4aadef28f: locking/spinlocks: Document the semantics of spin_is_locked()
> 173af2613efd: locking/Documentation: Use `warning` RST directive
> fc7bdc90249b: locking/Documentation: Fix incorrect example code
> e89641dd038a: locking/memory-barriers.txt/kokr: Update Korean translation to de-emphasize smp_read_barrier_depends() some more
> e2ba8041f2ed: locking/memory-barriers.txt/kokr: Update Korean translation to fix description of data dependency barriers
> df9e0cc85c01: locking/memory-barriers.txt/kokr: Update Korean translation to cross-reference "tools/memory-model/"
> 1ea32723c42a: locking/memory-barriers.txt/kokr: Update Korean translation to de-emphasize smp_read_barrier_depends()
> eabed716672c: locking/memory-barriers.txt/kokr: Update Korean translation to indicate that READ_ONCE() now implies smp_barrier_depends()
> 5846581e3563: locking/memory-barriers.txt: Fix broken DMA vs. MMIO ordering example

Very good, I will follow this style for the next merge window.

> In particular the Korean translation commits are IMHO more readable in this 
> fashion. I also simplified the translation commits internally:
> 
>     Translate this commit to Korean:
>     
>       f28f0868feb1 ("locking/memory-barriers: De-emphasize smp_read_barrier_depends() some more")

I have passed this on to SeongJae, and will check as well.

							Thanx, Paul