Don't sit on the fence
A static analysis approach to automatic fence insertion
Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency between threads. As both the semantics of the program under these architectures and the semantics of these fences may be subtle, the automation of their placement is highly desirable. However, precise methods to restore strong consistency do not scale to the size of deployed systems code. We choose to trade some precision for genuine scalability: we present a novel technique suitable for interprocedural analysis of large code bases. We implement this method in our new musketeer tool, and detail experiments on more than 350 executables of packages found in a Debian Linux distribution, e.g. memcached (about 10000 LoC).
|April 4th 2014||A fixed version of the tool is now available|
|Jan 20th 2014||Comparison with other static approaches for Debian experiments|
|Dec 4th 2013||Release of the tool|
Paper (CAV 2014) and arXiv version.
Tool and tool manual
Here is the tool musketeer and its manual.
``En garde !'' \ ~__ |) /|_____ / | /| / |
Here are all our experimental data, for both the parametric and Debian benchmarks. We also implemented other static approaches and compared them to musketeer on the Debian experiments. We further provide data about the overhead of programs with fences inserted by musketeer and other approaches and compiled with gcc -O1.
Here are the formal definitions of the transformers in p. 10 that construct the abstract event graph from a goto-program. We also explain here how to construct the abstract event graph to capture recursion. (not yet implemented in the tool)
The benchmarks Classic, Fast and Param can be downloaded here.