Programming Devices and Services with P
May 11, 2016 at 3:30pm
P is a programming framework for design, implementation, and validation of event-driven asynchronous systems. The P language incorporates deep modeling and specification techniques into asynchronous programming. It allows the programmer to systematically test and debug their applications before deployment, thus preventing Heisenbugs that are extremely difficult to find and fix later.
P is used in Microsoft products. The USB drivers shipped by Microsoft (Windows 8.1 onwards) have been written in P; these drivers run on hundreds of millions of devices. The design of P has also been implemented independently by engineers in Microsoft Office and Azure for components being written by their team. In Microsoft Azure, there are ongoing projects that are using P to implement services. Finally, researchers at Microsoft and UC Berkeley are exploiting P to build a reliable software stack for autonomous robots.
My talk will provide an overview of the key ideas behind P and conclude with a discussion of open research problems.
Shaz Qadeer is a Principal Researcher at Microsoft. His research interest lie at the intersection of (in)formal methods, program verification, programming languages, and software engineering. Currently, he spends most of his time on P and P#, available open-source at https://github.com/p-org.