Linux-Kernel Memory Model Workshop track

Friday, September 15, 2017 from 9:30am12:30pm
Platinum C

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.

It might be a bit early for experience reports, but they would nevertheless be quite welcome! Propose them if you’ve got them!!!



Microconference Leader

Paul McKenney

Proposals for this track

* LKMM Installation and Use Workshop

Get LKMM installed and make use of it! (slides)
Linux-Kernel Memory Model Workshop 05/18/2017
Paul McKenney

* LKMM overview

Quick overview of Linux kernel memory model: How to install and use (slides)
Linux-Kernel Memory Model Workshop 05/18/2017
Paul McKenney