Asynchronous Programming, Analysis and Testing with State Machines

This webpage accompanies our PLDI 2015 paper. We publicly provide an artifact for reproducing all the results from our experiments. Our artifact was independently evaluated and accepted by the PLDI 2015 Artifact Evaluation Committee.

P# is a new language for high-reliability asynchronous .NET programming, co-designed with a static data race analysis and testing infrastructure. The co-design aspect of P# allows us to combine language design, analysis and testing in a unique way: the state-machine structure of a P# program enables us to create a more precise and scalable static analysis; while the race-freedom guarantees, provided by our analysis, contribute to the feasibility of systematically exploring a P# program to find bugs (e.g. assertion failures and unhandled exceptions).

PLDI 2015 Artifact Evaluated Badge

Links and Downloads

Artifact Details

Please download our artifact. For instructions, see the README files inside the zip file. Please note that the toolchain and experiments require Visual Studio 2015 Preview to be installed. We have only tested the artifact on Windows 8.1 and Windows 7 installations. Please use one of these versions, as we do not currently support other OS versions.

The artifact includes 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.

The artifact also includes thorough documentation (in README.md files) for each of the above items, and instructions on how to reproduce the experimental results from the paper. You can read the documentation either on your favorite markdown viewer or simply use a text editor.

The focus of the artifact is on writing a simple program in P# and most importantly on reproducing the experimental evaluation of the paper. Towards this, we address the following claims:

  1. Our static analysis is more precise than previous work (SOTER).
  2. Our static analysis scales well with respect to our benchmark sets
  3. The P# random scheduler is efficient in finding bugs.
  4. The two P# integrated schedulers are faster than CHESS.

In the artifact documentation (in README.md files) we include information on how we address each of these claims.

Note: we do not include AsyncSystem as it is proprietary software; we also do not include CHESS, but details on how to obtain CHESS can be found here. Our scripts do not support running automatically the CHESS-related experiments, as they required a lot of manual effort and tricky dependencies, but we provide precompiled DLLs of our benchmarks that someone can use to manually run with CHESS out-of-the-box. All other experiments are automated.