P is a language for asynchronous event-driven programming. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be systematically tested using Model Checking. P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. P is currently being used extensively inside Amazon (AWS) for model checking complex distributed systems.

Publications

• Compositional Programming and Testing of Dynamic Distributed Systems. Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit Seshia. International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2018.

• DRONA: A Framework for Safe Distributed Mobile Robotics. Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer, and Sanjit A. Seshia. In Proceedings of the 8th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2017.

• Systematic Testing of Asynchronous Reactive Systems. Ankush Desai, Shaz Qadeer, and Sanjit A. Seshia. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2015).

• P: Safe asynchronous event-driven programming. Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2013.

Manual

Check the P Wiki.

Information for building P framework is available here.

Demos

See fun demo video using P to control a quadrocopter and make sense of the MavLink stream, all visualized in a live DGML diagram.

Application to Robotics

We built DRONA, a software framework for distributed mobile robotics systems. DRONA uses P language for implementing and model-checking the distributed robotics software stack (wiki). The C code generated from P compiler can be easily deployed on Robot Operating System (ROS). More details about the DRONA framework and simulation videos are available here: https://drona-org.github.io/Drona/

Blogs

• P: A programming language designed for asynchrony, fault-tolerance and uncertainty by Shaz Qadeer.
• Building robust USB 3.0 support

News

• TechWorld[2016]: Microsoft open-sources P language for IoT
• InfoQ[2016]: Microsoft Open-Sources P Language for Safe Async Event-Driven Programming
• Reddit[2016]: Microsoft opensources P language