Safe Asynchronous Programming with P and P#

成立时间：April 21, 2014

We are designing programming languages for building safe and reliable asynchronous systems. These languages are based on the programming idiom of asynchronous communicating state machines. They offer first-class support for writing safety and liveness specifications as well as building abstract models of the code. They offer systematic testing capabilities that exhaustively (in the limit) test all possible executions of the program, weeding out hard-to-find concurrency bugs.

P is a (domain-specific) programming language for modeling and specifying protocols in asynchronous event-driven applications. The P programmer writes the protocol and its specification at a high-level. The P compiler provides automated testing for concurrency-related race conditions and executable code for running the protocol. P provides first-class support for modeling concurrency, specifying safety and liveness properties, and checking that the program satisfies its specification using systematic search. A P program can also be compiled into executable C code. This capability bridges the gap between high-level model and low-level implementation and eliminates a huge hurdle to the acceptance of formal modeling and specification among programmers.

P# is a programming framework for building highly reliable asynchronous reactive software (such as distributed systems and microservices) that brings P-like semantics to C#, a general-purpose language that is already familiar to many programmers. In production, P# programs execute on an efficient, lightweight runtime that is build on top of the .NET Task Parallel Library (TPL). P# provides support for writing safety and liveness specifications (similar to TLA+) programmatically in C#. To find bugs (e.g. race conditions, crashes or specification violations), P# has a built-in automated testing engine that can control the schedule of a P# program (as well as all declared sources of nondeterminism, e.g. failures and timeouts), and automatically explore the actual executable code by enumerating execution paths and interleavings. If a bug is found, P# will report a deterministic reproducible trace that can be replayed using the Visual Studio Debugger. In contrast to P, the approach in P# is minimal syntactic extension and maximal use of libraries to deliver modeling, specification, and testing capabilities. P# can be used both to write new services and to test existing services.

P has been used extensively in developing device drivers for Windows, and P# is being used by several teams in Azure for building reliable microservices.

We are also working on a distributed runtime with fault-tolerance guarantees (opens in new tab), as well as extensions to serverless computing.