Cloud computing has become popular for its low cost. A storage sub-system is a key component
in many cloud computing infrastructures, and many systems have used so-called“NoSQL”
databases, where data is often organised in a key-value structure, for example Dynamo DB,
a distributed key-value store from Amazon Web Service (AWS). This is driven by the need
to store unstructured data, such as pictures, videos, or documents. Similar to traditional
relational databases, transactions are the de facto interfaces in cloud storages. Many distributed
cloud storages often provide high availability and fault-tolerance, but adopt weak
consistency, where individual server is allowed to operate without synchronisation in certain
situation. Engineers and researchers have proposed various weak consistency models via reference
implementations in their specific setting. However, there has been little work on formal,
implementation-independent definitions of consistency models. We introduce an interleaving
operational semantics, with the focus on the client-observable behaviour of atomic transactions
on distributed key-value stores. Our semantics builds on abstract states comprising centralised,
global key-value stores, representing the overall states of distributed systems and multiple, mutually
independent, partial client views, representing client-observable states. In each step, a
client with its view commits a transaction to the abstract key-value store, and this step must
satisfy certain conditions of the chosen consistency model, called an execution test, which is a
novel operational definition of this consistency model. We provide definitions of various wellknown
consistency models such as snapshot isolation and causal consistency and show that our
definitions are equivalent to the well-known declarative definitions of consistency models. We
then explore two immediate applications of our semantics: specific implementation protocols
can be verified in our operational semantics via trace refinement; client programs can be shown
to satisfies invariant properties. These two applications show that our operational semantics
captures the interfaces between client programs and implementation protocols.