Symbiosis Tutorial

 

This page provides a simple tutorial on how to run and use Symbiosis -- a tool that automatically isolates concurrency bugs. See our PLDI’15 paper for a full description of this system.


The source code, as well as a virtual machine ready to use, can be found in the following links:


- Source code (github)

  1. -VirtualBox image (the default keyboard configuration in the VM is Portuguese; click on the button “Pt” at the top right corner of the screen and choose the option English to switch keyboard configurations)


Notes:

- All the Symbiosis components and the required additional tools (e.g. LLVM) are already built and ready to use.

  1. -All test cases are already compiled, and the concrete traces from failing executions (extension .traceBB) can be found in the respective folder for each test subject. In turn, the Differential Schedule Projections (DSPs) for all test cases can be found in folder /home/symbiosis/work/symbiosis/SymbiosisSolver/tmp/DSP

  2. -The programs have sleeps injected to increase the failure rate. However, the bug is still not guaranteed to appear in every run.

-  Since the executions of the programs are non-deterministic and the bug can be triggered at different points in time, the traces and the DSPs are not guaranteed to be always identical (for instance, for some cases they might exhibit less events).

- the root credentials for the VM are: username: symbiosis ; password: symbiosis


=== TEST CASES - C/C++ ===


#CRASHER

Compile and run non-instrumented version

$ make plain

$ ./Crasher


Compile instrumented version (applies LLVM pass)

$ make RUN


Run instrumented version and generate trace with thread execution paths

$ export SYMBTRACE=$PWD/crasher.traceBB

$ export LD_LIBRARY_PATH=/home/symbiosis/work/symbiosis/SymbiosisRuntime/

$ ./CrasherRUN_inst //according to whether the execution fails or not, the trace file created will have the extension ".fail" or ".ok"


Compile symbolic version

make KLEE


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ /home/symbiosis/work/symbiosis/SymbiosisSE/Release+Asserts/bin/symbiosisse --allow-external-sym-calls --bb-trace=$PWD/crasher.traceBB.fail CrasherKLEE_inst.bc

$ cd klee-last; ls | grep -v ^T | xargs rm       //delete all output files excepting the thread symbolic traces

//Unfortunately, the symbolic execution engine is not able to obtain the id of the threads when capturing join events. As such, it is necessary to manually insert those thread ids in the trace file. For Crasher, it suffices to change each event of type "CrasherKLEE.c@...:S-join-0" in the file /klee-last/T0_-1 to "CrasherKLEE.c@...:S-join_<id>-0", where <id> in {1, 2, 3, 4, 5} (i.e. each event will correspond to the join operation of a given thread)


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosis/Tests/crasher/klee-last --model=$PWD/tmp/modelCrasher.txt --solution=$PWD/tmp/failCrasher.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/crasher/      


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --fix-mode --model=$PWD/tmp/modelCrasher.txt --solution=$PWD/tmp/failCrasher.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/crasher/


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failCrasher_Alt0.gv -o dsp_failCrasher_Alt0.ps


Example of a possible DSP for program Crasher:



From the figure it is possible to see that the bug occurs when the read on variable shrPtr at line 46 (assert(shrdPtr != NULL)) returns the value written at line 17 (*old = NULL). However, the bug will not occur if shrPtr at line 46 receives the value written at line 32 (shrdPtr = newval), as shown by the alternate schedule on the right. Moreover, note that the DSP suggests that the block of instructions from lines 27-33 should execute contiguously. Looking at the source code, this is actually a valid fix for the bug.




#PBZIP2

(Note: The following commands consider _testSMALL.tar as the input, but the same procedure applies for inputs _testMEDIUM.tar.gz and _testLARGE.tar.gz)

Compile and run non-instrumented version

$ make plain

$ ./pbzip2 -k -f _testSMALL.tar


Compile insmake trumented version (applies LLVM pass)

$ make RUN


Run instrumented version and generate trace with thread execution paths

$ export SYMBTRACE=$PWD/pbzip2.traceBB

$ export LD_LIBRARY_PATH=/home/symbiosis/work/symbiosis/SymbiosisRuntime/

$ ./pbzip2RUN_inst -k -f _testSMALL.tar


Compile symbolic version

$ make KLEE


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ /home/symbiosis/work/symbiosis/SymbiosisSE/Release+Asserts/bin/symbiosisse --allow-external-sym-calls --bb-trace=$PWD/pbzip2.traceBB.fail pbzip2KLEE_inst.bc -k -f _testSMALL.tar        //this might take some seconds to finish

$ cd klee-last; ls | grep -v ^T | xargs rm      

//Unfortunately, the symbolic execution engine is not able to obtain the id of the threads when capturing join events. As such, it is necessary to manually insert those thread ids in the trace file. For pbzip2, it suffices to change each event of type "pbzip2KLEE.c@...:S-join-0" in the file /klee-last/T0_-1... to "pbzip2KLEE.c@...:S-join_<id>-0", where <id> corresponds to the highest thread id created (for the small test case it's 2)


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosis/Tests/pbzip2/klee-last --model=$(pwd)/tmp/modelPbzip2.txt --solution=$(pwd)/tmp/failPbzip2.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/pbzip2/        


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --model=$(pwd)/tmp/modelPbzip2.txt --solution=$(pwd)/tmp/failPbzip2.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/pbzip2/ --fix-mode


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failPbzip2_Alt0.gv -o dsp_failPbzip2_Alt0.ps



#STRINGBUFFER

Compile and run non-instrumented version

$ make

$ ./main


Compile instrumented version (applies LLVM pass)

$ make RUN


Run instrumented version and generate trace with thread execution paths

$ export SYMBTRACE=$PWD/stringbuffer.traceBB

$ export LD_LIBRARY_PATH=/home/symbiosis/work/symbiosis/SymbiosisRuntime/

$ ./mainRUN_inst


Compile symbolic version

$ make KLEE


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ /home/symbiosis/work/symbiosis/SymbiosisSE/Release+Asserts/bin/symbiosisse --allow-external-sym-calls --bb-trace=$PWD/stringbuffer.traceBB.fail mainKLEE_inst.bc

$ cd klee-last; ls | grep -v ^T | xargs rm      


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosis/Tests/stringbuffer/klee-last --model=$PWD/tmp/modelStringbuffer.txt --solution=$(pwd)/tmp/failStringbuffer.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/stringbuffer


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosis/Tests/stringbuffer/klee-last --model=$(pwd)/tmp/modelStringbuffer.txt --solution=$(pwd)/tmp/failStringbuffer.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/stringbuffer --fix-mode


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failStringbuffer_Alt0.gv -o dsp_failStringbuffer_Alt0.ps



#PFSCAN

Compile and run non-instrumented version

$ make lnx

$ ./pfscan -n4 jalbert inputs/modeltype2.h


Compile instrumented version (applies LLVM pass)

make RUN


Run instrumented version and generate trace with thread execution paths

$ export SYMBTRACE=$PWD/pfscan.traceBB

$ export LD_LIBRARY_PATH=/home/symbiosis/work/symbiosis/SymbiosisRuntime/

$ ./pfscanRUN_inst -n4 jalbert inputs/modeltype2.h


Compile symbolic version

$ make KLEE


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ /home/symbiosis/work/symbiosis/SymbiosisSE/Release+Asserts/bin/symbiosisse --allow-external-sym-calls --bb-trace=$PWD/pfscan.traceBB pfscanKLEE_inst.bc -n4 jalbert inputs/modeltype2.h       

$ cd klee-last; ls | grep -v ^T | xargs rm     


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosis/Tests/pfscan/klee-last --model=$PWD/tmp/modelPfscan.txt --solution=$(pwd)/tmp/failPfscan.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/pfscan


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosis/Tests/pfscan/klee-last --model=$(pwd)/tmp/modelPfscan.txt --solution=$(pwd)/tmp/failPfscan.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/stringbuffer --fix-mode


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failPfscan_Alt0.gv -o dsp_failPfscan_Alt0.ps





=== TEST CASES - JAVA ===


#AIRLINE

Run non-instrumented version

$ cd /home/symbiosis/work/symbiosisJava/Tests/

$ java airline.airline ./airline/out.txt little


Instrument program for SymbiosisRuntime

$ cd /home/symbiosis/work/symbiosisJava/

$ ./instrument.sh airline.airline    //soot is not working correctly in the VM!


Run instrumented version and generate trace with thread execution paths

$ ./runtime.sh airline.airline out.txt little       //this will create a file name airline.airline.traceBB.fail in folder /SymbiosisRuntime/traces


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ ./symbiosisse.sh airline.airline


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/airline --model=$PWD/tmp/modelAirline.txt --solution=$PWD/tmp/failAirline.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosisJava/Tests/airline


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/airline --model=$PWD/tmp/modelAirline.txt --solution=$PWD/tmp/failAirline.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosisJava/Tests/airline --fix-mode


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failAirline_Alt0.gv -o dsp_failAirline_Alt0.ps



#BANK

Run non-instrumented version

$ cd /home/symbiosis/work/symbiosisJava/Tests/

$ java bank.Bank


Instrument program for SymbiosisRuntime

$ cd /home/symbiosis/work/symbiosisJava/

$ ./instrument.sh bank.Bank


Run instrumented version and generate trace with thread execution paths

$ ./runtime.sh bank.Bank     


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ ./symbiosisse.sh bank.Bank


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/bank --model=$PWD/tmp/modelBank.txt --solution=$PWD/tmp/failBank.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/bank


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/bank --fail-thread=0 --model=$PWD/tmp/modelBank.txt --solution=$(pwd)/tmp/failBank.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/bank --fix-mode


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failBank_Alt0.gv -o dsp_failBank_Alt0.ps



#TWOSTAGE

Run non-instrumented version

$ cd /home/symbiosis/work/symbiosisJava/Tests/

$ java twostage.Main 2 1


Instrument program for SymbiosisRuntime

$ cd /home/symbiosis/work/symbiosisJava/

$ ./instrument.sh twostage.Main


Run instrumented version and generate trace with thread execution paths

$ ./runtime.sh twostage.Main 2 1      


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ ./symbiosisse.sh twostage.Main


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/twostage --model=$(pwd)/tmp/modelTwostage.txt --solution=$(pwd)/tmp/failTwostage.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/twostage


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/twostage --fail-thread=3 --model=$(pwd)/tmp/modelTwostage.txt --solution=$(pwd)/tmp/failTwostage.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --fix-mode --source=/home/symbiosis/work/symbiosis/Tests/twostage


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failTwostage_Alt0.gv -o dsp_failTwostage_Alt0.ps



#CACHE4J

Run non-instrumented version

$ cd /home/symbiosis/work/symbiosisJava/Tests/cache4j

$ java -ea -cp ./bin/:. net.sf.cache4j.test.Cache4jBugDriver


Instrument program for SymbiosisRuntime

$ cd /home/symbiosis/work/symbiosisJava/

$ ./instrument.sh net.sf.cache4j.test.Cache4jBugDriver


Run instrumented version and generate trace with thread execution paths

$ ./runtime.sh net.sf.cache4j.test.Cache4jBugDriver


Run Symbiosis Symbolic Execution engine (SymbiosisSE) to produce per thread symbolic trace files

$ ./symbiosisse.sh net.sf.cache4j.test.Cache4jBugDriver


Run Symbiosis Solver to find the failing schedule

$ cd /home/symbiosis/work/symbiosis/SymbiosisSolver

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/cache4j --model=$(pwd)/tmp/modelCache4j.txt --solution=$(pwd)/tmp/failCache4j.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --source=/home/symbiosis/work/symbiosis/Tests/cache4j


Run Symbiosis Solver to find the alternate, non-failing schedule

$ ./symbiosisSolver --trace-folder=/home/symbiosis/work/symbiosisJava/jpf-symbiosis/traces/cache4j --model=$(pwd)/tmp/modelCache4j.txt --solution=$(pwd)/tmp/failCache4j.txt --with-solver=/home/symbiosis/work/z3-4.3.2/bin/z3 --fix-mode --source=/home/symbiosis/work/symbiosis/Tests/cache4j


If the solver finds a valid alternate schedule, it will output a graphviz file containing the Differential Schedule Projection (extension .gv) in folder SymbiosisSolver/tmp/DSP.  To

produce a .ps version of the DSP:

$ cd ./tmp/DSP

$ dot -Tps dsp_failCache4j_Alt0.gv -o dsp_failCache4j_Alt0.ps