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. We provide operational definitions of consistency models for our key-value stores which are shown to be equivalent to the well-known declarative definitions of consistency model for execution graphs. We explore two immediate applications of our semantics: specific protocols of geo-replicated databases (e.g. COPS) and partitioned databases (e.g. Clock-SI) can be shown to be correct for a specific consistency model by embedding them in our centralised semantics; programs can be directly shown to have invariant properties such as robustness results against a weak consistency model.
@article{arxiv.1901.10615,
title = {Data Consistency in Transactional Storage Systems: a Centralised Approach},
author = {Shale Xiong and Andrea Cerone and Azalea Raad and Philippa Gardner},
journal= {arXiv preprint arXiv:1901.10615},
year = {2019}
}