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.
The P language has been used extensively in developing device drivers for Windows, and P# is currently being used by several teams in Azure for developing microservices. We are also working on a distributed runtime with fault-tolerance guarantees, as well as extensions to serverless compute.
- Ankush Desai (U. Berkeley)