Growing a protocol


Kamala Ramasubramanian, Kathryn Dahlgren, Asha Karim, Sanjana Maiya, Sarah Borland, UC Santa Cruz, Boaz Leskes, Elastic; Peter Alvaro, UC Santa Cruz


Verification is often regarded as a one-time procedure undertaken after a protocol is specified but before it is implemented. However, in practice, protocols continually evolve with the addition of new capabilities and performance optimizations. Existing verification tools are ill-suited to “tracking” protocol evolution and programmers are too busy (or too lazy?) to simultaneously co-evolve specifications manually. This means that the correctness guarantees determined at verification time can erode as protocols evolve. Existing software quality techniques such as regression testing and root cause analysis, which naturally support system evolution, are poorly suited to reasoning about fault tolerance properties of a distributed system because these properties require a search of the execution schedule rather than merely replaying inputs. This paper advocates that our community should explore the intersection of testing and verification to better ensure quality for distributed software and presents our experience evolving a data replication protocol at Elastic using a novel bug-finding technology called Lineage Driven Fault Injection (LDFI) as evidence.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {203322,
author = {Kamala Ramasubramanian and Kathryn Dahlgren and Asha Karim and Sanjana Maiya and Sarah Borland and Boaz Leskes and Peter Alvaro},
title = {Growing a protocol},
booktitle = {9th USENIX Workshop on Hot Topics in Cloud Computing (HotCloud 17)},
year = {2017},
address = {Santa Clara, CA},
url = {},
publisher = {USENIX Association},
month = jul