VeriFx: Correct Replicated Data Types for the Masses

Research output: Chapter in Book/Report/Conference proceedingConference paper

Abstract

Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence. Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants. Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalization instead of a real-world implementation. Furthermore, writing mechanized proofs is reserved for verification experts and is extremely time-consuming. To simplify the design, implementation, and verification of RDTs, we propose VeriFx, a specialized programming language for RDTs with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala and JavaScript). VeriFx provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties. We use the libraries to implement and verify an extensive portfolio of 51 CRDTs, 16 of which are used in industrial databases, and reproduce a study on the correctness of OT functions.
Original languageEnglish
Title of host publicationVeriFx: Correct Replicated Data Types for the Masses
EditorsGuido Salvaneschi, Karim Ali
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages1-45
Number of pages45
Volume263
Edition37th
ISBN (Electronic)978-3-95977-281-5
DOIs
Publication statusPublished - 2023
EventEuropean Conference on Object-Oriented Programming - University of Washington, Seattle campus, Seattle, United States
Duration: 17 Jul 202321 Jul 2023
Conference number: 2023

Publication series

NameEuropean Conference on Object-Oriented Programming (ECOOP 2023)

Conference

ConferenceEuropean Conference on Object-Oriented Programming
Abbreviated titleECOOP
Country/TerritoryUnited States
CitySeattle
Period17/07/2321/07/23

Bibliographical note

Software (ECOOP 2023 Artifact Evaluation approved artifact) https://doi.org/10.4230/DARTS.9.2.19

Keywords

  • distributed systems
  • eventual consistency
  • replicated data types
  • verification

Fingerprint

Dive into the research topics of 'VeriFx: Correct Replicated Data Types for the Masses'. Together they form a unique fingerprint.

Cite this