Hi,
* Paul E. McKenney <[email protected]> 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
