Understanding and Reasoning about Distributed Data Types

Regular data structures like stacks, queues, sets and lists are practically unusable in distributed settings because their operations require strong and frequent synchronization. As it is a well-known trade-off in distributed setting, strong synchronization enforces low availability if the state of the data structure is partitioned across replicas. Therefore, it is impossible to have efficient implementations of regular data structures for distributed programs.
Luckily, most of the distributed programs require weaker guarantees than the standard data structures. To take advantage of this, Conflict-free and Convergent Replicated Data Types (CRDTs) [1] are proposed as basic data types for distributed programs. CRDTs are loosely synchronized and hence they are efficient. However, loose synchronization leads to more possible interleavings and more possible behaviours. Therefore, it is hard to reason about programs with CRDTs manually or using testing methods. Moreover, behaviours of the CRDTs highly dependent on the underlying semantic model of the distributed platform and the network.
This project aims to develop reasoning methodologies for CRDTs using formal methods techniques and develop new specifications for replicated data types.
[1] https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type