Linux-Kernel Memory Ordering: Help Arrives At Last!

Paul E. McKenney
http://linux.conf.au/schedule/present...
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/

• Category

  • Education

• License

  • Creative Commons Attribution license (reuse allowed)