Contents
Manual
I. Musketeer
``En garde !''
\
~__
|)
/|_____
/ |
/|
/ |
|
|
| lastest musketeer | 17 Apr 2014 | binaries | source | duplicates loop bodies more cleverly |
| fixed musketeer | 4 Apr 2014 | binaries | source | fixes a bug spotted during the reviews (thanks!) |
| first musketeer | 4 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