Commit daeb2401 authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia

Update publications.bib

parent 7aa4b7c5
......@@ -1749,6 +1749,36 @@ and C, and use these tools to find bugs in real-world code,
thus demonstrating the viability of our parametric approach.},
}
@PhdThesis{Xiong2020Parametric,
author = {Shale Xiong},
title = {Parametric Operational Semantics for Consistency Models},
school = {Imperial College London},
year = {2020},
type = {phdthesis},
project = {concurrency},
abstract = {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.},
}
@InProceedings{Xiong2020Data,
author = {Shale Xiong and
Andrea Cerone and
......
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