Performal: Formal Verification of Latency Properties for Distributed Systems
Understanding and debugging the performance of distributed systems is a notoriously hard task, but a critical one. Traditional techniques like logging, tracing, and benchmarking represent a best-effort way to find performance bugs, but they either require a full deployment to be effective or can only find bugs after they manifest. Even with such techniques in place, real deployments often exhibit performance bugs that cause unwanted behavior.
In this paper, we present Performal, a novel methodology that leverages the recent advances in formal verification to provide rigorous latency guarantees for real, complex distributed systems. The task is not an easy one: it requires carefully decoupling the formal proofs from the execution environment, formally defining latency properties, and proving them on real, distributed implementations. We used Performal to prove rigorous upper bounds for the latency of three applications: a distributed lock, ZooKeeper and a MultiPaxos-based State Machine Replication system. Our experimental evaluation shows that these bounds are a good proxy for the behavior of the deployed system and can be used to identify performance bugs in real-world systems.
Mon 19 JunDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | PLDI: Concurrency & ParallelismPLDI Research Papers at Cypress 2 Chair(s): Calin Cascaval Google Research | ||
16:00 20mTalk | Type-Checking CRDT Convergence PLDI Research Papers George Zakhour University of St.Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen DOI Pre-print | ||
16:20 20mTalk | Reliable Actors with Retry Orchestration PLDI Research Papers Olivier Tardieu IBM Research, David Grove IBM Research, Gheorghe-Teodor Bercea IBM Research, Paul Castro IBM Research, Jaroslaw Cwiklik IBM Research, Edward Epstein IBM Research DOI | ||
16:40 20mTalk | Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels PLDI Research Papers Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea LIX, CNRS, Ecole Polytechnique, Enrique Román-Calvo Université Paris Cité - CNRS - IRIF DOI | ||
17:00 20mTalk | Responsive Parallelism with Synchronization PLDI Research Papers Stefan K. Muller Illinois Institute of Technology, Kyle Singer Washington University in St. Louis, USA, Devyn Terra Keeney Illinois Institute of Technology, Andrew Neth Illinois Institute of Technology, Kunal Agrawal Washington University in St. Louis, USA, I-Ting Angelina Lee Washington University in St. Louis, USA, Umut A. Acar Carnegie Mellon University DOI | ||
17:20 20mTalk | Parallelism in a Region Inference Context PLDI Research Papers DOI | ||
17:40 20mTalk | Performal: Formal Verification of Latency Properties for Distributed Systems PLDI Research Papers Nuda Zhang University of Michigan, Upamanyu Sharma Massachusetts Institute of Technology, Manos Kapritsos University of Michigan, USA DOI |