Concurrency Contracts for Designing Highly Available Replicated Data Types

ABSTRACT Introduction Distributed system programmers rely on Replicated Data Types (RDTs), which resemble sequential data types but incorporate conflict resolution strategies to guarantee convergence when conflicts occur. The semantics of RDTs depend on the underlying conflict resolution strategy, but these cannot be customized. Moreover, ensuring state convergence alone is not enough because the resulting state may break application‐specific invariants. Although some approaches support application‐level invariants atop existing RDTs, they do not help build the RDT in the first place. As a result, custom RDTs are implemented using ad hoc approaches, which are known to be error‐prone and result in brittle systems. We previously proposed Explicitly Consistent Replicated Objects (ECROs) to address these issues, enabling programmers to build custom RDTs by augmenting sequential data types with a distributed specification. However, the specification requires a complete first‐order logic formalization of the data type and its operations, which is hard to develop. Furthermore, subtle errors in the specification may result in runtime anomalies such as state divergence and broken invariants. Methods To tackle these problems, we combine the ECRO programming model with automated program verification. The result is EFx, a minimalist object‐oriented programming language whose core consists of a contract system that simplifies the development of RDTs. EFx does not require tedious first‐order logic specifications because it analyses the data type's implementation, thereby preventing runtime anomalies due to errors in the specification. Results We reconstruct the original portfolio of ECROs in EFx to validate our approach. We consistently achieve a 2x to 4x reduction of the code size. Additionally, we implement several applications, such as the RUBiS auction system, the SmallBank benchmark, a distributed voting game, and an airline reservation system. Conclusion Our evaluation shows that EFx simplifies the development of RDTs.