Bounded implementations of replicated data types

Mukund, Madhavan ; Shenoy R., Gautham ; Suresh, S. P. (2015) Bounded implementations of replicated data types In: 16th International Conference, VMCAI 2015, 12-14 Jan 2015, Mumbai, India.

Full text not available from this repository.

Official URL:

Related URL:


Replicated data types store copies of identical data across multiple servers in a distributed system. For the replicas to satisfy eventual consistency, these data types should be designed to guarantee conflict free convergence of all copies in the presence of concurrent updates. This requires maintaining history related metadata that, in principle, is unbounded. Burkhardt et al have proposed a declarative framework to specify eventually consistent replicated data types (ECRDTs). Using this, they introduce replication-aware simulations for verifying the correctness of ECRDT implementations. Unfortunately, this approach does not yield an effective strategy for formal verification. By imposing reasonable restrictions on the underlying network, we recast their declarative framework in terms of standard labelled partial orders. For well-behaved ECRDT specifications, we are able to construct canonical finite-state reference implementations with bounded metadata, which can be used for formal verification of ECRDT implementations via CEGAR. We can also use our reference implementations to design more effective test suites for ECRDT implementations.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag.
Keywords:Partial Order; Test Suite; Bounded Solution; Primary Information; Reference Implementation
ID Code:114105
Deposited On:25 May 2018 04:54
Last Modified:25 May 2018 04:54

Repository Staff Only: item control page