2026-07-22T01:18:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13178 2024-03-06T10:49:55Z ddc:004 open_access

Data Consistency in Transactional Storage Systems: A Centralised Semantics Xiong, Shale Cerone, Andrea Raad, Azalea Gardner, Philippa Operational Semantics Consistency Models Transactions Distributed Key-value Stores 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Shale Xiong and Andrea Cerone and Azalea Raad and Philippa Gardner 2020 Is Part Of LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2020.21 urn:nbn:de:0030-drops-131782 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.21 eng https://creativecommons.org/licenses/by/3.0/legalcode