Commit 637dfd45 authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia

Update publications.bib

parent d4bc7492
...@@ -1752,27 +1752,30 @@ year = {2020}, ...@@ -1752,27 +1752,30 @@ year = {2020},
type = {phdthesis}, type = {phdthesis},
project = {concurrency}, project = {concurrency},
phdthesis = {Y}, phdthesis = {Y},
abstract = {The cloud has become popular for its low cost, high availability and abstract = {Cloud computing has become popular for its low cost. A storage sub-system is a key component
high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and in many cloud computing infrastructures, and many systems have used so-called“NoSQL”
Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface, databases, where data is often organised in a key-value structure, for example Dynamo DB,
to hide the complex internal implementation that consists of hundreds of thousands a distributed key-value store from Amazon Web Service (AWS). This is driven by the need
of machines globally that work together as a whole system, known as a distributed to store unstructured data, such as pictures, videos, or documents. Similar to traditional
system. Clients of those systems only need to work with the abstract interfaces. relational databases, transactions are the de facto interfaces in cloud storages. Many distributed
Transactions are the de facto interfaces in modern distributed databases. cloud storages often provide high availability and fault-tolerance, but adopt weak
Because of the CAP theorem, a distributed system must sacrifice strong consistency consistency, where individual server is allowed to operate without synchronisation in certain
to achieve high availability and high fault-tolerance. Engineers and researchers situation. Engineers and researchers have proposed various weak consistency models via reference
have proposed many reference implementations in specific setting for various weak implementations in their specific setting. However, there has been little work on formal,
consistency models. However, there have been little work on formalising the interfaces. implementation-independent definitions of consistency models. We introduce an interleaving
We introduce an interleaving operational semantics for describing such interfaces, operational semantics, with the focus on the client-observable behaviour of atomic transactions
with the focus on the client-observable behaviour of atomic transactions on on distributed key-value stores. Our semantics builds on abstract states comprising centralised,
distributed key-value stores. Our semantics builds on abstract states comprising global key-value stores, representing the overall states of distributed systems and multiple, mutually
centralised, global key-value stores and partial client views. We provide independent, partial client views, representing client-observable states. In each step, a
operational definitions of consistency models for our key-value stores which client with its view commits a transaction to the abstract key-value store, and this step must
are shown to be equivalent to the well-known declarative definitions of consistency satisfy certain conditions of the chosen consistency model, called an execution test, which is a
models for execution graphs. We explore two immediate applications of our semantics: novel operational definition of this consistency model. We provide definitions of various well known
specific protocols of databases for a specific consistency can be verified in consistency models such as snapshot isolation and causal consistency and show that our
our centralised semantics; programs can be directly shown to have invariant definitions are equivalent to the well-known declarative definitions of consistency models. We
properties such as robustness results against a weak consistency model.}, 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.},
} }
@InProceedings{Xiong2020Data, @InProceedings{Xiong2020Data,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment