# Asynchronous Programming, Analysis and Testing with State Machines: Additional Supporting Materials

This is the artifact that accompanies our PLDI 2015 paper.

We provide four main items:

1. Prebuilt executables and the source code of the P# toolchain.
2. Tutorial on writing a simple "Hello, World!" example in P# (and source code of the example).
3. Prebuilt executables and the source code for our benchmarks.
4. Scripts for running the experiments and reproducing the results in the paper.

Note: we do not include AsyncSystem as it is proprietary software.
Note: we do not include the CHESS experiments, as they require many complex external dependencies; but we provide precompiled
  DLLs that someone could use to run with CHESS.

## Prerequisites

* Windows 8.1 or Windows 7

* Visual Studio 2015 Preview, which is available at http://www.visualstudio.com/en-us/downloads/visual-studio-2015-downloads-vs.aspx
  - Required as P# depends on and uses the latest Roslyn code analysis APIs. Please let us know if you have any difficulties.
  - When installing VS 2015, only "Core" is required. The other options can be skipped.

* Python 2.7.5
  - Required for running our experiments-related scripts.

* LaTeX (optional)
  - For compiling the experiment outputs into an easy-to-read pdf file.
  - You can use your favorite pdflatex installation.

* CHESS (optional)
  - For running the CHESS-related systematic testing experiments.
  - https://chesstool.codeplex.com

## Contents

Each directory contains a corresponding README file with further instructions.

* 0-paper-and-data
  This directory contains the draft paper and the data used for generating Table 1 and Table 2 from the evaluation section. These
  are given for convenience, so someone can easily compare with the generated results from running the artifact experiments.

* 1-psharp
  Source code for the P# runtime (which includes the systematic testing schedulers) and P# static analyser, together with build
  instructions. This directory also provides details (in the README file) as to where in the source code the various ideas and
  features, described in the paper, are implemented. Building from scratch is completely optional, as the directories with the
  experiments ("3-static-analysis" and "4-systematic-testing") contain prebuilt versions of the toolchain.

* 2-psharp-example
  This directory contains the source code of a "Hello, world!" program in P#. We also give a tutorial (in the README file) on
  how to create this simple P# program.

* 3-static-analysis
  This directory contains the prebuilt executable of the P# static analyser. It also contains the source code of the benchmarks
  that are evaluated in Table 1 of the paper. There are 3 benchmark categories: non-racy P# benchmarks; racy versions of the same
  P#benchmarks; and the SOTER benchmarks ported to P#. We also include a regression suite. Finally, the directory contains scripts
  for running the experiments.

* 4-systematic-testing
  This directory contains prebuilt executables to run 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 we do not support in this artifact). Finally, the directory contains instructions and scripts for
  running the experiments.

## License

We do not have an official license for the P# language yet, and submission of this artifact does not contain tacit permission to
make any of its contents public. By accepting to evaluate this artifact you agree to not publicise any part of the artifact, nor
retain it for further purposes, during or after the completion of the evaluation.
