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.01.0 or better: http://caml.inria.fr/download.en.html (Or, likely easier, install your distro's version)
  * But read -all- of Step 5 before starting, or you will miss the "make world.opt" shortcut
* Download and install "herd" tool: http://diy.inria.fr/sources/index.html
* Download and install memory model itself: http://www.rdrop.com/users/paulmck/scalability/paper/LCA-LinuxMemoryModel.2017.01.15a.tgz
* (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 strong.cfg litmus/auto/C-RW-G+RW-Rr+RW-Ra.litmus
* Strong vs. weak model
* Constructing litmus tests to use memory model as a design/debugging aid
* Feedback, including from architecture maintainers
* ...

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/05/23 19:41 by 9.70.82.110
 
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