Don't sit on the fence
A static analysis approach to automatic fence insertion

Abstract

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).

News
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

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.


Formal Definitions

Here are the formal definitions of the transformers in p. 10 that construct the abstract event graph from a goto-program.


Benchmarks

The benchmarks Classic, Fast and Param can be downloaded here.


People