====== McPatom and AVFilter/PPA ======

Available to download at https://reng.sharefile.com/d-s3945ef51b8348888

Tested on Ubuntu

Required Software:
Spin 6.1.0
Pin 2.9

====== Get Spin 6.1.0 ======

http://spinroot.com/fluxbb/viewtopic.php?pid=387

here’s a simple sequence of steps to download, compile, and install Spin on either a Linux system, or a Windows system with cygwin (assuming you have the required commands all installed, and assuming that you have a standard development environment with wget, yacc, gcc, etc.):

wget [url]http://spinroot.com/spin/Src/spin610.tar.gz[/url]
gunzip spin610.tar.gz
tar -xf spin610.tar
cd Spin/Src6.1.0/
make
cp ./spin /usr/local/bin/spin # or wherever your standard bin directory is
make clean

# in linux/ubuntu, you will need to prefix the last command with “sudo ”

on windows, you could also get and install the latest binary like this (you can get wget from cygwin)

wget [url]http://spinroot.com/spin/Bin/spin610.exe[/url]
mv spin610.exe /bin/spin.exe

====== Quick Guide ======

Quick guide: (Spin 6.1.0 required to read the trail files)

In directories including ffmpeg, apache243, run PPA:
python genPoints4PP.py
then check the result by running:
cat Feasible.out
in which each line is a feasible prediction, which can be rescheduled by the Pin tool replay.so.
====== Understanding the result: Feasible.out ======

Each line is a feasible prediction, which can be rescheduled by the Pin tool replay.so, or Spin replaying print_one_trail.sh in the same directory of this README.

Here are examples, in which you can see a predicted interleaving (Wr – Write; Rd – Read), and corresponding source code file name – line number.

alan@pegleg:~/Dropbox/codeblocks/McPatom/test/cav14/CTP-benchmark/atom001$ cat Feasible.out
spin_gCurrentScript.pml.p4.trail

alan@pegleg:~/Dropbox/codeblocks/McPatom/test/cav14/CTP-benchmark/atom001$ ../../print_one_trail.sh spin_gCurrentScript.pml.p4.trail
spin_gCurrentScript.pml.p4.trail
v_gCurrentScript – Wr – Thd 1; /* atom001.c – 45 – (In trace: 13 func: 0) */
v_gCurrentScript – Wr – Thd 2; /* atom001.c – 95 – (In trace: 48 func: 0) */
v_gCurrentScript – Rd – Thd 1; /* atom001.c – 63 – (In trace: 29 func: 0) */
v_gCurrentScript – Rd – Thd 1; /* atom001.c – 66 – (In trace: 30 func: 0) */

alan@pegleg:~/Dropbox/codeblocks/McPatom/test/cav14/CTP-benchmark/banking/av$ cat Feasible.out | sort
spin_ManageAccount_accounts___18.pml.p27.trail
spin_ManageAccount_accounts___27.pml.p28.trail
spin_ManageAccount_accounts___36.pml.p17.trail
spin_ManageAccount_accounts___45.pml.p7.trail
spin_ManageAccount_accounts___54.pml.p7.trail
spin_ManageAccount_accounts___63.pml.p7.trail
spin_ManageAccount_accounts___9.pml.p23.trail
spin_ManageAccount_accounts___9.pml.p25.trail
spin_ManageAccount_accounts___9.pml.p27.trail
spin_ManageAccount_accounts___9.pml.p29.trail
spin_ManageAccount_accounts.pml.p18.trail

alan@pegleg:~/Dropbox/codeblocks/McPatom/test/cav14/CTP-benchmark/banking/av$ ../../../print_one_trail.sh spin_ManageAccount_accounts.pml.p18.trail
spin_ManageAccount_accounts.pml.p18.trail
v_ManageAccount_accounts – Rd – Thd 1; /* banking_av.c – 52 – (In trace: 44 func: 2952637580) */
v_ManageAccount_accounts – Wr – Thd 1; /* banking_av.c – 52 – (In trace: 66 func: 0) */
v_ManageAccount_accounts – Rd – Thd 8; /* banking_av.c – 71 – (In trace: 398 func: 2894692748) */
v_ManageAccount_accounts – Rd – Thd 1; /* banking_av.c – 59 – (In trace: 252 func: 3070567060) */
v_ManageAccount_accounts – Wr – Thd 1; /* banking_av.c – 59 – (In trace: 253 func: 3070567060) */
v_ManageAccount_accounts – Wr – Thd 8; /* banking_av.c – 71 – (In trace: 403 func: 0) */

====== Complete Guide ======

Complete instructions:
1. Instrument the execution using our Pin tool trace.so to capture traces in the file unique_file_name.trace
For ffmpeg, we leverage the test suite by hacking the ‘make’ process:
make V=1 SAMPLES=fate-suite THREADS=2 TARGET_EXEC=”pin -t trace.so — ” fate | tee fate2014_002.log
For Apache,

2. For each captured trace file, put it to a new directory as trace.out and run our checking. E.g., trace.out can be found in each sub-directory of this directory.

3. ./McPatom_PPA.sh Note that the complete model checking can take long time. For PPA only, please just run “python genPoints4PP.py” then check the result by “cat Feasible.out”

4. It will be prompted, or it can be found by opening McPatom.log (tail McPatom.log):
There are n violation patterns predicted in Feasible.out