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|
Tool and tool manual
Here is the tool musketeer and its manual.
``En garde !'' \ ~__ |) /|_____ / | /| / |
Here are the formal definitions of the transformers in p. 10 that construct the abstract event graph from a goto-program.
The benchmarks Classic, Fast and Param can be downloaded here.