Venue

Ph.D. Thesis, Imperial College London

Publication Year

2020

Authors

Abstract

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 well known 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.

Source Materials