---
_id: '2301'
abstract:
- lang: eng
  text: We describe the design and implementation of P, a domain-specific language
    to write asynchronous event driven code. P allows the programmer to specify the
    system as a collection of interacting state machines, which communicate with each
    other using events. P unifies modeling and programming into one activity for the
    programmer. Not only can a P program be compiled into executable code, but it
    can also be tested using model checking techniques. P allows the programmer to
    specify the environment, used to "close" the system during testing,
    as nondeterministic ghost machines. Ghost machines are erased during compilation
    to executable code; a type system ensures that the erasure is semantics preserving.
    The P language is designed so that a P program can be checked for responsiveness-the
    ability to handle every event in a timely manner. By default, a machine needs
    to handle every event that arrives in every state. But handling every event in
    every state is impractical. The language provides a notion of deferred events
    where the programmer can annotate when she wants to delay processing an event.
    The default safety checker looks for presence of unhan-dled events. The language
    also provides default liveness checks that an event cannot be potentially deferred
    forever. P was used to implement and verify the core of the USB device driver
    stack that ships with Microsoft Windows 8. The resulting driver is more reliable
    and performs better than its prior incarnation (which did not use P); we have
    more confidence in the robustness of its design due to the language abstractions
    and verification provided by P.
author:
- first_name: Ankush
  full_name: Desai, Ankush
  last_name: Desai
- first_name: Vivek
  full_name: Gupta, Vivek
  last_name: Gupta
- first_name: Ethan
  full_name: Jackson, Ethan
  last_name: Jackson
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. P: Safe asynchronous
    event-driven programming. In: <i>Proceedings of the 34th ACM SIGPLAN Conference
    on Programming Language Design and Implementation</i>. ACM; 2013:321-331. doi:<a
    href="https://doi.org/10.1145/2491956.2462184">10.1145/2491956.2462184</a>'
  apa: 'Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., &#38; Zufferey,
    D. (2013). P: Safe asynchronous event-driven programming. In <i>Proceedings of
    the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>
    (pp. 321–331). Seattle, WA, United States: ACM. <a href="https://doi.org/10.1145/2491956.2462184">https://doi.org/10.1145/2491956.2462184</a>'
  chicago: 'Desai, Ankush, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani,
    and Damien Zufferey. “P: Safe Asynchronous Event-Driven Programming.” In <i>Proceedings
    of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>,
    321–31. ACM, 2013. <a href="https://doi.org/10.1145/2491956.2462184">https://doi.org/10.1145/2491956.2462184</a>.'
  ieee: 'A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, and D. Zufferey,
    “P: Safe asynchronous event-driven programming,” in <i>Proceedings of the 34th
    ACM SIGPLAN Conference on Programming Language Design and Implementation</i>,
    Seattle, WA, United States, 2013, pp. 321–331.'
  ista: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. 2013. P: Safe
    asynchronous event-driven programming. Proceedings of the 34th ACM SIGPLAN Conference
    on Programming Language Design and Implementation. PLDI: Programming Languages
    Design and Implementation, 321–331.'
  mla: 'Desai, Ankush, et al. “P: Safe Asynchronous Event-Driven Programming.” <i>Proceedings
    of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>,
    ACM, 2013, pp. 321–31, doi:<a href="https://doi.org/10.1145/2491956.2462184">10.1145/2491956.2462184</a>.'
  short: A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:,
    Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design
    and Implementation, ACM, 2013, pp. 321–331.
conference:
  end_date: 2013-06-19
  location: Seattle, WA, United States
  name: 'PLDI: Programming Languages Design and Implementation'
  start_date: 2013-06-16
date_created: 2018-12-11T11:56:52Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2491956.2462184
ec_funded: 1
fulldoi: https://doi.org/10.1145/2491956.2462184
language:
- iso: eng
main_file_link:
- url: http://research.microsoft.com/pubs/191069/pldi212_desai.pdf
month: '06'
oa_version: None
page: 321 - 331
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language
  Design and Implementation
publication_status: published
publisher: ACM
publist_id: '4626'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'P: Safe asynchronous event-driven programming'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...