During the development of Windows 8, the USB team at Microsoft took a bold step while shipping USB 3.0 in Windows 8.1 and in Windows phone and decided to unify modeling and programming. Various components of the USB driver stack were specified as state machines and asynchronous driver code was auto-generated from these state machines. They were able to use model checking techniques directly on the state machines to find and fix design bugs. Since the executable code was auto-generated from the source, they could make changes at the level of state machines and perform both verification and compilation from one description. This methodology was used to design, validate and generate code for the USB stack that ships with Windows 8. The resulting driver stack is not only more reliable, but also more performant and presents the salient aspects of this methodology as a domain specific language P.
What is P programming language?
P is a programming language for modeling and specifying protocols in asynchronous event-driven applications. It is designed to address the challenges of asynchronous computation such as asynchrony and Heisenbugs.
How does it work?
The P programmer writes the protocol and its specification at a high-level. A P program is a collection of machines. Machines communicate with each other asynchronously through events. Events are queued, but machines are required to handle them in a responsive manner. The P compiler provides automated testing and executable code for running the protocol. P provides first-class support for modeling concurrency, specifying safety 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.
Extensions to P Language
P is transforming the development of cloud infrastructure in Azure. Azure is similar to other cloud providers which faces the challenge of Heisenbugs caused by unexpected race conditions and software or hardware faults. These bugs result in disruption of live services which is a huge problem for both customers and providers of cloud services. P is being used to find and debug Heisenbugs in already-deployed services and to design and validate new services before deployment. P allows engineers to precisely model asynchronous interfaces among components in a large Azure service. It also allows engineers to discover and debug problems on their desktops that would otherwise take months and sometimes even years to manifest after the service is deployed.
Important Features
An important feature of P that makes it particularly suitable for validating fault-tolerant distributed services is the ability to perform thorough failover testing that is, validating that the service recovers and resumes operation when an unexpected fault happens. Both network message drops and individual state machine failures are modeled as events. Modeling a fault as an event in P fully automates fault-injection and enables systematic testing of failover under a huge number of event orderings and faults with little effort from the programmer.
Limitations:
Its capabilities are limited with respect to handling explicit data input, especially when that input is over large domains which makes it difficult to apply P to applications such as robotics where a significant source of complexity is decision-making under uncertain input. Dealing with large and uncertain input domains is an ongoing research investigation.
Image Reference: www.microsoft.com
Important links:
- Download P
- Safe asynchronous programming with P
