Search Results

Documents authored by Gotsman, Alexey

Document
DOI: 10.4230/LIPIcs.DISC.2024.10
Vertical Atomic Broadcast and Passive Replication

Authors: Manuel Bravo, Gregory Chockler, Alexey Gotsman, Alejandro Naser-Pastoriza, and Christian Roldán

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)

Abstract
Atomic broadcast is a reliable communication abstraction ensuring that all processes deliver the same set of messages in a common global order. It is a fundamental building block for implementing fault-tolerant services using either active (aka state-machine) or passive (aka primary-backup) replication. We consider the problem of implementing reconfigurable atomic broadcast, which further allows users to dynamically alter the set of participating processes, e.g., in response to failures or changes in the load. We give a complete safety and liveness specification of this communication abstraction and propose a new protocol implementing it, called Vertical Atomic Broadcast, which uses an auxiliary service to facilitate reconfiguration. In contrast to prior proposals, our protocol significantly reduces system downtime when reconfiguring from a functional configuration by allowing it to continue processing messages while agreement on the next configuration is in progress. Furthermore, we show that this advantage can be maintained even when our protocol is modified to support a stronger variant of atomic broadcast required for passive replication.
Cite as

Manuel Bravo, Gregory Chockler, Alexey Gotsman, Alejandro Naser-Pastoriza, and Christian Roldán. Vertical Atomic Broadcast and Passive Replication. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2024.10,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey and Naser-Pastoriza, Alejandro and Rold\'{a}n, Christian},
  title =	{{Vertical Atomic Broadcast and Passive Replication}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.10},
  URN =		{urn:nbn:de:0030-drops-212363},
  doi =		{10.4230/LIPIcs.DISC.2024.10},
  annote =	{Keywords: Reconfiguration, consensus, replication}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2023.21
Fault-Tolerant Computing with Unreliable Channels

Authors: Alejandro Naser-Pastoriza, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 286, 27th International Conference on Principles of Distributed Systems (OPODIS 2023)

Abstract
We study implementations of basic fault-tolerant primitives, such as consensus and registers, in message-passing systems subject to process crashes and a broad range of communication failures. Our results characterize the necessary and sufficient conditions for implementing these primitives as a function of the connectivity constraints and synchrony assumptions. Our main contribution is a new algorithm for partially synchronous consensus that is resilient to process crashes and channel failures and is optimal in its connectivity requirements. In contrast to prior work, our algorithm assumes the most general model of message loss where faulty channels are flaky, i.e., can lose messages without any guarantee of fairness. This failure model is particularly challenging for consensus algorithms, as it rules out standard solutions based on leader oracles and failure detectors. To circumvent this limitation, we construct our solution using a new variant of the recently proposed view synchronizer abstraction, which we adapt to the crash-prone setting with flaky channels.
Cite as

Alejandro Naser-Pastoriza, Gregory Chockler, and Alexey Gotsman. Fault-Tolerant Computing with Unreliable Channels. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{naserpastoriza_et_al:LIPIcs.OPODIS.2023.21,
  author =	{Naser-Pastoriza, Alejandro and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Fault-Tolerant Computing with Unreliable Channels}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.21},
  URN =		{urn:nbn:de:0030-drops-195118},
  doi =		{10.4230/LIPIcs.OPODIS.2023.21},
  annote =	{Keywords: Consensus, network partitions, liveness, synchronizers}
}
Document
DOI: 10.4230/LIPIcs.DISC.2022.12
Liveness and Latency of Byzantine State-Machine Replication

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)

Abstract
Byzantine state-machine replication (SMR) ensures the consistency of replicated state in the presence of malicious replicas and lies at the heart of the modern blockchain technology. Byzantine SMR protocols often guarantee safety under all circumstances and liveness only under synchrony. However, guaranteeing liveness even under this assumption is nontrivial. So far we have lacked systematic ways of incorporating liveness mechanisms into Byzantine SMR protocols, which often led to subtle bugs. To close this gap, we introduce a modular framework to facilitate the design of provably live and efficient Byzantine SMR protocols. Our framework relies on a view abstraction generated by a special SMR synchronizer primitive to drive the agreement on command ordering. We present a simple formal specification of an SMR synchronizer and its bounded-space implementation under partial synchrony. We also apply our specification to prove liveness and analyze the latency of three Byzantine SMR protocols via a uniform methodology. In particular, one of these results yields what we believe is the first rigorous liveness proof for the algorithmic core of the seminal PBFT protocol.
Cite as

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. Liveness and Latency of Byzantine State-Machine Replication. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2022.12,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Liveness and Latency of Byzantine State-Machine Replication}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.12},
  URN =		{urn:nbn:de:0030-drops-172037},
  doi =		{10.4230/LIPIcs.DISC.2022.12},
  annote =	{Keywords: Replication, blockchain, partial synchrony, liveness}
}
Document
DOI: 10.4230/LIPIcs.DISC.2020.23
Making Byzantine Consensus Live

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 179, 34th International Symposium on Distributed Computing (DISC 2020)

Abstract
Partially synchronous Byzantine consensus protocols typically structure their execution into a sequence of views, each with a designated leader process. The key to guaranteeing liveness in these protocols is to ensure that all correct processes eventually overlap in a view with a correct leader for long enough to reach a decision. We propose a simple view synchronizer abstraction that encapsulates the corresponding functionality for Byzantine consensus protocols, thus simplifying their design. We present a formal specification of a view synchronizer and its implementation under partial synchrony, which runs in bounded space despite tolerating message loss during asynchronous periods. We show that our synchronizer specification is strong enough to guarantee liveness for single-shot versions of several well-known Byzantine consensus protocols, including HotStuff, Tendermint, PBFT and SBFT. We furthermore give precise latency bounds for these protocols when using our synchronizer. By factoring out the functionality of view synchronization we are able to specify and analyze the protocols in a uniform framework, which allows comparing them and highlights trade-offs.
Cite as

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. Making Byzantine Consensus Live. In 34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2020.23,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Making Byzantine Consensus Live}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020.23},
  URN =		{urn:nbn:de:0030-drops-131013},
  doi =		{10.4230/LIPIcs.DISC.2020.23},
  annote =	{Keywords: Byzantine consensus, blockchain, partial synchrony, liveness}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.24
Privatization-Safe Transactional Memories

Authors: Artem Khyzha, Hagit Attiya, and Alexey Gotsman

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)

Abstract
Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions, and would prefer their programs to have a strongly atomic semantics, which allows transactions to be viewed as executing atomically with respect to non-transactional accesses. Since guaranteeing such semantics for arbitrary programs is prohibitively expensive, researchers have suggested guaranteeing it only for certain data-race free (DRF) programs, particularly those that follow the privatization idiom: from some point on, threads agree that a given object can be accessed non-transactionally. In this paper we show that a variant of Transactional DRF (TDRF) by Dalessandro et al. is appropriate for a class of privatization-safe TMs, which allow using privatization idioms. We prove that, if such a TM satisfies a condition we call privatization-safe opacity and a program using the TM is TDRF under strongly atomic semantics, then the program indeed has such semantics. We also present a method for proving privatization-safe opacity that reduces proving this generalization to proving the usual opacity, and apply the method to a TM based on two-phase locking and a privatization-safe version of TL2. Finally, we establish the inherent cost of privatization-safety: we prove that a TM cannot be progressive and have invisible reads if it guarantees strongly atomic semantics for TDRF programs.
Cite as

Artem Khyzha, Hagit Attiya, and Alexey Gotsman. Privatization-Safe Transactional Memories. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{khyzha_et_al:LIPIcs.DISC.2019.24,
  author =	{Khyzha, Artem and Attiya, Hagit and Gotsman, Alexey},
  title =	{{Privatization-Safe Transactional Memories}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.24},
  URN =		{urn:nbn:de:0030-drops-113310},
  doi =		{10.4230/LIPIcs.DISC.2019.24},
  annote =	{Keywords: Transactional memory, privatization, observational refinement}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2018.17
Federated Byzantine Quorum Systems

Authors: Álvaro García-Pérez and Alexey Gotsman

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

Abstract
Some of the recent blockchain proposals, such as Stellar and Ripple, use quorum-like structures typical for Byzantine consensus while allowing for open membership. This is achieved by constructing quorums in a decentralised way: each participant independently chooses whom to trust, and quorums arise from these individual decisions. Unfortunately, the theoretical foundations underlying such blockchains have not been thoroughly investigated. To close this gap, in this paper we study decentralised quorum construction by means of federated Byzantine quorum systems, used by Stellar. We rigorously prove the correctness of basic broadcast abstractions over federated quorum systems and establish their relationship to the classical Byzantine quorum systems. In particular, we prove correctness in the realistic setting where Byzantine nodes may lie about their trust choices. We show that this setting leads to a novel variant of Byzantine quorum systems where different nodes may have different understanding of what constitutes a quorum.
Cite as

Álvaro García-Pérez and Alexey Gotsman. Federated Byzantine Quorum Systems. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{garciaperez_et_al:LIPIcs.OPODIS.2018.17,
  author =	{Garc{\'\i}a-P\'{e}rez, \'{A}lvaro and Gotsman, Alexey},
  title =	{{Federated Byzantine Quorum Systems}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.17},
  URN =		{urn:nbn:de:0030-drops-100772},
  doi =		{10.4230/LIPIcs.OPODIS.2018.17},
  annote =	{Keywords: Blockchain, Stellar, Byzantine quorum systems}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.14
Multi-Shot Distributed Transaction Commit

Authors: Gregory Chockler and Alexey Gotsman

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
Atomic Commit Problem (ACP) is a single-shot agreement problem similar to consensus, meant to model the properties of transaction commit protocols in fault-prone distributed systems. We argue that ACP is too restrictive to capture the complexities of modern transactional data stores, where commit protocols are integrated with concurrency control, and their executions for different transactions are interdependent. As an alternative, we introduce Transaction Certification Service (TCS), a new formal problem that captures safety guarantees of multi-shot transaction commit protocols with integrated concurrency control. TCS is parameterized by a certification function that can be instantiated to support common isolation levels, such as serializability and snapshot isolation. We then derive a provably correct crash-resilient protocol for implementing TCS through successive refinement. Our protocol achieves a better time complexity than mainstream approaches that layer two-phase commit on top of Paxos-style replication.
Cite as

Gregory Chockler and Alexey Gotsman. Multi-Shot Distributed Transaction Commit. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chockler_et_al:LIPIcs.DISC.2018.14,
  author =	{Chockler, Gregory and Gotsman, Alexey},
  title =	{{Multi-Shot Distributed Transaction Commit}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.14},
  URN =		{urn:nbn:de:0030-drops-98038},
  doi =		{10.4230/LIPIcs.DISC.2018.14},
  annote =	{Keywords: Atomic commit problem, two-phase commit, Paxos}
}
Document
DOI: 10.4230/DagRep.8.2.101
Data Consistency in Distributed Systems: Algorithms, Programs, and Databases (Dagstuhl Seminar 18091)

Authors: Annette Bieniusa, Alexey Gotsman, Bettina Kemme, and Marc Shapiro

Published in: Dagstuhl Reports, Volume 8, Issue 2 (2018)

Abstract
For decades distributed computing has been mainly an academic subject. Today, it has become mainstream: our connected world demands applications that are inherently distributed, and the usage of shared, distributed, peer-to-peer or cloud-computing infrastructures are increasingly common. However, writing distributed applications that are both correct and well distributed (e.g., highly available) is extremely challenging. In fact, there exists a fundamental trade-off between data consistency, availability, and the ability to tolerate failures. This trade-off has implications on the design of the entire distributed computing infrastructure, including storage systems, compilers and runtimes, application development frameworks and programming languages. Unfortunately, this also has significant implications on the programming model exposed to the designers and developers of applications. We need to enable programmers who are not experts in these subtle aspects to build distributed applications that remain correct in the presence of concurrency, failures, churn, replication, dynamically-changing and partial information, high load, absence of a single line of time, etc. This Dagstuhl Seminar proposes to bring together researchers and practitioners in the areas of distributed systems, programming languages, verifications, and databases. We would like to understand the lessons learnt in building scalable and correct distributed systems, the design patterns that have emerged, and explore opportunities for distilling these into programming methodologies, programming tools, and languages to make distributed computing easier and more accessible. Main issues in discussion: Application writers are constantly making trade-offs between consistency and availability. What kinds of tools and methodologies can we provide to simplify this decision making? How does one understand the implications of a design choice? Available systems are hard to design, test and debug. Do existing testing and debugging tools suffice for identifying and isolating bugs due to weak consistency? How can these problems be identified in production using live monitoring? Can we formalize commonly desired (generic) correctness (or performance) properties? How can we teach programmers about these formalisms and make them accessible to a wide audience? Can we build verification or testing tools to check that systems have these desired correctness properties? How do applications achieve the required properties, while ensuring adequate performance, in practice? What design patterns and idioms work well? To what degree can these properties be guaranteed by the platform (programming language, libraries, and runtime system)? What are the responsibilities of the application developer, and what tools and information does she have?
Cite as

Annette Bieniusa, Alexey Gotsman, Bettina Kemme, and Marc Shapiro. Data Consistency in Distributed Systems: Algorithms, Programs, and Databases (Dagstuhl Seminar 18091). In Dagstuhl Reports, Volume 8, Issue 2, pp. 101-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{bieniusa_et_al:DagRep.8.2.101,
  author =	{Bieniusa, Annette and Gotsman, Alexey and Kemme, Bettina and Shapiro, Marc},
  title =	{{Data Consistency in Distributed Systems: Algorithms, Programs, and Databases (Dagstuhl Seminar 18091)}},
  pages =	{101--121},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{2},
  editor =	{Bieniusa, Annette and Gotsman, Alexey and Kemme, Bettina and Shapiro, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.2.101},
  URN =		{urn:nbn:de:0030-drops-92923},
  doi =		{10.4230/DagRep.8.2.101},
  annote =	{Keywords: consistency, CRDTs, Distributed Algorithms, distributed computing, Distributed Systems, partitioning, replication, Strong Consistency, transactions, Weak Consistency}
}
Document
DOI: 10.4230/LIPIcs.DISC.2017.23
Consistency Models with Global Operation Sequencing and their Composition

Authors: Alexey Gotsman and Sebastian Burckhardt

Published in: LIPIcs, Volume 91, 31st International Symposium on Distributed Computing (DISC 2017)

Abstract
Modern distributed systems often achieve availability and scalability by providing consistency guarantees about the data they manage weaker than linearizability. We consider a class of such consistency models that, despite this weakening, guarantee that clients eventually agree on a global sequence of operations, while seeing a subsequence of this final sequence at any given point of time. Examples of such models include the classical Total Store Order (TSO) and recently proposed dual TSO, Global Sequence Protocol (GSP) and Ordered Sequential Consistency. We define a unified model, called Global Sequence Consistency (GSC), that has the above models as its special cases, and investigate its key properties. First, we propose a condition under which multiple objects each satisfying GSC can be composed so that the whole set of objects satisfies GSC. Second, we prove an interesting relationship between special cases of GSC - GSP, TSO and dual TSO: we show that clients that do not communicate out-of-band cannot tell the difference between these models. To obtain these results, we propose a novel axiomatic specification of GSC and prove its equivalence to the operational definition of the model.
Cite as

Alexey Gotsman and Sebastian Burckhardt. Consistency Models with Global Operation Sequencing and their Composition. In 31st International Symposium on Distributed Computing (DISC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 91, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gotsman_et_al:LIPIcs.DISC.2017.23,
  author =	{Gotsman, Alexey and Burckhardt, Sebastian},
  title =	{{Consistency Models with Global Operation Sequencing and their Composition}},
  booktitle =	{31st International Symposium on Distributed Computing (DISC 2017)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-053-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{91},
  editor =	{Richa, Andr\'{e}a},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2017.23},
  URN =		{urn:nbn:de:0030-drops-79748},
  doi =		{10.4230/LIPIcs.DISC.2017.23},
  annote =	{Keywords: Consistency conditions, Weak memory models, Compositionality}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.26
Algebraic Laws for Weak Consistency

Authors: Andrea Cerone, Alexey Gotsman, and Hongseok Yang

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Modern distributed systems often rely on so called weakly consistent databases, which achieve scalability by weakening consistency guarantees of distributed transaction processing. The semantics of such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications. The former has been used for specifying and verifying the implementation of the databases, while the latter for proving properties of client programs of the databases. In this paper, we present a set of novel algebraic laws (inequalities) that connect these two styles of specifications. The laws relate binary relations used in a specification based on abstract executions to those used in a specification based on dependency graphs. We then show that this algebraic connection gives rise to so called robustness criteria: conditions which ensure that a client program of a weakly consistent database does not exhibit anomalous behaviours due to weak consistency. These criteria make it easy to reason about these client programs, and may become a basis for dynamic or static program analyses. For a certain class of consistency models specifications, we prove a full abstraction result that connects the two styles of specifications.
Cite as

Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic Laws for Weak Consistency. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cerone_et_al:LIPIcs.CONCUR.2017.26,
  author =	{Cerone, Andrea and Gotsman, Alexey and Yang, Hongseok},
  title =	{{Algebraic Laws for Weak Consistency}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.26},
  URN =		{urn:nbn:de:0030-drops-77946},
  doi =		{10.4230/LIPIcs.CONCUR.2017.26},
  annote =	{Keywords: Weak Consistency Models, Distributed Databases, Dependency Graphs}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.7
Robustness against Consistency Models with Atomic Visibility

Authors: Giovanni Bernardi and Alexey Gotsman

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
To achieve scalability, modern Internet services often rely on distributed databases with consistency models for transactions weaker than serializability. At present, application programmers often lack techniques to ensure that the weakness of these consistency models does not violate application correctness. We present criteria to check whether applications that rely on a database providing only weak consistency are robust, i.e., behave as if they used a database providing serializability. When this is the case, the application programmer can reap the scalability benefits of weak consistency while being able to easily check the desired correctness properties. Our results handle systematically and uniformly several recently proposed weak consistency models, as well as a mechanism for strengthening consistency in parts of an application.
Cite as

Giovanni Bernardi and Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bernardi_et_al:LIPIcs.CONCUR.2016.7,
  author =	{Bernardi, Giovanni and Gotsman, Alexey},
  title =	{{Robustness against Consistency Models with Atomic Visibility}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.7},
  URN =		{urn:nbn:de:0030-drops-61652},
  doi =		{10.4230/LIPIcs.CONCUR.2016.7},
  annote =	{Keywords: Robustness, Replication, Consistency models, Transactions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.58
A Framework for Transactional Consistency Models with Atomic Visibility

Authors: Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of distributed transaction processing. The semantics of programs interacting with such a database depends on its consistency model, defining these guarantees. Unfortunately, consistency models are usually stated informally or using disparate formalisms, often tied to the database internals. To deal with this problem, we propose a framework for specifying a variety of consistency models for transactions uniformly and declaratively. Our specifications are given in the style of weak memory models, using structures of events and relations on them. The specifications are particularly concise because they exploit the property of atomic visibility guaranteed by many consistency models: either all or none of the updates by a transaction can be visible to another one. This allows the specifications to abstract from individual events inside transactions. We illustrate the use of our framework by specifying several existing consistency models. To validate our specifications, we prove that they are equivalent to alternative operational ones, given as algorithms closer to actual implementations. Our work provides a rigorous foundation for developing the metatheory of the novel form of concurrency arising in weakly consistent large-scale databases.
Cite as

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cerone_et_al:LIPIcs.CONCUR.2015.58,
  author =	{Cerone, Andrea and Bernardi, Giovanni and Gotsman, Alexey},
  title =	{{A Framework for Transactional Consistency Models with Atomic Visibility}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{58--71},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.58},
  URN =		{urn:nbn:de:0030-drops-53756},
  doi =		{10.4230/LIPIcs.CONCUR.2015.58},
  annote =	{Keywords: Replication, Consistency models, Transactions}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact