Repository logo
 

AMC: Towards Trustworthy and Explorable CRDT Applications with the Automerge Model Checker

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Mortier, Richard 

Abstract

Conflict-free Replicated Data Types (CRDTs) enable local-first operations and asynchronous collaboration without the need for always-on centralised services. CRDTs can have a high overhead, so implementations need to be optimised, but this optimisation can lead to bugs despite the use of test suites and fuzzing. Furthermore, using CRDTs in applications is complex, observing unexpected conflict resolution, issues synchronising documents and difficulties implementing appropriate data models. Automerge is a library, exposing a JSON CRDT, that sees users having difficulties in modelling their problems, understanding their edge cases and implementing applications correctly. We introduce the Automerge Model Checker (AMC), empowering application developers to check properties about their implementations and explore them dynamically. AMC can check a range of applications as well as being able to check properties about the core of Automerge itself, helping to make more trustworthy Automerge applications.

Description

Keywords

conflict-free replicated data types, distributed systems, eventual consistency, model checking

Journal Title

Proceedings of the 10th Workshop on Principles and Practice of Consistency for Distributed Data

Conference Name

10th Workshop on Principles and Practice of Consistency for Distributed Data

Journal ISSN

Volume Title

Publisher

ACM
Relationships
Is supplemented by:

Version History

Now showing 1 - 2 of 2
VersionDateSummary
2023-11-22 09:09:38
Published version added
1*
2023-04-12 23:30:36
* Selected version