Effective verification of replicated data types using later appearance records (LAR)

Mukund, Madhavan ; Shenoy R., Gautham ; Suresh, S. P. (2015) Effective verification of replicated data types using later appearance records (LAR) In: 13th International Symposium, ATVA 2015, 12-15 Oct 2015, Shanghai, China.

Full text not available from this repository.

Official URL: https://link.springer.com/chapter/10.1007/978-3-31...

Related URL: http://dx.doi.org/10.1007/978-3-319-24953-7_23


Replicated data types store copies of identical data across multiple servers in a distributed system. For the replicas to satisfy strong 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. While earlier work such as [2] and [9] has concentrated on declarative frameworks for formally specifying Conflict-free Replicated Data Types (CRDTs) and conditions that guarantee the existence of finite-state (distributed) reference implementations, there has not been a systematic attempt so far to use the declarative specifications for effective verification of CRDTs. In this work, we propose a simple global reference implementation for CRDTs specified declaratively, and simple conditions under which this is guaranteed to be finite. Our implementation uses the technique of Later Appearance Record (LAR). We also outline a methodology for effective verification of CRDT implementations using CEGAR.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer.
Keywords:Network Node; Message Delivery; Reference Implementation; Relevant Node; Maximum Arity
ID Code:114104
Deposited On:25 May 2018 04:55
Last Modified:25 May 2018 04:55

Repository Staff Only: item control page