lkml.org 
[lkml]   [2018]   [May]   [15]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: [PATCH memory-model 0/19] Updates to the formal memory model
    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

    \
     
     \ /
      Last update: 2018-05-15 18:19    [W:3.766 / U:0.836 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site