# Static analysis benchmarks and experiments

We provide the prebuilt executable for the P# static analyser. We also provide the source code for the benchmarks that are
evaluated in Table 1 of the paper. We also provide instructions and a script for running the experiments. The script invokes
the prebuilt P# static analyser (in the Binaries dir).

Note: running all the experiments from the script should take approximately 25-30 mins.
Note: please do not attempt to build the benchmarks solution; the P# static analyser works directly on the source code.

## Contents

* Binaries
  This dir contains a prebuilt version of the P# static analyser (PSharpStaticAnalyser.exe).

* Output
  This dir is used for dumping the output from the experiments. There is a tex file that can be compiled
  with the output to produce an easy-to-read Table 1.

* PSharpBench
  This dir contains the non-racy PSharpBench suite (BasicPaxos, BoundedAsync, ChainReplication, Chord, German, MultiPaxos,
  Raft and TwoPhaseCommit). Each of the benchmarks has its own directory and corresponding project file.

* PSharpBenchRacy
  This dir contains the racy PSharpBench suite (same 8 benchmarks as above). Each of the benchmarks has its own directory
  and corresponding project file.

* SOTER
  This dir contains the 4 SOTER benchmarks that we ported to P# (Chameneos, Leader, Pi and Swordfish). Each of the benchmarks
  has its own directory and corresponding project file.

* RegressionSuite
  This dir contains a regression suite used to test various racy and non-racy test cases (reports 91 found errors).

## Claims

Claim 1: Our static analysis is more precise than previous work (SOTER).
Claim 2: Our static analysis scales well with respect to our benchmark sets.

Below we provide instructions on how to reproduce the results that substantiate these claims.

## Reproducing results

1. Open Windows PowerShell (you might have to open it in administrator mode).
2. cd to this directory (\pldi15_artifact\3-static-analysis\)
3. Run the command:

```
python RunExperiments.py
```

This will run the following 8 experiments using the prebuilt P# static analyser:

- Analyse non-racy PSharpBench benchmarks without xSA
- Analyse non-racy PSharpBench benchmarks with xSA
- Time non-racy PSharpBench benchmarks (10 iterations)
- Analyse racy PSharpBench benchmarks
- Time racy PSharpBench benchmarks (10 iterations)
- Analyse SOTER benchmarks without xSA
- Analyse SOTER benchmarks with xSA
- Time SOTER benchmarks (10 iterations)

Note: We do not include the AsyncSystem in this artifact, as it is proprietary software.

The script will report any data races found in the benchmarks as output to the terminal. When the script terminates,
it will dump the results in the following LaTeX file in the Output directory:

\pldi15_artifact\3-static-analysis\Output\analysis_table.tex

Optional: open the Output dir and compile the results.tex file using pdflatex, for an easy-to-read version.

Claim 1: The P# static analyser does not report any false data races in the 4 SOTER benchmarks. In the SOTER paper
  they reported multiple false positives for these 4 benchmarks.
Claim 2: The P# static analyser performs similarly well in all our benchmarks, regardless of benchmark size.
  This is because our analysis is both machine and procedure modular.

Note: this script does not produce values for the LoC, #M, #ST and #AB columns of Table 1, as these are only simple
  program statistics, unrelated to the static analysis experiment.
Note: there is a rare issue that the python script seems to get stuck, this is typically fixed by pressing "enter"
  in the PowerShell terminal, else just "ctrl + c" and retry.

## Running the P# static analyser directly

cd to the Binaries dir and run:

```
.\PSharpStaticAnalyser.exe /s:{PROJECT_PATH}\{SOLUTION_NAME}.sln /p:{PROJECT_NAME}
```

Where PROJECT_PATH is the path to the project you want to analyse; SOLUTION_NAME is the name of the solution; and
PROJECT_NAME is the name of the individual project (inside the solution).

For example, you can use this command to run the regression suite:

```
.\PSharpStaticAnalyser.exe /s:..\StaticAnalysisBenchmarks.sln /p:RacyRegressionSuite
```

Note: the analyser uses xSA by default; if you want to disable it, please use the option /noStateTransitionAnalysis
Note: if you want to print timing information, please use the option /time
