A big “thank you” to all my partners in LKMM crime, most especially to Jade, Luc, Andrea, and Alan! Jade presented our paper (slides, supplementary material) at ASPLOS, which was well-received. A number of people asked how they could learn more about LKMM, which is what much of this blog post is about.
Approaches to learning LKMM include:
- Read the documentation, starting with explanation.txt. This documentation replaces most of the older LWN series.
- Go through Ted Cooper‘s coursework for Portland State University‘s CS510 Advanced Topics in Concurrency class, taught by Jon Walpole.
- Those interested in the history of LKMM might wish to look at my 2017 linux.conf.au presentation (video).
- Play with the actual model.
The first three options are straightforward, but playing with the model requires some installation. However, playing with the model is probably key to gaining a full understanding of LKMM, so this installation step is well worth the effort.
Installation instructions may be found here (see the “REQUIREMENTS” section). The ocaml language is a prerequisite, which is fortunately included in many Linux distros. If you choose to install ocaml from source (for example, because you need a more recent version), do yourself a favor and read the instructions completely before starting the build process! Otherwise, you will find yourself learning of the convenient one-step build process only after carrying out the laborious five-step process, which can be a bit frustrating.
Of course, if you come across better methods to quickly, easily, and thoroughly learn LKMM, please do not keep them a secret!
Those wanting a few rules of thumb safely approximating LKMM should look at slide 96 (PDF page 78) of the aforementioned linux.conf.au presentation. Please note that material earlier in the presentation is required to make sense of the three rules of thumb.
We also got some excellent questions during Jade’s ASPLOS talk, mainly from the renowned and irrepressible Sarita Adve:
- Question: How do we know that the model is correct?
Answer: We verified the model socially and experimentally. [ Ed. note: See Section 1 and Table 5 of the paper and the “Detailed hardware results” from the supplementary materials. ] - Question: What is the intuition behind the model?
Answer: There are a number of axioms, for example, the RCU axiom, that correspond to various intuitions. Additional axioms correspond to the load buffering and store buffering intuitions. - Question: How did you decide what to provide? For example, what about one of Paul’s favorite primitives, sequence locking?
Answer: The paper shows memory barrier, loads and stores, acquire and release, and read-modify-write atomic operations. We have since added locking, which in combination with some of the other operations allows sequence locking to be easily implemented within litmus tests. [ Ed. note: Not sure that sequence locking makes my list of favorites, but we do have a pair of sequence-locking litmus tests in preparation. ]
There were of course a great many other excellent presentations at ASPLOS, but that is a topic for another post!
paulmckrcu 