Manual

I. Musketeer

``En garde !''
             \

               ~__
                |)
               /|_____
              / |
               /|
              / |
The lastest binaries of musketeer (and goto-cc) for Linux 64 bit are available here (last update: 17 April 2014), along with a fence insertion script. The source can be collected and compiled from here. The old versions are still available below: (changelog)

lastest musketeer17 Apr 2014 binaries source duplicates loop bodies more cleverly
fixed musketeer4 Apr 2014 binaries source fixes a bug spotted during the reviews (thanks!)
first musketeer4 Dec 2013 binaries source first implementation

Our technique is parametrised by the pointer analysis we apply. We provide musketeer, with a precise yet expensive pointer analysis, and lwmusketeer, which uses a lightweight pointer analysis. Note that the experiments for Debian in particular require lwmusketeer.

II. Framework

Musketeer has been developed with the framework CProver 4.3, whose original source is available using
svn co http://www.cprover.org/svn/cbmc/releases/cbmc-4.3

It also requires a SAT solver for compiling. We chose Minisat2 for our experiments, but any SAT/SMT solver supported by the framework will do. (This file can help with this regard)

It also requires the library GLPK.

III. Compiling

Follow the steps described here to install the SAT solver, then compile musketeer with
make musketeer.dir

To compile lwmusketeer, replace in config.inc the flag CXXFLAGS with
CXXFLAGS = -Wall -O2 -DLOCAL_MAY
and compile as before.

IV. Running

Suppose we want to insert some fences in a program my_program.c for an architecture A:

(i) Generate a goto-program:
goto-cc -o my_program.gb my_program.c

(ii) Analyse the goto-program for MM in {tso, pso, rmo, power, arm}:
musketeer --mm MM my_program.gb

(iii) Apply the fence insertion script for A in {x86, ARM} and F in {fence, dp} (inserts fences only or fences and dependencies):
fence-inserter.py A F results.txt

V. Options

* *     musketeer 0.37     * *

              ~__
               |)
              /|_____
             / |
              /|
             / |

Usage:                        Purpose:

 musketeer [-?] [-h] [--help] show help

Main options:

 --mm {tso,pso,rmo,power}     detects all the fences to insert for a weak
                              memory model

Alternative methods:

 --all-shared                 detects and fences all the accesses to shared
                              variables (context insensitive)
 --all-shared-aeg             detects all the accesses to shared variables
                              (context sensitive)
 --volatile                   detects all the accesses to volatile variables
 --pensieve                   detects all the pairs to be delayed with
                              Pensieve's criteria (context sensitive)
 --naive                      detects all the pairs to be delayed in a naive
                              approach (context sensitive)

Options:

 --async                      replaces all the pthread_creates by CPROVER_ASYNC
 --const-function-pointer-propagation
                              propagates the constant pointers to functions
 --scc                        detects critical cycles in parallel (one thread
                              per SCC) (EXPERIMENTAL)
 --force-loop-duplication     duplicates the bodies of all the loops, and not
                              only those with arrays accesses (EXPERIMENTAL)
 --no-loop-duplication        constructs back-edges for all the loops
 --no-dependencies            ignores existing dependencies in the program
 --print-graph                prints the AEG into graph.dot
 --max-po-var {n}             limits the number of variables per cycle
 --max-po-trans {n}           limits the size of pos^+ in terms of pos
 --ignore-arrays              ignores cycles with multiple accesses to the
                              same array

VI. Tutorial

Coming soon...

VII. Responsibilities

THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS `AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.