BT

Your opinion matters! Please fill in the InfoQ Survey!

Microsoft Open-Sources P Language for Safe Async Event-Driven Programming

| by Sergio De Simone Follow 6 Followers on Oct 12, 2016. Estimated reading time: 1 minute |

A note to our readers: As per your request we have developed a set of features that allow you to reduce the noise, while not losing sight of anything that is important. Get email and web notifications by choosing the topics you are interested in.

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.

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

actor model by Ezequiel Gioia

Same concepts than the actor model?

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

1 Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT