Ph.D. Thesis, Imperial College London
The cloud has become popular for its low cost, high availability and high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface, to hide the complex internal implementation that consists of hundreds of thousands of machines globally that work together as a whole system, known as a distributed system. Clients of those systems only need to work with the abstract interfaces. Transactions are the de facto interfaces in modern distributed databases. Because of the CAP theorem, a distributed system must sacrifice strong consistency to achieve high availability and high fault-tolerance. Engineers and researchers have proposed many reference implementations in specific setting for various weak consistency models. However, there have been little work on formalising the interfaces. We introduce an interleaving operational semantics for describing such interfaces, 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 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 models for execution graphs. We explore two immediate applications of our semantics: specific protocols of databases for a specific consistency can be verified in our centralised semantics; programs can be directly shown to have invariant properties such as robustness results against a weak consistency model.