P: Safe Asynchronous Event-Driven Programming

P: a domain specific language for writing asynchronous
event-driven programs. This asynchronous
language promotes a discipline of programming
where deferrals need to be declared explicitly, and consequently
leads to responsive systems.

The main technical
contribution of this work is an asynchronous model which forces
each event in the queue to be handled as soon as the machine associated
with the queue is scheduled, and has a chance to de-queue the
event. The system’s verifier systematically explores the state space of machines
and ensures that there are no unhandled events. In certain
circumstances, such as processing a high priority event, or processing
a sequence of event exchanges during a transaction, some other
lower priority events may have to be queued temporarily. P has features
such as deferred events for a programmer to explicitly specify
such deferrals.