P: Formal Modeling and Analysis of Distributed Systems
Abstract:
Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about correctness in the presence of myriad possible interleaving of messages and failures. Unsurprisingly, it is common for service teams to uncover correctness bugs after deployment. Formal methods (FM) can play an important role in addressing this challenge. But the key requirement for “success” in an industrial setting would be the ability to integrate FM in all the phases of development process from system design, to implementation, to unit and integration testing, and even in production.
In this talk, we will provide an overview of the P programming framework. We will discuss how P is currently being used extensively inside Amazon (AWS) to integrate principles of FM in to the development lifecycle of service teams and deliver complex distributed services with higher assurance of correctness.
P is a state machine-based programming language for modeling and specifying complex distributed systems. Details about the P framework with tutorials and related publications can be found here: https://p-org.github.io/P/.
P is an open-source tool with users and contributors from industry and academia. It would be great to through this talk engage with the industrial and adacemic community.
Ankush Desai is a Senior Applied Scientist in the Database Services (DBS) group at AWS. The goal of Ankush’s work at AWS is to integrate formal methods techniques in all the phases of development process from system design, to implementation, to unit and integration testing, and even in production. These techniques range from lightweight approaches like model checking, to systematic testing, to more rigorous deductive verification that provides mathematical proofs. He is currently exploring how formal tools and techniques can help developers deliver complex distributed database services (DBS) with high assurance of correctness! Before joining the DBS group, Ankush was part of the S3 team and worked on the Amazon S3's Strong Consistency project.
Ankush graduated with a PhD in computer science from UC, Berkeley (2019). His PhD. research had an impact both in Industry and Academia for which he was awarded the Sevin Rosen Funds Award for Innovation. Before joining graduate school, Ankush spent 2+ years working at Microsoft Research, India working on formal verification of device drivers and distributed systems. Webpage: https://ankushdesai.github.io/