# P# systematic testing benchmarks and experiments

We provide prebuilt executables for running the systematic testing benchmarks from Table 2 of the paper. There are three benchmark
categories: benchmarks compiled in bug-finding mode using the P# random scheduler; benchmarks compiled in bug-finding mode using
the P# DFS scheduler; and benchmarks compiled so they can be used with CHESS out-of-the-box (this requires CHESS, which is not
supported in this artifact).

We provide instructions and an automated way to run the P#-related benchmark categories for 10,000 iterations or a 5 max mins limit
(whichever hits first).

Note: running the P# Random experiments should take approximately 60 mins.
Note: running the P# DFS experiments should take approximately 30 mins.

## Contents

* psharp-random
  This dir contains prebuilt versions of the buggy PSharpBench suite (BasicPaxos, BoundedAsync, ChainReplication,
  Chord, German, MultiPaxos, Raft and TwoPhaseCommit). The benchmarks were compiled in bug-finding mode using the
  P# random scheduler.

* psharp-dfs
  This dir contains prebuilt versions of the buggy PSharpBench suite (BasicPaxos, BoundedAsync, ChainReplication,
  Chord, German, MultiPaxos, Raft and TwoPhaseCommit). The benchmarks were compiled in bug-finding mode using the
  P# DFS scheduler.

* chess
  This dir contains prebuilt dlls for the buggy PSharpBench suite (BasicPaxos, BoundedAsync, ChainReplication,
  Chord, German, MultiPaxos, Raft and TwoPhaseCommit). The benchmarks were compiled with all dependencies required
  to run out-of-the-box using CHESS (this requires CHESS, which is not supported in this artifact).

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

## Claims

Claim 1: The P# random scheduler is efficient in finding bugs.
Claim 2: The two P# integrated schedulers are faster than CHESS (requires CHESS, which is not included in the artifact).

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

## Reproducing results for the two P#-schedulers

P# Random:

1. Open Windows PowerShell (you might have to open it in administrator mode).
2. cd to the directory "\pldi15_artifact\4-systematic-testing\psharp-random\"
3. Run the command:

```
.\RunBenchmarks.exe > out.txt
```

This will systematically test one by one the benchmarks for 10,000 iterations using the P# random scheduler and
output the results in a "results-XXXX-X-X--XX-XX-XX" file.

P# DFS:

1. Open Windows PowerShell (you might have to open it in administrator mode).
2. cd to the directory "\pldi15_artifact\4-systematic-testing\psharp-dfs\"
3. Run the command:

```
.\RunBenchmarks.exe > out.txt
```

This will systematically test one by one the benchmarks for 10,000 iterations using the P# DFS scheduler and
output the results in a "results-XXXX-X-X--XX-XX-XX" file.

After you run both of the above experiments, you can compile the results into an easy-to-read table:

1. cd to the directory "\pldi15_artifact\4-systematic-testing\"
2. Run the command:

```
python AggregateResults.py
```

The results are dumped in \pldi15_artifact\3-systematic-testing\Output\testing_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# random scheduler finds the bug in every benchmark. On the other hand, the P# DFS scheduler finds a bug in
  only 3 of our benchmarks.
Claim 2: The P# schedulers are more effective in findings bugs than CHESS. This is because (1) we do not need to perform
  dynamic data race detection (we have race freedom guarantees provided by the P# static analyser); and (2) the P#
  schedulers have domain knowledge about the P# framework, whereas CHESS does not have this domain knowledge and thus needs
  to analyse more scheduling points.

Note: the "Buggy %"" results might slightly vary due to the P# random scheduler and non-determinism in the machines
  that model the environment in some of the benchmarks.
Note: the "sch/sec" results can vary depending on the machine that runs the experiments; a similar trend can be observed
  though with the results we reported in the paper.
Note: please do not try to run the benchmark executables on their own; they have been compiled in a specific way so they
  can be used with our automatic benchmark execution infrastructure.

## Running CHESS (optional and not supported)

Although we do not officially support CHESS in this artifact, we give the command line options that we used to run CHESS
on each of our benchmarks. E.g. for the buggy Chord benchmark:

1. With data race detection ON:

```
mchess /dr /met:0 /mct:500 /me:10000 MChordBuggy.dll
```

2. With data race detection OFF:

```
mchess /met:0 /mct:500 /me:10000 MChordBuggy.dll
```

Note: you might get a deadlock reported in some of the benchmarks; these are not considered as bugs in our evaluation.
Note: if an assertion failure is found, then a notification window will pop up; just press "continue", "ignore" or "abort".
