Recommend using the same OS in dynamic validation.

—————–IMPLEMENTATION————–

The static analysis component was implemented using the Clang Tool 3.4. The corresponding directory Static-Analysis.

Our guided symbolic execution was implemented based on KLEE 1.2. The directory is Guided-Symbolic-Execution/klee and Guided-Symbolic-Execution/klee-uclibc, compile it using the instruction at http://klee.github.io/build-llvm34/.

We used Simics virtual platforms 4.6 to implement the dynamic validation phase. The directory is Dynamic-Validation.

——————Static Detection————–

klee-gcc is a tool compiling device driver to clang AST, this tool is in directory Static-Analysis/scripts/klee-gcc.

$cd Experiment-and-Subjects/moti-example$

make CC=/path/to/klee-gcc

then compile SRacer

$cd Static-Analysis/SRacer$

mkdir build; cd build; cmake ..

$make After finishing compiling SRacer and device drivers.$

find $(pwd) -name “*.ast” > astList.txt

Note that ast files are generated by klee-gcc.

run the command:

$SRacer /path/to/astList.txt /path/to/config.txt /output/path i.e., SRacer astList.txt config.txt ./ config.txt can be found in Experiment-and-Subjects and Static-Analysis/SRacer A simple warning manager tool provided in directory Experiment-and-Subjects/static-result/ is warningManager.py. ------------------Symbolic Execution-------------- Use klee-gcc-bc to compile kernel module to llvm IR. The LLVM verison is 3.4. Note: instrumentations are required to make KLEE able to execute drivers. First, Experiment-and-Subjects/static-result/autoIns.py is proivided to instrument interupt calls. Second, determine variables as symbolic by using klee_make_symbolic. Third, provided guided files named as GuideSrc.txt, so that the modified KLEE could regonize which path sould cover and which not. The file format is as follows: Info: filename1 linenumber1 filename2 linenumber2 filename3 linenumber3 Very similar with the output file of SRacer (name of static analysis phase).$

cd Experiment-and-Subjects/moti-example

$make CC=/path/to/klee-gcc-bc$

klee -entry-point=dataRace_init -guidedExe -libc=uclibc exampleSym.bc

——————Dynamic Validation————–

Use Simics4.6 to dynamic validate each potentional data race.

Test case configureation:

Open checkpoint “ubuntu-gcc” (we install ubuntu on Simics)

“simics>” means in command line window (Simics GUI -> “tools”->”command line window”)

“$” means in simulated system.

simics> enable-real-time-mode

The following instructions are used to transform subjects:

$ftp 10.10.0.1 Press enter$

bin

$get example.tar.gz$

quit

The following instructions are used to compile drivers:

$tar xf example.tar.gz$

cd general

$make$

sudo insmod example.ko

The following instructions are used to save the status so that we can use it again without redo previous steps:

simics> stop

simics> write-configuration ckp-example

simics> c

The following instructions are used to store symbol file to host:

$cat /proc/kallsyms > exampleSymbol$

ftp 10.10.0.1

Press enter

$put exampleSymbol$

quit

When performing automatic validation (Scripts are in directory Dynamic-Validation/scripts/analysePDR.py):

If Simics is running and you want to test the next case, open “command line window” and input “quit”.

When performing validation one by one:

Scripts are provided in directory Dynamic-Validation/conf.py. It read Dynamic-Validation/Info.py as information file.

The conf.py can be run by entering run-python-scripts in command line window or selecting python file in Simics menu.