Data Consistency in Transactional Storage Systems: a Centralised Approach
Venue
Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Publication Year
2020
Authors
Abstract
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 abstract states which we show to be equivalent to the well known declarative definitions of consistency model on abstract executions. We explore two applications, verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and proving invariant properties of client programs.