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 2014A fixed version of the tool is now available
Jan 20th 2014Comparison with other static approaches for Debian experiments
Dec 4th 2013Release of the tool


Paper (CAV 2014) and arXiv version.

Tool and tool manual

Here is the tool musketeer and its manual.

``En garde !''

              / |
              / |         

Experimental Results

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.

Formal Definitions

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.