Abstract
We describe the design and implementation of P, an asynchronous event-driven programming language. 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 validated using systematic testing. P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. P is now also being used for the design and implementation of robotics and distributed systems inside Microsoft and in academia.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., Zufferey, D.: P: safe asynchronous event-driven programming. In: Programming Language Design and Implementation (PLDI), pp. 321–332 (2013)
Desai, A., Qadeer, S., Seshia, S.A.: Systematic testing of asynchronous reactive systems. In: Foundations of Software Engineering (FSE), pp. 73–83 (2015)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc, Boston (2002)
Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)
Deligiannis, P., Donaldson, A.F., Ketema, J., Lal, A., Thomson, P.: Asynchronous programming, analysis and testing with state machines. ACM SIGPLAN Not. 50, 154–164 (2015). ACM
Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: DRONA: a framework for safe distributed mobile robotics. In: Proceedings of the 8th International Conference on Cyber-Physical Systems, ICCPS 2017, New York, NY, USA, pp. 239–248. ACM (2017)
Desai, A., Dreossi, T., Seshia, S.: Combining model checking and runtime verification for safe robotics. In: International Conference on Runtime Verification (RV) (2017)
Gray, J., Lamport, L.: Consensus on transaction commit. ACM Trans. Database Syst. 31, 133–160 (2006)
Lamport, L.: Paxos made simple. ACM SIGACT News 32 (2001)
van Renesse, R., Schneider, F.B.: Chain replication for supporting high throughput and availability. In: Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation, OSDI 2004, vol. 6, p. 7. USENIX Association, San Francisco (2004). http://dl.acm.org/citation.cfm?id=1251254.1251261
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Desai, A., Qadeer, S. (2017). P: Modular and Safe Asynchronous Programming. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-67531-2_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67530-5
Online ISBN: 978-3-319-67531-2
eBook Packages: Computer ScienceComputer Science (R0)