Safe replication through bounded concurrency verification
Abstract
High-level data types are often associated with semantic invariants that must be preserved by any correct implementation. While having implementations enforce strong guarantees such as linearizability or serializability can often be used to prevent invariant violations in concurrent settings, such mechanisms are impractical in geo-distributed replicated environments, the platform of choice for many scalable Web services. To achieve high-availability essential to this domain, these environments admit various forms of weak consistency that do not guarantee all replicas have a consistent view of an application's state. Consequently, they often admit difficult-to-understand anomalous behaviors that violate a data type's invariants, but which are extremely challenging, even for experts, to understand and debug.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 24, 2018
- Source ID
- 10.1145/3276534
Entities
People
- Gowtham Kaki
- Kapil Earanky
- Kc Sivaramakrishnan
- Suresh Jagannathan
Organizations
- Air Force Research Laboratory
- National Science Foundation
- Purdue University
- University of Cambridge