Microsoft’s recently open-sourced P language aims to make it possible to write safe asynchronous event-driven programs on Linux, macOS, and Windows.
Microsoft describes P as a domain-specific language to model communication between components of an asynchronous system, such as an embedded, networked, or distributed system. A P program is defined in terms of finite state machines than run concurrently. Each of them has an input queue, states, transitions, a machine-local store, and can send asynchronous messages to the others. A basic operation in P either updates a local store, sends a message, or creates new machines. The following partial code snippet shows how you can describe a state and its transitions in P. Additionally, it shows how you send a message or create a new machine:
...
start state Init {
entry {
server = new Server();
raise SUCCESS;
} on SUCCESS goto SendPing;
state SendPing {
entry {
send server, PING, this;
raise SUCCESS;
}
on SUCCESS goto WaitPong;
}
...
According to Microsoft, P programs can be verified using model checking. This allows developers to ensure that a system is able to handle every event in a timely manner. For a P program to be responsive, its state machines must handle all event that can be dequeued in every state. Since this is not always practical, it is possible to defer the handling of some events. In such case, the language ensures that an event cannot be potentially deferred forever. To be able to verify the properties of a program, besides generating C code which can be then fed to a C compiler for execution, the P compiler will output a Zing model that can be used for systematic testing. Zing is an open source model checker for concurrent programs that is able to systematically explore all possible states of a model.
Microsoft used the P language to implement and verify the core of the Windows 8 USB device driver stack. According to Microsoft, the use of P helped their engineers to serialize large numbers of uncoordinated events coming in from hardware, operating system, function drivers and other driver components with improved reliability and performance. Specifically, they maintain, the number in the new USB hub driver due to invalid memory accesses and race conditions is insignificant, while enumeration times are 30% faster and no cases of worker item starvation were observed.
