LinuxCon+ContainerCon Europe 2016

It has been said that Documentation/memory-barriers.txt can be used to frighten small children, and perhaps this is true. But even if it is true, it is woefully inefficient. After all, there is a huge number of children in this world, so a correspondingly huge amount of time and effort would be required in order to read it to them all.

This situation clearly calls for an automated tool, which is the topic of this talk, and which is now available in prototype form. This tool takes short fragments of concurrent C code as input, and exhaustively analyzes the possible results. In other words, instead of perusing memory-barriers.txt to find the answer to a memory-ordering question, you can get your answer by writing a small test case and feeding it to the tool. This talk will give an introduction to this tool, describing how to use it and how it works, including a short demo.