Linux-Kernel Memory Model Workshop

Why frighten small children by reading memory-barriers.txt to them when you can now automate this process with a shiny new tool allegedly implementing the Linux-kernel memory model? This tool takes a “litmus test” that contains concurrent quasi-C code along with an assertion. The tool then tells you whether this assertion always, sometimes, or never triggers after the concurrent quasi-C code completes execution.

To this end, the Linux Plumbers 2017 Linux-Kernel Memory Model Workshop is intended to help Linux-kernel developers with the prototype tooling that has been developed over the past couple of years. A video of a recent presentation is available, as are slides. Slide 98 contains instructions for installing the tool and its dependencies, and attendees should feel free to do the installation before the workshop. Both the first and second articles in a two-part LWN series have also appeared.

Key Attendees (tentative)

  • Alan Stern [*]
  • Paul E. McKenney [*]
  • Will Deacon [*]
  • Steve Rostedt
  • Andrea Parri [*]
  • Dhaval Giani
  • Josh Triplett
  • Jade Alglave [*]
  • Waiman Long
  • Davidlohr Bueso

[*] People so marked have installed and used the tools.

Key Topics for Discussion (tentative)

The following is the list of items presently considered as candidate topics for the microconf. Still very much subject to change.

Installing the memory model and related tools:
* ocaml v4.02.0 or better: http://caml.inria.fr/download.en.html (Or, likely easier, install your distro's version)
  * But if you choose to build it yourself, do yourself a favor and read -all- of Step 5 before starting, or you will miss the "make world.opt" shortcut
  * In addition, recent versions of ocaml require opam (see "herd" README from next step)
* Download and install "herd" tool: http://diy.inria.fr/sources/index.html
* Download and install memory model itself: https://github.com/aparri/memory-model
* (Optional) Download litmus tests: https://github.com/paulmckrcu/litmus
Using the memory model:
* Running the model against existing litmus tests (for example, this one: https://raw.githubusercontent.com/paulmckrcu/litmus/master/auto/C-RW-G%2BRW-Rr%2BRW-Ra.litmus)
  * herd7 -conf linux-kernel.cfg litmus/auto/C-RW-G+RW-Rr+RW-Ra.litmus
* Hardware vs. kernel model
* Constructing litmus tests to use memory model as a design/debugging aid
* Feedback, including from architecture maintainers
* ...

If you wish to try out the snazzy new klitmus7 tool (and you most definitely should!), please bring a running Linux environment that you care so little about that you would be happy to install and run a kernel module generated by a new tool that has not been tested all that thoroughly. (As far as we know, this tool has not yet frightened any small children or eaten any pets, but it is probably only a matter of time.)

Proposed Schedule (tentative)

  • Short overview of the Linux-kernel memory model
  • Assistance installing and using the tools
  • Possible short presentations from users on their experience with and questions about these tools (add your name and topic if you are interested)

Contact

Runner: Paul E. McKenney paulmck@linux.vnet.ibm.com

 
2017/linux-kernel_memory_model_workshop.txt · Last modified: 2017/10/17 13:24 by 50.39.104.80
 
Except where otherwise noted, content on this wiki is licensed under the following license:CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki