Linux-Kernel Memory Ordering: Help Arrives At Last!
Presented by
Paul E. McKenney
Thursday
10:40 a.m.–11:25 a.m.
Target audience:
Developer
Abstract
It has been said that Documentation/memory-barriers.txt can be used to [frighten small children][1], and perhaps this is true. However, it is woefully inefficient. After all, there are a very large number of children in this world, and it would take a huge amount of time and effort to read it to all of them.
This situation clearly calls out for automation, which has been developed over the past two years. An automated tool takes short fragments of C code as input, along with an assertion, and carries out the axiomatic equivalent of a full state-space search to determine whether the assertion always, sometimes, or never triggers. This talk will describe this tool and give a short demonstration of its capabilities.
[1] http://lwn.net/Articles/575835/
Presented by
Paul E. McKenney
Paul E. McKenney has been coding for more than 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 (AKA hiking) along with the usual house-wife-and-kids habit.