Ensuring Convergence and Invariants Without Coordination (Artifact)

Our related paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. We implemented the core of the No-Op replication protocol in VeriFx [De Porre et al., 2023], a programming language for RDTs with automated proof capabilities. Alongside the algorithm implementation, we developed formal proofs to automatically verify the algorithm’s correctness properties when applied to specific data types or application implementations. This artifact bundles the implementation of the No-Op framework, various CRDTs [Marc Shapiro et al., 2011], and an eBay-like auction system akin to the RUBiS system [Emmanuel Cecchet et al., 2002] described in Section 5 of the paper. The artifact also provides a Dockerfile that can be used to reproduce the verification results (Section 4 of the paper).