A Formal Model of Linux-Kernel Memory Ordering

Session information has not yet been published for this event.

60 Minute BoF session
Scheduled: Thursday, November 3, 2016 from 7:00 – 8:00pm in Sweeney AB

One Line Summary

Review, explore, and critique a draft formal model of Linux-kernel memory ordering.


This BoF session will give an overview and some demos of a draft Linux-kernel formal memory model. This memory model is designed to accommodate the range of hardware that the kernel runs on as well as the range of use cases within the Linux kernel, and can be thought of as a formalization of and extension to Documentation/memory-barriers.txt. As far as we know, this is the first realistic formal memory model for the Linux kernel, and the first formal memory model of any kind that correctly models RCU.

Joint work with Jade Alglave, Luc Maranget, Andrea Parri, and Alan Stern.


kernel, concurrency, formal methods


  • Italy2010a

    Paul McKenney

    IBM Linux Technology Center


    Paul E. McKenney has been coding for almost four decades, more than half of that on parallel hardware, where his work has earned him a reputation among some as a flaming heretic. Over the past decade, Paul has been an IBM Distinguished Engineer at the IBM Linux Technology Center. Paul maintains the RCU implementation within the Linux kernel, where the variety of workloads present highly entertaining performance, scalability, real-time response, and energy-efficiency challenges. Prior to that, he worked on the DYNIX/ptx kernel at Sequent, and prior to that on packet-radio and Internet protocols (but long before it was polite to mention Internet at cocktail parties), system administration, business applications, and real-time systems. His hobbies include what passes for running at his age along with the usual house-wife-and-kids habit.