文章基本信息

标题：Data Consistency in Transactional Storage Systems: A Centralised Semantics
本地全文：下载
作者：Shale Xiong ; Andrea Cerone ; Azalea Raad 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：166
页码：1-31
DOI：10.4230/LIPIcs.ECOOP.2020.21
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. Using our abstract states, we present operational definitions of well-known consistency models in the literature, and prove them to be equivalent to their existing declarative definitions using abstract executions. We explore two applications of our operational framework: 1) verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and 2) proving invariant properties of client programs.
关键词：Operational Semantics; Consistency Models; Transactions; Distributed Key-value Stores