Skip to content
This repository was archived by the owner on Aug 26, 2022. It is now read-only.
/ PSharp Public archive

A framework for rapid development of reliable asynchronous software.

License

Notifications You must be signed in to change notification settings

p-org/PSharp

Folders and files

NameName
Last commit message
Last commit date

Latest commit

a31c747 · Jun 15, 2020
Dec 11, 2019
Dec 11, 2019
Dec 11, 2019
Oct 30, 2019
Dec 11, 2019
Dec 11, 2019
Dec 11, 2019
May 26, 2016
Oct 30, 2019
Oct 30, 2019
Jun 20, 2017
Apr 26, 2019
Jun 15, 2020
Apr 23, 2020

Repository files navigation

News: P# has evolved into Coyote. This repository is now deprecated and development has moved here. Check it out!


P# is a framework for rapid development of reliable asynchronous software. The P# project, which started as a collaboration between Microsoft Research and Imperial College London, is used by several teams in Azure to design, implement and automatically test production distributed systems and services.

Features

The P# framework provides:

  • An actor-based programming model for building event-driven asynchronous applications. The unit of concurrency in P# is an asynchronous communicating state-machine, which is basically an actor that can create new machines, send and receive events, and transition to different states. Using P# machines, you can express your design and code at a higher level that is a natural fit for many cloud services.
  • An efficient, lightweight runtime that is build on top of the Task Parallel Library (TPL). This runtime can be used to deploy a P# program in production. The P# runtime is very flexible and can work with any communication and storage layer.
  • The capability to easily write safety and liveness specifications (similar to TLA+) programmatically in C#.
  • A systematic testing engine that can control the P# program schedule, as well as all declared sources of nondeterminism (e.g. failures and timeouts), and systematically explore the actual executable code to discover bugs (e.g. crashes or specification violations). If a bug is found, the P# testing engine will report a deterministic reproducible trace that can be replayed using the Visual Studio Debugger.

Getting started

Read the P# programming guide and then read about various features and topics here.

How to build

Follow the instructions to build P# from source, or just install our latest P# NuGet package.

How to contribute

We welcome contributions! However, before you start contributing, please read carefully the development guidelines.

Contact us

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.