Growing a Protocol
Verification is often regarded as a one-time procedure undertaken after protocol specification is completed and before actual implementation. 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. The process nullifies correctness guarantees determined at verification time. Existing software quality techniques are insufficient to support the correctness of desired fault tolerance properties within the context of distributed systems because the failure space includes both execution schedules and inputs. We present our experience evolving a data replication protocol at Elastic as evidence that our community should explore the intersection of testing and verification to better ensure quality for distributed software. We also describe how a novel bug-finding methodology called LDFI helps restore many of the benefits of classic software quality best practices for evolving distributed systems.
Monday, April 24, 2017 at 1:15 PM