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 three years, and which has recently been accepted into the Linux kernel [2] and was presented at ASPLOS 2018 [3]. 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 [4]. This talk will describe this tool and its history, and will also give a short demonstration of its capabilities.
[1] http://lwn.net/Articles/575835/
[2] git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git in the directory tools/memory-model
[3] https://dl.acm.org/citation.cfm?id=3177156
[4] http://lwn.net/Articles/608550/
Bio:
Paul E. McKenney is a Distinguished Engineer with the IBM Linux
Technology Center, where he maintains the RCU implementation
within the Linux kernel. He has been coding for four decades,
and more than half of that on parallel hardware. His prior
lives include working on the DYNIX/ptx kernel at Sequent, work
on packet radio, Internet protocols, and system administration
at SRI International, and work on soft-realtime systems as a
self-employed contract programmer. His hobbies include what
passes for running at his age (AKA hiking) along with the usual
house-wife-and-grown-kids habit.