From daeb2401074658e28a2b08de2657d779047f3fd8 Mon Sep 17 00:00:00 2001
From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk>
Date: Wed, 13 May 2020 11:05:31 +0100
Subject: [PATCH] Update publications.bib
---
publications.bib | 30 ++++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)
diff --git a/publications.bib b/publications.bib
index 4514bba..d6f45f0 100644
--- a/publications.bib
+++ b/publications.bib
@@ -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
--
GitLab