P# is a framework that provides the capability of creating asynchronous state-machines, sending events from one machine to another, and writing assertions about system properties (both safety and liveness).
During testing, the built-in P# testing engine captures and controls all (implicit as well as specified) nondeterminism in the system, thoroughly explores the actual executable code to discover bugs, and reports fully-reproducible bug traces. A P# bug trace provides a global order of all events and transitions, and thus is easier to debug.
First, build P# from source, following the instructions here, or install our latest NuGet package.
Next, learn about the different ways of using P# here, and how to write your first P# program here.
Now you are ready to dive into various features and topics:
- Machine termination
- Specifying models and safety/liveness properties
- Using async/await in a machine
- Sharing objects across machines
- Synchronous execution of machines
- Using timers in P#
- Logging and tracking operation groups
Learn how to use the P# testing infrastructure to write unit-tests, thoroughly check safety and liveness properties, and deterministically reproduce bugs:
- Unit-testing P# machines in isolation
- Automatically testing P# programs end-to-end and reproducing bugs
- Effectively checking liveness properties
- Testing async/await code using P#
- Code and activity coverage
- Semantics of uncaught exceptions
The following provides information regarding the available tools in the P# ecosystem:
We provide support for editing the P# language syntax in Visual Studio:
We provide a collection of samples that show how to use the P# framework to build and systematically test asynchronous, event-driven applications. The P# samples are available in the Git repository, under the Samples directory. You can read more here.
We have also used P# to test applications on top of Azure Service Fabric and Orleans:
List of publications on P#:
- Lasso Detection using Partial-State Caching. Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal, Shaz Qadeer . In Formal Methods in Computer-Aided Design (FMCAD), 2017.
- Uncovering Bugs in Distributed Storage Systems During Testing (not in Production!). Pantazis Deligiannis, Matt McCutchen, Paul Thomson, Shuo Chen, Alastair F. Donaldson, John Erickson, Cheng Huang, Akash Lal, Rashmi Mudduluru, Shaz Qadeer and Wolfram Schulte. In the 14th USENIX Conference on File and Storage Technologies (FAST), 2016.
- Asynchronous Programming, Analysis and Testing with State Machines. Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal and Paul Thomson. In the 36th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2015.
To start contributing to P#, read our contribution guidelines.
If you are interested in using P# in your project, or have any P# related questions, please send us an email or open a new issue.