Safe Asynchronous Programming with P and P#

Established: March 15, 2016



We are designing programming languages for building safe and reliable asynchronous systems. The languages are based on the programming idiom of communicating state machines. They offer first-class support for writing safety and liveness specifications as well as building abstract models of code. They offer systematic testing capabilities that exhaustively (in the limit) tests all possible executions of the program, weeding out even 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# provides P-style modeling and specification techniques not as a separate language but as an extension to C#, a language that is already familiar to many programmers. 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.


External collaborators

  • Ankush Desai (U. Berkeley)