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

[Ingo Molnar <mingo@kernel.org>]

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

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")

Thanks,

	Ingo