Linux-Kernel Memory Ordering: Help Arrives At Last!

  • Date Wednesday, May 16, 2018  Time 11:00 AM
  • Speaker Paul E. McKenney
  • Location Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

    This talk will also be live streamed on our YouTube channel


It has been said that Documentation/memory-barriers.txt can be used to frighten small children [1], and perhaps this is true. However, it is woefully inefficient.  After all, there are a very large number of children in this world, and it would take a huge amount of time and effort to read it to all of them.

This situation clearly calls out for automation, which has been developed over the past three years, and which has recently been accepted into the Linux kernel [2] and was presented at ASPLOS 2018 [3].  An automated tool takes short fragments of C code as input, along with an assertion, and carries out the axiomatic equivalent of a full state-space search to determine whether the assertion always, sometimes, or never triggers [4]. This talk will describe this tool and its history, and will also give a short demonstration of its capabilities.

[2] git:// in the directory tools/memory-model


Paul E. McKenney is a Distinguished Engineer with the IBM Linux
Technology Center, where he maintains the RCU implementation
within the Linux kernel. He has been coding for four decades,
and more than half of that on parallel hardware. His prior
lives include working on the DYNIX/ptx kernel at Sequent, work
on packet radio, Internet protocols, and system administration
at SRI International, and work on soft-realtime systems as a
self-employed contract programmer. His hobbies include what
passes for running at his age (AKA hiking) along with the usual
house-wife-and-grown-kids habit.