Replicated Data Types: Specification, Verification, Optimality

Cited 71 time in webofscience Cited 0 time in scopus
  • Hit : 463
  • Download : 0
DC FieldValueLanguage
dc.contributor.authorBurckhardt, Sebastianko
dc.contributor.authorGotsman, Alexeyko
dc.contributor.authorYang, Hongseokko
dc.contributor.authorZawirski, Marekko
dc.date.accessioned2017-08-08T06:54:12Z-
dc.date.available2017-08-08T06:54:12Z-
dc.date.created2017-08-02-
dc.date.created2017-08-02-
dc.date.created2017-08-02-
dc.date.created2017-08-02-
dc.date.issued2014-01-
dc.identifier.citationACM SIGPLAN NOTICES, v.49, no.1, pp.271 - 284-
dc.identifier.issn0362-1340-
dc.identifier.urihttp://hdl.handle.net/10203/225272-
dc.description.abstractGeographically distributed systems often rely on replicated eventually consistent data stores to achieve availability and performance. To resolve conflicting updates at different replicas, researchers and practitioners have proposed specialized consistency protocols, called replicated data types, that implement objects such as registers, counters, sets or lists. Reasoning about replicated data types has however not been on par with comparable work on abstract data types and concurrent data types, lacking specifications, correctness proofs, and optimality results. To fill in this gap, we propose a framework for specifying replicated data types using relations over events and verifying their implementations using replication-aware simulations. We apply it to 7 existing implementations of 4 data types with nontrivial conflict-resolution strategies and optimizations (last-writer-wins register, counter, multi-value register and observed-remove set). We also present a novel technique for obtaining lower bounds on the worst-case space overhead of data type implementations and use it to prove optimality of 4 implementations. Finally, we show how to specify consistency of replicated stores with multiple objects axiomatically, in analogy to prior work on weak memory models. Overall, our work provides foundational reasoning tools to support research on replicated eventually consistent stores.-
dc.languageEnglish-
dc.publisherASSOC COMPUTING MACHINERY-
dc.titleReplicated Data Types: Specification, Verification, Optimality-
dc.typeArticle-
dc.identifier.wosid000331120500024-
dc.identifier.scopusid2-s2.0-84893500058-
dc.type.rimsART-
dc.citation.volume49-
dc.citation.issue1-
dc.citation.beginningpage271-
dc.citation.endingpage284-
dc.citation.publicationnameACM SIGPLAN NOTICES-
dc.identifier.doi10.1145/2535838.2535848-
dc.contributor.localauthorYang, Hongseok-
dc.contributor.nonIdAuthorBurckhardt, Sebastian-
dc.contributor.nonIdAuthorGotsman, Alexey-
dc.contributor.nonIdAuthorZawirski, Marek-
dc.description.isOpenAccessN-
dc.type.journalArticleArticle; Proceedings Paper-
dc.subject.keywordAuthorReplication-
dc.subject.keywordAuthoreventual consistency-
dc.subject.keywordAuthorweak memory-
Appears in Collection
CS-Journal Papers(저널논문)
Files in This Item
There are no files associated with this item.
This item is cited by other documents in WoS
⊙ Detail Information in WoSⓡ Click to see webofscience_button
⊙ Cited 71 items in WoS Click to see citing articles in records_button

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0