P Tutorials @ SOSP 23

Formal Methods, should I attend this tutorials?

Formal methods are rigorous techniques for specification, analysis, and verification of software systems. Formal methods complement the existing testing approaches to validate correctness of complex system. The general perception is that formal methods is hard to apply in practice, has steep learning curve, fails to scale for real-world distributed systems. The purpose of this tutorial is to introduce tools and techniques that help make formal methods easy to apply to distributed systems. Please attend the tutorial to learn about formal methods and how engineers at Amazon Web Services (AWS) leverage them in practice.

Abstract

Large scale distributed systems are difficult to design and test. Hence, it is not uncommon for design bugs to escape guard rails of design reviews, pass functional and stress testing, and get uncovered when serving customers in production. Formal methods can play an important role in addressing these challenges and help catch these bugs early on in the development process. In this tutorial, we present formal methods tools and techniques used at Amazon Web Services (AWS) to reason about the correctness of distributed systems. We will provide an introduction to the P framework and also share our experience of integrating P in all phases of the development process from design to testing to deployment in production. One goal of this tutorial is to ignite a discussion between the formal methods and systems communities on the challenges faced by practitioners in industry when building complex distributed systems.

P Framework

This tutorial covers the P framework and its associated tools. P is a state machine based programming language for formally modeling and specifying complex distributed systems. P allows programmers to model their system design as a collection of communicating state machines. P supports several backend analysis engines (based on formal techniques like model checking and symbolic execution) to check that the distributed system modeled in P satisfies the desired correctness specification. P leverages runtime monitoring to connect design level specifications to system implementations.

State machine based programming language.
P allows programmers to specify their system design as a collection of communicating state machines, which is how they normally think about complex system design. P being a programming language (rather than a mathematical modeling language) has been one of the key reasons for its large-scale adoption in industry.
Scalable Model Checking.
P provides a scalable model checker to check that the distributed system modeled in P satisfies the desired correctness specification. P leverages distributed compute clusters to scale its analysis to a large system design. It has helped find critical bugs inside AWS early on in the design phase.
Code conformance checking
To bridge the gap between design specifications and the actual implementation, P leverages runtime monitoring to check that system traces satisfy the P specification checked during the design phase.

Performance simulations
P also supports a backend explorer that performs random probabilistic simulations of the system for reasoning about performance quantitatively.
Integration into CI/CD
P provides the capability to integrate formal analysis engines and code conformance checks into the build pipelines of the service teams.

Usage of P inside AWS

Teams across AWS from storage (e.g., S3, EBS), to databases (e.g., Aurora, DynamoDB), to compute (e.g., EC2) have been using P to reason about the correctness of the innovative distributed protocols utilized by these services. P has helped find and eliminate several critical design bugs that could not be found using the traditional testing approaches. From our experience (4+ years) of using P inside AWS, we have observed that P has helped developers in several different ways, from acting as a thinking tool, to an effective bug finder for complex designs, and finally, boosting the overall velocity of service teams in delivering reliable systems. We will share some of our experiences in this tutorial.

Tutorial Overview

Details of the tutorial examples along with videos for each chapter of the tutorials coming soon.... It is going to be a fun tutorial with introduction to light-weight formal methods. You can find the details of the tutorials here.

Contacts

Ankush Desai

Senior Applied Scientist, Database Systems Lab @ AWS

P Team

Database Systems Lab @ AWS

Formal Modeling and Analysis of Distributed Systems

Formal Methods, should I attend this tutorials?

Abstract

P Framework

P on Github

Publications

Videos and Talks

Usage of P inside AWS

Tutorial Overview

Contacts