1. build LLVM:
cd roundup_inspect/
mkdir build
cd build/
make; make install

2. build Inspect:
cd roundup_inspect/

3. build examples:
Benchmarks/examples : our hand made examples
Benchmarks/scal-benchmarks : the scal benchmarks

go to any folder of the example, for example "Benchmarks/scal-benchmarks/k-stack":
run: make
The makefiles of our examples are already replace with insp++, which is to compile the example with instrumented LLVM
To complie your own examples, please run"make CXX="../../../bin/insp++ --linCheck" or modify your makefile accordingly.

4. run examples:
In the scal benchmark folder, there are some scripts for your reference
For example, inside the k-stack folder:
run: ../run   -- to automatically check linearizability and quasi linearizability
In the handmade example, run ./ in each folder

5. general usage of the tool:
To generate specs: the first argument is 0
../../../inspect-0.3/inspect --linCheck 0 ./spec.exe 
To check linearizability: the first argument is 1
../../../inspect-0.3/inspect --linCheck 1 ./impl.exe
to check quasi linearizability: the first argument is 2, the second is the quasi factor
../../../inspect-0.3/inspect --linCheck 2 1 ./impl.exe

6. Important files:
The quasi linearizability check algorithm is in:
inspect-64bit/src/, lin_checker.hh

7. Envoriment:
We used Ubuntu 12.04-64 bit, with gcc4.6
Thank you for your interest!