Volume
LIPIcs, Volume 125
22nd International Conference on Principles of Distributed Systems (OPODIS 2018)
Event
OPODIS 2018, December 17-19, 2018, Hong Kong, ChinaEditors
Publication Details
- published at: 2019-01-15
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-098-9
- DBLP: db/conf/opodis/opodis2018
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 125, OPODIS'18, Complete Volume
Abstract
LIPIcs, Volume 125, OPODIS'18, Complete Volume
Cite as
22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{cao_et_al:LIPIcs.OPODIS.2018,
title = {{LIPIcs, Volume 125, OPODIS'18, Complete Volume}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
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},
URN = {urn:nbn:de:0030-drops-101742},
doi = {10.4230/LIPIcs.OPODIS.2018},
annote = {Keywords: Computer systems organization, Dependable and fault-tolerant systems and networks, Computing methodologies, Distributed algorithms, Networks, Mobile networks, Wireless access networks, Ad hoc networks, Software and its engineering, Distributed systems organizing principles,}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{cao_et_al:LIPIcs.OPODIS.2018.0,
author = {Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {0:i--0:xx},
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.0},
URN = {urn:nbn:de:0030-drops-100607},
doi = {10.4230/LIPIcs.OPODIS.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Keynote
Complexity of Multi-Valued Register Simulations: A Retrospective (Keynote)
Abstract
I will provide a historical perspective on wait-free simulations of multi-bit shared registers using single-bit shared registers, starting with classical results from the last century and ending with an overview of the recent resurgence of interest in the topic. Particular emphasis will be placed on the space and step complexities of such simulations.
Cite as
Jennifer L. Welch. Complexity of Multi-Valued Register Simulations: A Retrospective (Keynote). In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{welch:LIPIcs.OPODIS.2018.1,
author = {Welch, Jennifer L.},
title = {{Complexity of Multi-Valued Register Simulations: A Retrospective}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {1:1--1:1},
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.1},
URN = {urn:nbn:de:0030-drops-100611},
doi = {10.4230/LIPIcs.OPODIS.2018.1},
annote = {Keywords: Distributed Systems}
}
Document
Keynote
Distributed Systems and Databases of the Globe Unite! The Cloud, the Edge and Blockchains (Keynote)
Abstract
Significant paradigm shifts are occurring in Access patterns are widely dispersed and large scale analysis requires real-time responses. Many of the fundamental challenges have been studied and explored by both the distributed systems and the database communities for decades. However, the current changing and scalable setting often requires a rethinking of basic assumptions and premises. The rise of the cloud computing paradigm with its global reach has resulted in novel approaches to integrate traditional concepts in novel guises to solve fault-tolerance and scalability challenges. This is especially the case when users require real-time global access. Exploiting edge cloud resources becomes critical for improved performance, which requires a reevaluation of many paradigms, even for a traditional problem like caching. The need for transparency and accessibility has led to innovative ways for managing large scale replicated logs and ledgers, giving rise to blockchains and their many applications. In this talk we will be explore some of these new trends while emphasizing the novel challenges they raise from both distributed systems as well as database points of view. We will propose a unifying framework for traditional consensus and commitment protocols, and discuss novel protocols that exploit edge computing resources to enhance performance. We will highlight the advantages and discuss the limitations of blockchains. Our overall goal is to explore approaches that unite and exploit many of the significant efforts made in distributed systems and databases to address the novel and pressing needs of today's global computing infrastructure.
Cite as
Amr El Abbadi. Distributed Systems and Databases of the Globe Unite! The Cloud, the Edge and Blockchains (Keynote). In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{abbadi:LIPIcs.OPODIS.2018.2,
author = {Abbadi, Amr El},
title = {{Distributed Systems and Databases of the Globe Unite! The Cloud, the Edge and Blockchains}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {2:1--2:1},
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.2},
URN = {urn:nbn:de:0030-drops-100625},
doi = {10.4230/LIPIcs.OPODIS.2018.2},
annote = {Keywords: Consensus, Commitment, Cloud, Edge Computing, Blockchain}
}
Document
Keynote
How to Make Decisions (Optimally) (Keynote)
Abstract
Distributed systems are constantly faced with difficult decisions to make, such as in scheduling, caching, and traffic routing, to name a few. In most of these scenarios, the optimal decision is unknown and depends heavily on context. How can a system designer know if they have deployed the best decision-making policy, or if a different policy would perform better? As a community, we have developed a few methodologies for answering this question, some of them offline (e.g., simulation, trace-driven modeling) and some of them online (e.g., A/B testing). Neither approach is satisfactory: the offline methods suffer from bias and rely heavily on domain knowledge; the online methods are costly and difficult to deploy. What system designers ideally seek is the ability to ask "what if" questions about a policy without ever deploying it, which is called counterfactual evaluation. In this talk, I will show how reinforcement learning and causal inference can be synthesized to counterfactually evaluate a distributed system. We will apply this methodology to infrastructure systems in Azure, and face fundamental challenges and opportunities along the way. This talk will serve as an introduction to reinforcement learning and the counterfactual way of thinking, which I hope will interest and inspire the OPODIS community.
I will start by introducing reinforcement learning (RL) as the right framework for modeling decisions in a distributed system. In RL, an agent learns by interacting with its environment: i.e., making decisions and receiving feedback for them. This is a stark contrast to traditional (supervised) learning, where the correct answer, or "label", is known. Since an RL agent does not know the correct answer, it must constantly explore its world by randomizing some of its decisions. Now it turns out that this randomization, if used correctly, can give us a special superpower: the ability to evaluate policies that have never been deployed. As magical as this may sound, we can use statistics to show that this evaluation is indeed correct.
Unfortunately, applying this methodology to distributed systems is far from straightforward. Systems are complex, stateful amalgamations of components that navigate large decision spaces. We will need to wear both an RL hat and a systems hat to address these challenges. On the other hand, systems also present exciting opportunities. Many systems already use randomization in their decisions, e.g., to distribute data or work over replicas, or to manage resource contention. Sometimes, a conservative decision can implicitly yield feedback for other decisions: for example, when waiting for a timeout to expire, we automatically get feedback for what would have happened if we waited for any shorter amount of time. I will show how we can harvest this randomness and implicit feedback to achieve more effective counterfactual evaluation.
We will apply all of the above ideas to two production infrastructure systems in Azure: a machine health monitor that decides when to reboot unresponsive machines, and a geo-distributed edge proxy that chooses the TCP configuration of each proxy machine. In both cases, we are able to counterfactually evaluate arbitrary policies with estimates that match the ground truth. Production environments raise interesting constraints and challenges, some of which are preventing us from scaling up our methodology. I will describe a possible path forward, and invite others in the community to contemplate these problems as well.
Cite as
Siddhartha Sen. How to Make Decisions (Optimally) (Keynote). In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sen:LIPIcs.OPODIS.2018.3,
author = {Sen, Siddhartha},
title = {{How to Make Decisions (Optimally)}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {3:1--3:1},
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.3},
URN = {urn:nbn:de:0030-drops-100638},
doi = {10.4230/LIPIcs.OPODIS.2018.3},
annote = {Keywords: reinforcement learning, distributed systems, counterfactual evaluation}
}
Document
Sparse Matrix Multiplication and Triangle Listing in the Congested Clique Model
Abstract
We show how to multiply two n x n matrices S and T over semirings in the Congested Clique model, where n nodes communicate in a fully connected synchronous network using O(log{n})-bit messages, within O(nz(S)^{1/3} nz(T)^{1/3}/n + 1) rounds of communication, where nz(S) and nz(T) denote the number of non-zero elements in S and T, respectively. By leveraging the sparsity of the input matrices, our algorithm greatly reduces communication costs compared with general multiplication algorithms [Censor-Hillel et al., PODC 2015], and thus improves upon the state-of-the-art for matrices with o(n^2) non-zero elements. Moreover, our algorithm exhibits the additional strength of surpassing previous solutions also in the case where only one of the two matrices is such. Particularly, this allows to efficiently raise a sparse matrix to a power greater than 2. As applications, we show how to speed up the computation on non-dense graphs of 4-cycle counting and all-pairs-shortest-paths.
Our algorithmic contribution is a new deterministic method of restructuring the input matrices in a sparsity-aware manner, which assigns each node with element-wise multiplication tasks that are not necessarily consecutive but guarantee a balanced element distribution, providing for communication-efficient multiplication.
Moreover, this new deterministic method for restructuring matrices may be used to restructure the adjacency matrix of input graphs, enabling faster deterministic solutions for graph related problems. As an example, we present a new sparsity aware, deterministic algorithm which solves the triangle listing problem in O(m/n^{5/3} + 1) rounds, a complexity that was previously obtained by a randomized algorithm [Pandurangan et al., SPAA 2018], and that matches the known lower bound of Omega~(n^{1/3}) when m=n^2 of [Izumi and Le Gall, PODC 2017, Pandurangan et al., SPAA 2018]. Naturally, our triangle listing algorithm also implies triangle counting within the same complexity of O(m/n^{5/3} + 1) rounds, which is (possibly more than) a cubic improvement over the previously known deterministic O(m^2/n^3)-round algorithm [Dolev et al., DISC 2012].
Cite as
Keren Censor-Hillel, Dean Leitersdorf, and Elia Turner. Sparse Matrix Multiplication and Triangle Listing in the Congested Clique Model. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{censorhillel_et_al:LIPIcs.OPODIS.2018.4,
author = {Censor-Hillel, Keren and Leitersdorf, Dean and Turner, Elia},
title = {{Sparse Matrix Multiplication and Triangle Listing in the Congested Clique Model}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {4:1--4:17},
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.4},
URN = {urn:nbn:de:0030-drops-100645},
doi = {10.4230/LIPIcs.OPODIS.2018.4},
annote = {Keywords: congested clique, matrix multiplication, triangle listing}
}
Document
Large-Scale Distributed Algorithms for Facility Location with Outliers
Abstract
This paper presents fast, distributed, O(1)-approximation algorithms for metric facility location problems with outliers in the Congested Clique model, Massively Parallel Computation (MPC) model, and in the k-machine model. The paper considers Robust Facility Location and Facility Location with Penalties, two versions of the facility location problem with outliers proposed by Charikar et al. (SODA 2001). The paper also considers two alternatives for specifying the input: the input metric can be provided explicitly (as an n x n matrix distributed among the machines) or implicitly as the shortest path metric of a given edge-weighted graph. The results in the paper are:
- Implicit metric: For both problems, O(1)-approximation algorithms running in O(poly(log n)) rounds in the Congested Clique and the MPC model and O(1)-approximation algorithms running in O~(n/k) rounds in the k-machine model.
- Explicit metric: For both problems, O(1)-approximation algorithms running in O(log log log n) rounds in the Congested Clique and the MPC model and O(1)-approximation algorithms running in O~(n/k) rounds in the k-machine model.
Our main contribution is to show the existence of Mettu-Plaxton-style O(1)-approximation algorithms for both Facility Location with outlier problems. As shown in our previous work (Berns et al., ICALP 2012, Bandyapadhyay et al., ICDCN 2018) Mettu-Plaxton style algorithms are more easily amenable to being implemented efficiently in distributed and large-scale models of computation.
Cite as
Tanmay Inamdar, Shreyas Pai, and Sriram V. Pemmaraju. Large-Scale Distributed Algorithms for Facility Location with Outliers. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{inamdar_et_al:LIPIcs.OPODIS.2018.5,
author = {Inamdar, Tanmay and Pai, Shreyas and Pemmaraju, Sriram V.},
title = {{Large-Scale Distributed Algorithms for Facility Location with Outliers}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {5:1--5: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.5},
URN = {urn:nbn:de:0030-drops-100650},
doi = {10.4230/LIPIcs.OPODIS.2018.5},
annote = {Keywords: Distributed Algorithms, Clustering with Outliers, Metric Facility Location, Massively Parallel Computation, k-machine model, Congested Clique}
}
Document
Equilibria of Games in Networks for Local Tasks
Abstract
Distributed tasks such as constructing a maximal independent set (MIS) in a network, or properly coloring the nodes or the edges of a network with reasonably few colors, are known to admit efficient distributed randomized algorithms. Those algorithms essentially proceed according to some simple generic rules, by letting each node choosing a temptative value at random, and checking whether this choice is consistent with the choices of the nodes in its vicinity. If this is the case, then the node outputs the chosen value, else it repeats the same process. Although such algorithms are, with high probability, running in a polylogarithmic number of rounds, they are not robust against actions performed by rational but selfish nodes. Indeed, such nodes may prefer specific individual outputs over others, e.g., because the formers suit better with some individual constraints. For instance, a node may prefer not being placed in a MIS as it is not willing to serve as a relay node. Similarly, a node may prefer not being assigned some radio frequencies (i.e., colors) as these frequencies would interfere with other devices running at that node. In this paper, we show that the probability distribution governing the choices of the output values in the generic algorithm can be tuned such that no nodes will rationally deviate from this distribution. More formally, and more generally, we prove that the large class of so-called LCL tasks, including MIS and coloring, admit simple "Luby's style" algorithms where the probability distribution governing the individual choices of the output values forms a Nash equilibrium. In fact, we establish the existence of a stronger form of equilibria, called symmetric trembling-hand perfect equilibria for those games.
Cite as
Simon Collet, Pierre Fraigniaud, and Paolo Penna. Equilibria of Games in Networks for Local Tasks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{collet_et_al:LIPIcs.OPODIS.2018.6,
author = {Collet, Simon and Fraigniaud, Pierre and Penna, Paolo},
title = {{Equilibria of Games in Networks for Local Tasks}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {6:1--6: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.6},
URN = {urn:nbn:de:0030-drops-100668},
doi = {10.4230/LIPIcs.OPODIS.2018.6},
annote = {Keywords: Local distributed computing, Locally checkable labelings}
}
Document
The Sparsest Additive Spanner via Multiple Weighted BFS Trees
Abstract
Spanners are fundamental graph structures that sparsify graphs at the cost of small stretch. In particular, in recent years, many sequential algorithms constructing additive all-pairs spanners were designed, providing very sparse small-stretch subgraphs. Remarkably, it was then shown that the known (+6)-spanner constructions are essentially the sparsest possible, that is, larger additive stretch cannot guarantee a sparser spanner, which brought the stretch-sparsity trade-off to its limit. Distributed constructions of spanners are also abundant. However, for additive spanners, while there were algorithms constructing (+2) and (+4)-all-pairs spanners, the sparsest case of (+6)-spanners remained elusive.
We remedy this by designing a new sequential algorithm for constructing a (+6)-spanner with the essentially-optimal sparsity of O~(n^{4/3}) edges. We then show a distributed implementation of our algorithm, answering an open problem in [Keren Censor{-}Hillel et al., 2016].
A main ingredient in our distributed algorithm is an efficient construction of multiple weighted BFS trees. A weighted BFS tree is a BFS tree in a weighted graph, that consists of the lightest among all shortest paths from the root to each node. We present a distributed algorithm in the CONGEST model, that constructs multiple weighted BFS trees in |S|+D-1 rounds, where S is the set of sources and D is the diameter of the network graph.
Cite as
Keren Censor-Hillel, Ami Paz, and Noam Ravid. The Sparsest Additive Spanner via Multiple Weighted BFS Trees. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{censorhillel_et_al:LIPIcs.OPODIS.2018.7,
author = {Censor-Hillel, Keren and Paz, Ami and Ravid, Noam},
title = {{The Sparsest Additive Spanner via Multiple Weighted BFS Trees}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {7:1--7: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.7},
URN = {urn:nbn:de:0030-drops-100676},
doi = {10.4230/LIPIcs.OPODIS.2018.7},
annote = {Keywords: Distributed graph algorithms, congest model, weighted BFS trees, additive spanners}
}
Document
The Amortized Analysis of a Non-blocking Chromatic Tree
Abstract
A non-blocking chromatic tree is a type of balanced binary search tree where multiple processes can concurrently perform search and update operations. We prove that a certain implementation has amortized cost O(dot{c} + log n) for each operation, where dot{c} is the maximum number of concurrent operations at any point during the execution and n is the maximum number of keys in the tree during the operation. This amortized analysis presents new challenges compared to existing analyses of other non-blocking data structures.
Cite as
Jeremy Ko. The Amortized Analysis of a Non-blocking Chromatic Tree. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{ko:LIPIcs.OPODIS.2018.8,
author = {Ko, Jeremy},
title = {{The Amortized Analysis of a Non-blocking Chromatic Tree}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {8:1--8:17},
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.8},
URN = {urn:nbn:de:0030-drops-100688},
doi = {10.4230/LIPIcs.OPODIS.2018.8},
annote = {Keywords: amortized analysis, non-blocking, lock-free, balanced binary search trees}
}
Document
Lock-Free Search Data Structures: Throughput Modeling with Poisson Processes
Abstract
This paper considers the modeling and the analysis of the performance of lock-free concurrent search data structures. Our analysis considers such lock-free data structures that are utilized through a sequence of operations which are generated with a memoryless and stationary access pattern. Our main contribution is a new way of analyzing lock-free concurrent search data structures: our execution model matches with the behavior that we observe in practice and achieves good throughput predictions.
Search data structures are formed of basic blocks, usually referred to as nodes, which can be accessed by two kinds of events, characterized by their latencies; (i) CAS events originated as a result of modifications of the search data structure (ii) Read events that occur during traversals. An operation triggers a set of events, and the running time of an operation is computed as the sum of the latencies of these events. We identify the factors that impact the latency of such events on a multi-core shared memory system. The main challenge (though not the only one) is that the latency of each event mainly depends on the state of the caches at the time when it is triggered, and the state of caches is changing due to events that are triggered by the operations of any thread in the system. Accordingly, the latency of an event is determined by the ordering of the events on the timeline.
Search data structures are usually designed to accommodate a large number of nodes, which makes the occurrence of an event on a given node rare at any given time. In this context, we model the events on each node as Poisson processes from which we can extract the frequency and probabilistic ordering of events that are used to estimate the expected latency of an operation, and in turn the throughput. We have validated our analysis on several fundamental lock-free search data structures such as linked lists, hash tables, skip lists and binary trees.
Cite as
Aras Atalar, Paul Renaud-Goud, and Philippas Tsigas. Lock-Free Search Data Structures: Throughput Modeling with Poisson Processes. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{atalar_et_al:LIPIcs.OPODIS.2018.9,
author = {Atalar, Aras and Renaud-Goud, Paul and Tsigas, Philippas},
title = {{Lock-Free Search Data Structures: Throughput Modeling with Poisson Processes}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {9:1--9: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.9},
URN = {urn:nbn:de:0030-drops-100698},
doi = {10.4230/LIPIcs.OPODIS.2018.9},
annote = {Keywords: Lock-free, Search Data Structures, Performance, Modeling, Analysis}
}
Document
Concurrent Robin Hood Hashing
Abstract
In this paper we examine the issues involved in adding concurrency to the Robin Hood hash table algorithm. We present a non-blocking obstruction-free K-CAS Robin Hood algorithm which requires only a single word compare-and-swap primitive, thus making it highly portable. The implementation maintains the attractive properties of the original Robin Hood structure, such as a low expected probe length, capability to operate effectively under a high load factor and good cache locality, all of which are essential for high performance on modern computer architectures. We compare our data-structures to various other lock-free and concurrent algorithms, as well as a simple hardware transactional variant, and show that our implementation performs better across a number of contexts.
Cite as
Robert Kelly, Barak A. Pearlmutter, and Phil Maguire. Concurrent Robin Hood Hashing. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{kelly_et_al:LIPIcs.OPODIS.2018.10,
author = {Kelly, Robert and Pearlmutter, Barak A. and Maguire, Phil},
title = {{Concurrent Robin Hood Hashing}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {10:1--10: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.10},
URN = {urn:nbn:de:0030-drops-100701},
doi = {10.4230/LIPIcs.OPODIS.2018.10},
annote = {Keywords: concurrency, Robin Hood Hashing, data-structures, hash tables, non-blocking}
}
Document
Parallel Combining: Benefits of Explicit Synchronization
Abstract
A parallel batched data structure is designed to process synchronized batches of operations on the data structure using a parallel program. In this paper, we propose parallel combining, a technique that implements a concurrent data structure from a parallel batched one. The idea is that we explicitly synchronize concurrent operations into batches: one of the processes becomes a combiner which collects concurrent requests and initiates a parallel batched algorithm involving the owners (clients) of the collected requests. Intuitively, the cost of synchronizing the concurrent calls can be compensated by running the parallel batched algorithm.
We validate the intuition via two applications. First, we use parallel combining to design a concurrent data structure optimized for read-dominated workloads, taking a dynamic graph data structure as an example. Second, we use a novel parallel batched priority queue to build a concurrent one. In both cases, we obtain performance gains with respect to the state-of-the-art algorithms.
Cite as
Vitaly Aksenov, Petr Kuznetsov, and Anatoly Shalyto. Parallel Combining: Benefits of Explicit Synchronization. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{aksenov_et_al:LIPIcs.OPODIS.2018.11,
author = {Aksenov, Vitaly and Kuznetsov, Petr and Shalyto, Anatoly},
title = {{Parallel Combining: Benefits of Explicit Synchronization}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {11:1--11: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.11},
URN = {urn:nbn:de:0030-drops-100713},
doi = {10.4230/LIPIcs.OPODIS.2018.11},
annote = {Keywords: concurrent data structure, parallel batched data structure, combining}
}
Document
Specification and Implementation of Replicated List: The Jupiter Protocol Revisited
Abstract
The replicated list object is frequently used to model the core functionality of replicated collaborative text editing systems. Since 1989, the convergence property has been a common specification of a replicated list object. Recently, Attiya et al. proposed the strong/weak list specification and conjectured that the well-known Jupiter protocol satisfies the weak list specification. The major obstacle to proving this conjecture is the mismatch between the global property on all replica states prescribed by the specification and the local view each replica maintains in Jupiter using data structures like 1D buffer or 2D state space. To address this issue, we propose CJupiter (Compact Jupiter) based on a novel data structure called n-ary ordered state space for a replicated client/server system with n clients. At a high level, CJupiter maintains only a single n-ary ordered state space which encompasses exactly all states of each replica. We prove that CJupiter and Jupiter are equivalent and that CJupiter satisfies the weak list specification, thus solving the conjecture above.
Cite as
Hengfeng Wei, Yu Huang, and Jian Lu. Specification and Implementation of Replicated List: The Jupiter Protocol Revisited. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{wei_et_al:LIPIcs.OPODIS.2018.12,
author = {Wei, Hengfeng and Huang, Yu and Lu, Jian},
title = {{Specification and Implementation of Replicated List: The Jupiter Protocol Revisited}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {12:1--12: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.12},
URN = {urn:nbn:de:0030-drops-100720},
doi = {10.4230/LIPIcs.OPODIS.2018.12},
annote = {Keywords: Collaborative text editing systems, Replicated list, Concurrency control, Strong/weak list specification, Operational transformation, Jupiter protocol}
}
Document
Local Fast Segment Rerouting on Hypercubes
Abstract
Fast rerouting is an essential mechanism in any dependable communication network, allowing to quickly, i.e., locally, recover from network failures, without invoking the control plane. However, while locality ensures a fast reaction, the absence of global information also renders the design of highly resilient fast rerouting algorithms more challenging. In this paper, we study algorithms for fast rerouting in emerging Segment Routing (SR) networks, where intermediate destinations can be added to packets by nodes along the path. Our main contribution is a maximally resilient polynomial-time fast rerouting algorithm for SR networks based on a hypercube topology. Our algorithm is attractive as it preserves the original paths (and hence waypoints traversed along the way), and does not require packets to carry failure information. We complement our results with an integer linear program formulation for general graphs and exploratory simulation results.
Cite as
Klaus-Tycho Foerster, Mahmoud Parham, Stefan Schmid, and Tao Wen. Local Fast Segment Rerouting on Hypercubes. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{foerster_et_al:LIPIcs.OPODIS.2018.13,
author = {Foerster, Klaus-Tycho and Parham, Mahmoud and Schmid, Stefan and Wen, Tao},
title = {{Local Fast Segment Rerouting on Hypercubes}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {13:1--13:17},
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.13},
URN = {urn:nbn:de:0030-drops-100739},
doi = {10.4230/LIPIcs.OPODIS.2018.13},
annote = {Keywords: segment routing, local fast failover, link failures}
}
Document
Effects of Topology Knowledge and Relay Depth on Asynchronous Appoximate Consensus
Abstract
Consider a point-to-point message-passing network. We are interested in the asynchronous crash-tolerant consensus problem in incomplete networks. We study the feasibility and efficiency of approximate consensus under different restrictions on topology knowledge and the relay depth, i.e., the maximum number of hops any message can be relayed. These two constraints are common in large-scale networks, and are used to avoid memory overload and network congestion respectively. Specifically, for positive integer values k and k', we consider that each node knows all its neighbors of at most k-hop distance (k-hop topology knowledge), and the relay depth is k'. We consider both directed and undirected graphs. More concretely, we answer the following question in asynchronous systems: "What is a tight condition on the underlying communication graphs for achieving approximate consensus if each node has only a k-hop topology knowledge and relay depth k'?" To prove that the necessary conditions presented in the paper are also sufficient, we have developed algorithms that achieve consensus in graphs satisfying those conditions:
- The first class of algorithms requires k-hop topology knowledge and relay depth k. Unlike prior algorithms, these algorithms do not flood the network, and each node does not need the full topology knowledge. We show how the convergence time and the message complexity of those algorithms is affected by k, providing the respective upper bounds.
- The second set of algorithms requires only one-hop neighborhood knowledge, i.e., immediate incoming and outgoing neighbors, but needs to flood the network (i.e., relay depth is n, where n is the number of nodes). One result that may be of independent interest is a topology discovery mechanism to learn and "estimate" the topology in asynchronous directed networks with crash faults.
Cite as
Dimitris Sakavalas, Lewis Tseng, and Nitin H. Vaidya. Effects of Topology Knowledge and Relay Depth on Asynchronous Appoximate Consensus. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sakavalas_et_al:LIPIcs.OPODIS.2018.14,
author = {Sakavalas, Dimitris and Tseng, Lewis and Vaidya, Nitin H.},
title = {{Effects of Topology Knowledge and Relay Depth on Asynchronous Appoximate Consensus}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {14:1--14: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.14},
URN = {urn:nbn:de:0030-drops-100744},
doi = {10.4230/LIPIcs.OPODIS.2018.14},
annote = {Keywords: Asynchrony, crash, consensus, incomplete graphs, topology knowledge}
}
Document
Hybrid Fault-Tolerant Consensus in Asynchronous and Wireless Embedded Systems
Abstract
Byzantine fault-tolerant (BFT) consensus in an asynchronous system can only tolerate up to floor[(n-1)/3] faulty processes in a group of n processes. This is quite a strict limit in certain application scenarios, for example a group consisting of only 3 processes. In order to break through this limit, we can leverage a hybrid fault model, in which a subset of the system is enhanced and cannot be arbitrarily faulty except for crashing. Based on this model, we propose a randomized binary consensus algorithm that executes in complete asynchrony, rather than in partial synchrony required by deterministic algorithms. It can tolerate up to floor[(n-1)/2] Byzantine faulty processes as long as the trusted subsystem in each process is not compromised, and terminates with a probability of one. The algorithm is resilient against a strong adversary, i. e. the adversary is able to inspect the state of the whole system, manipulate the delay of every message and process, and then adjust its faulty behaviour during execution.
From a practical point of view, the algorithm is lightweight and has little dependency on lower level protocols or communication primitives. We evaluate the algorithm and the results show that it performs promisingly in a testbed consisting of up to 10 embedded devices connected via an ad hoc wireless network.
Cite as
Wenbo Xu, Signe Rüsch, Bijun Li, and Rüdiger Kapitza. Hybrid Fault-Tolerant Consensus in Asynchronous and Wireless Embedded Systems. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{xu_et_al:LIPIcs.OPODIS.2018.15,
author = {Xu, Wenbo and R\"{u}sch, Signe and Li, Bijun and Kapitza, R\"{u}diger},
title = {{Hybrid Fault-Tolerant Consensus in Asynchronous and Wireless Embedded Systems}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {15:1--15: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.15},
URN = {urn:nbn:de:0030-drops-100757},
doi = {10.4230/LIPIcs.OPODIS.2018.15},
annote = {Keywords: Distributed system, consensus, fault tolerance}
}
Document
Correctness of Tendermint-Core Blockchains
Abstract
Tendermint-core blockchains (e.g. Cosmos) are considered today one of the most viable alternatives for the highly energy consuming proof-of-work blockchains such as Bitcoin and Ethereum. Their particularity is that they aim at offering strong consistency (no forks) in an open system combining two ingredients (i) a set of validators that generate blocks via a variant of Practical Byzantine Fault Tolerant (PBFT) consensus protocol and (ii) a selection strategy that dynamically selects nodes to be validators for the next block via a proof-of-stake mechanism. The exact assumptions on the system model under which Tendermint underlying algorithms are correct and the exact properties Tendermint verifies, however, have never been formally analyzed. The contribution of this paper is as follows. First, while formalizing Tendermint algorithms we precisely characterize the system model and the exact problem solved by Tendermint, then, we prove that in eventual synchronous systems a modified version of Tendermint solves (i) under additional assumptions, a variant of one-shot consensus for the validation of one single block and (ii) a variant of the repeated consensus problem for multiple blocks. These results hold even if the set of validators is hit by Byzantine failures, provided that for each one-shot consensus instance less than one third of the validators is Byzantine.
Cite as
Yackolley Amoussou-Guenou, Antonella Del Pozzo, Maria Potop-Butucaru, and Sara Tucci-Piergiovanni. Correctness of Tendermint-Core Blockchains. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{amoussouguenou_et_al:LIPIcs.OPODIS.2018.16,
author = {Amoussou-Guenou, Yackolley and Del Pozzo, Antonella and Potop-Butucaru, Maria and Tucci-Piergiovanni, Sara},
title = {{Correctness of Tendermint-Core Blockchains}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {16:1--16: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.16},
URN = {urn:nbn:de:0030-drops-100764},
doi = {10.4230/LIPIcs.OPODIS.2018.16},
annote = {Keywords: Blockchain, Consensus, Proof-of-Stake, Fairness}
}
Document
Federated Byzantine Quorum Systems
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
Characterizing Asynchronous Message-Passing Models Through Rounds
Abstract
Message-passing models of distributed computing vary along numerous dimensions: degree of synchrony, kind of faults, number of faults... Unfortunately, the sheer number of models and their subtle distinctions hinder our ability to design a general theory of message-passing models. One way out of this conundrum restricts communication to proceed by round. A great variety of message-passing models can then be captured in the Heard-Of model, through predicates on the messages sent in a round and received during or before this round. Then, the issue is to find the most accurate Heard-Of predicate to capture a given model. This is straightforward in synchronous models, because waiting for the upper bound on communication delay ensures that all available messages are received, while not waiting forever. On the other hand, asynchrony allows unbounded message delays. Is there nonetheless a meaningful characterization of asynchronous models by a Heard-Of predicate?
We formalize this characterization by introducing Delivered collections: the collections of all messages delivered at each round, whether late or not. Predicates on Delivered collections capture message-passing models. The question is to determine which Heard-Of predicates can be generated by a given Delivered predicate. We answer this by formalizing strategies for when to change round. Thanks to a partial order on these strategies, we also find the "best" strategy for multiple models, where "best" intuitively means it waits for as many messages as possible while not waiting forever. Finally, a strategy for changing round that never blocks a process forever implements a Heard-Of predicate. This allows us to translate the order on strategies into an order on Heard-Of predicates. The characterizing predicate for a model is then the greatest element for that order, if it exists.
Cite as
Adam Shimi, Aurélie Hurault, and Philippe Quéinnec. Characterizing Asynchronous Message-Passing Models Through Rounds. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{shimi_et_al:LIPIcs.OPODIS.2018.18,
author = {Shimi, Adam and Hurault, Aur\'{e}lie and Qu\'{e}innec, Philippe},
title = {{Characterizing Asynchronous Message-Passing Models Through Rounds}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {18:1--18:17},
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.18},
URN = {urn:nbn:de:0030-drops-100783},
doi = {10.4230/LIPIcs.OPODIS.2018.18},
annote = {Keywords: Message-passing, Asynchronous Rounds, Dominant Strategies, Failures}
}
Document
You Only Live Multiple Times: A Blackbox Solution for Reusing Crash-Stop Algorithms In Realistic Crash-Recovery Settings
Abstract
Distributed agreement-based algorithms are often specified in a crash-stop asynchronous model augmented by Chandra and Toueg's unreliable failure detectors. In such models, correct nodes stay up forever, incorrect nodes eventually crash and remain down forever, and failure detectors behave correctly forever eventually, However, in reality, nodes as well as communication links both crash and recover without deterministic guarantees to remain in some state forever.
In this paper, we capture this realistic temporary and probabilitic behaviour in a simple new system model. Moreover, we identify a large algorithm class for which we devise a property-preserving transformation. Using this transformation, many algorithms written for the asynchronous crash-stop model run correctly and unchanged in real systems.
Cite as
David Kozhaya, Ognjen Maric, and Yvonne-Anne Pignolet. You Only Live Multiple Times: A Blackbox Solution for Reusing Crash-Stop Algorithms In Realistic Crash-Recovery Settings. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{kozhaya_et_al:LIPIcs.OPODIS.2018.19,
author = {Kozhaya, David and Maric, Ognjen and Pignolet, Yvonne-Anne},
title = {{You Only Live Multiple Times: A Blackbox Solution for Reusing Crash-Stop Algorithms In Realistic Crash-Recovery Settings}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {19:1--19:17},
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.19},
URN = {urn:nbn:de:0030-drops-100792},
doi = {10.4230/LIPIcs.OPODIS.2018.19},
annote = {Keywords: Crash recovery, consensus, asynchrony}
}
Document
Causal Broadcast: How to Forget?
Abstract
Causal broadcast constitutes a fundamental communication primitive of many distributed protocols and applications. However, state-of-the-art implementations fail to forget obsolete control information about already delivered messages. They do not scale in large and dynamic systems. In this paper, we propose a novel implementation of causal broadcast. We prove that all and only obsolete control information is safely removed, at cost of a few lightweight control messages. The local space complexity of this protocol does not monotonically increase and depends at each moment on the number of messages still in transit and the degree of the communication graph. Moreover, messages only carry a scalar clock. Our implementation constitutes a sustainable communication primitive for causal broadcast in large and dynamic systems.
Cite as
Brice Nédelec, Pascal Molli, and Achour Mostéfaoui. Causal Broadcast: How to Forget?. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{nedelec_et_al:LIPIcs.OPODIS.2018.20,
author = {N\'{e}delec, Brice and Molli, Pascal and Most\'{e}faoui, Achour},
title = {{Causal Broadcast: How to Forget?}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {20:1--20: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.20},
URN = {urn:nbn:de:0030-drops-100805},
doi = {10.4230/LIPIcs.OPODIS.2018.20},
annote = {Keywords: Causal broadcast, complexity trade-off, large and dynamic systems}
}
Document
Output-Oblivious Stochastic Chemical Reaction Networks
Abstract
We classify the functions f:N^2 -> N which are stably computable by output-oblivious Stochastic Chemical Reaction Networks (CRNs), i.e., systems of reactions in which output species are never reactants. While it is known that precisely the semilinear functions are stably computable by CRNs, such CRNs sometimes rely on initially producing too many output species, and then consuming the excess in order to reach a correct stable state. These CRNs may be difficult to integrate into larger systems: if the output of a CRN C becomes the input to a downstream CRN C', then C' could inadvertently consume too many outputs before C stabilizes. If, on the other hand, C is output-oblivious then C' may consume C's output as soon as it is available. In this work we prove that a semilinear function f:N^2 -> N is stably computable by an output-oblivious CRN with a leader if and only if it is both increasing and either grid-affine (intuitively, its domains are congruence classes), or the minimum of a finite set of fissure functions (intuitively, functions behaving like the min function).
Cite as
Ben Chugg, Hooman Hashemi, and Anne Condon. Output-Oblivious Stochastic Chemical Reaction Networks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{chugg_et_al:LIPIcs.OPODIS.2018.21,
author = {Chugg, Ben and Hashemi, Hooman and Condon, Anne},
title = {{Output-Oblivious Stochastic Chemical Reaction Networks}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {21:1--21: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.21},
URN = {urn:nbn:de:0030-drops-100815},
doi = {10.4230/LIPIcs.OPODIS.2018.21},
annote = {Keywords: Chemical Reaction Networks, Stable Function Computation, Output-Oblivious, Output-Monotonic}
}
Document
The Synergy of Finite State Machines
Abstract
What can be computed by a network of n randomized finite state machines communicating under the stone age model (Emek & Wattenhofer, PODC 2013)? The inherent linear upper bound on the total space of the network implies that its global computational power is not larger than that of a randomized linear space Turing machine, but is this tight? We answer this question affirmatively for bounded degree networks by introducing a stone age algorithm (operating under the most restrictive form of the model) that given a designated I/O node, constructs a tour in the network that enables the simulation of the Turing machine's tape. To construct the tour with high probability, we first show how to 2-hop color the network concurrently with building a spanning tree.
Cite as
Yehuda Afek, Yuval Emek, and Noa Kolikant. The Synergy of Finite State Machines. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{afek_et_al:LIPIcs.OPODIS.2018.22,
author = {Afek, Yehuda and Emek, Yuval and Kolikant, Noa},
title = {{The Synergy of Finite State Machines}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {22:1--22: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.22},
URN = {urn:nbn:de:0030-drops-100825},
doi = {10.4230/LIPIcs.OPODIS.2018.22},
annote = {Keywords: finite state machines, stone-age model, beeping communication scheme, distributed network computability}
}
Document
Task Computability in Unreliable Anonymous Networks
Abstract
We consider the anonymous broadcast model: a set of n anonymous processes communicate via send-to-all primitives. We assume that underlying communication channels are asynchronous but reliable, and that the processes are subject to crash failures. We show first that in this model, even a single faulty process precludes implementations of atomic objects with non-commuting operations, even as simple as read-write registers or add-only sets. We, however, show that a sequentially consistent read-write memory and add-only sets can be implemented t-resiliently for t<n/2, i.e., provided that a majority of the processes do not fail. We use this implementation to establish an equivalence between the t-resilient read-write anonymous shared-memory model and the t-resilient anonymous broadcast model in terms of colorless task solvability. As a result, we obtain the first task computability characterization for unreliable anonymous message-passing systems.
Cite as
Petr Kuznetsov and Nayuta Yanagisawa. Task Computability in Unreliable Anonymous Networks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 23:1-23:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{kuznetsov_et_al:LIPIcs.OPODIS.2018.23,
author = {Kuznetsov, Petr and Yanagisawa, Nayuta},
title = {{Task Computability in Unreliable Anonymous Networks}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {23:1--23:13},
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.23},
URN = {urn:nbn:de:0030-drops-100830},
doi = {10.4230/LIPIcs.OPODIS.2018.23},
annote = {Keywords: Distributed tasks, anonymous broadcast, fault-tolerance}
}
Document
Optimal Rendezvous L-Algorithms for Asynchronous Mobile Robots with External-Lights
Abstract
We study the Rendezvous problem for two autonomous mobile robots in asynchronous settings with persistent memory called light. It is well known that Rendezvous is impossible in a basic model when robots have no lights, even if the system is semi-synchronous. On the other hand, Rendezvous is possible if robots have lights of various types with a constant number of colors. If robots can observe not only their own lights but also other robots' lights, their lights are called full-light. If robots can only observe the state of other robots' lights, the lights are called external-light. This paper focuses on robots with external-lights in asynchronous settings and a particular class of algorithms called L-algorithms, where an L-algorithm computes a destination based only on the current colors of observable lights. When considering L-algorithms, Rendezvous can be solved by robots with full-lights and three colors in general asynchronous settings (called ASYNC) and the number of colors is optimal under these assumptions. In contrast, there exist no L-algorithms in ASYNC with external-lights regardless of the number of colors.
In this paper, extending the impossibility result, we show that there exist no L-algorithms in so-called LC-1-Bounded ASYNC with external-lights regardless of the number of colors, where LC-1-Bounded ASYNC is a proper subset of ASYNC and other robots can execute at most one Look operation between the Look operation of a robot and its subsequent Compute operation. We also show that LC-1-Bounded ASYNC is the minimal subclass in which no L-algorithms with external-lights exist. That is, Rendezvous can be solved by L-algorithms using external-lights with a finite number of colors in LC-0-Bounded ASYNC (equivalently LC-atomic ASYNC). Furthermore, we show that the algorithms are optimal in the number of colors they use.
Cite as
Takashi Okumura, Koichi Wada, and Xavier Défago. Optimal Rendezvous L-Algorithms for Asynchronous Mobile Robots with External-Lights. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{okumura_et_al:LIPIcs.OPODIS.2018.24,
author = {Okumura, Takashi and Wada, Koichi and D\'{e}fago, Xavier},
title = {{Optimal Rendezvous L-Algorithms for Asynchronous Mobile Robots with External-Lights}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {24:1--24: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.24},
URN = {urn:nbn:de:0030-drops-100843},
doi = {10.4230/LIPIcs.OPODIS.2018.24},
annote = {Keywords: Autonomous mobile robots, Rendezvous, Lights, L-algorithms}
}
Document
Linear Rendezvous with Asymmetric Clocks
Abstract
Two anonymous robots placed at different positions on an infinite line need to rendezvous. Each robot possesses a clock which it uses to time its movement. However, the robot's individual parameters in the form of their walking speed and time unit may or may not be the same for both robots. We study the feasibility of rendezvous in different scenarios, in which some subsets of these parameters are not the same. As the robots are anonymous, they execute the same algorithm and when both parameters are identical the rendezvous is infeasible. We propose a universal algorithm, such that the robots are assured of meeting in finite time, in any case when at least one of the parameters is not equal for both robots.
Cite as
Jurek Czyzowicz, Ryan Killick, and Evangelos Kranakis. Linear Rendezvous with Asymmetric Clocks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{czyzowicz_et_al:LIPIcs.OPODIS.2018.25,
author = {Czyzowicz, Jurek and Killick, Ryan and Kranakis, Evangelos},
title = {{Linear Rendezvous with Asymmetric Clocks}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {25:1--25: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.25},
URN = {urn:nbn:de:0030-drops-100855},
doi = {10.4230/LIPIcs.OPODIS.2018.25},
annote = {Keywords: anonymous, asymmetric clock, infinite line, rendezvous, mobile robot, speed, competitive ratio}
}
Document
Approximate Neighbor Counting in Radio Networks
Abstract
For many distributed algorithms, neighborhood size is an important parameter. In radio networks, however, obtaining this information can be difficult due to ad hoc deployments and communication that occurs on a collision-prone shared channel. This paper conducts a comprehensive survey of the approximate neighbor counting problem, which requires nodes to obtain a constant factor approximation of the size of their network neighborhood. We produce new lower and upper bounds for three main variations of this problem in the radio network model: (a) the network is single-hop and every node must obtain an estimate of its neighborhood size; (b) the network is multi-hop and only a designated node must obtain an estimate of its neighborhood size; and (c) the network is multi-hop and every node must obtain an estimate of its neighborhood size. In studying these problem variations, we consider solutions with and without collision detection, and with both constant and high success probability. Some of our results are extensions of existing strategies, while others require technical innovations. We argue this collection of results provides insight into the nature of this well-motivated problem (including how it differs from related symmetry breaking tasks in radio networks), and provides a useful toolbox for algorithm designers tackling higher level problems that might benefit from neighborhood size estimates.
Cite as
Calvin Newport and Chaodong Zheng. Approximate Neighbor Counting in Radio Networks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{newport_et_al:LIPIcs.OPODIS.2018.26,
author = {Newport, Calvin and Zheng, Chaodong},
title = {{Approximate Neighbor Counting in Radio Networks}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {26:1--26: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.26},
URN = {urn:nbn:de:0030-drops-100860},
doi = {10.4230/LIPIcs.OPODIS.2018.26},
annote = {Keywords: Radio networks, neighborhood size estimation, approximate counting}
}
Document
On Simple Back-Off in Unreliable Radio Networks
Abstract
In this paper, we study local and global broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local and global broadcast in the dual graph model. We also precisely characterize how this efficiency degrades as the new constraints are reduced down to non-existent, and prove new lower bounds that establish this degradation as near optimal for a large class of natural algorithms. We conclude with an analysis of a more general model where we propose an enhanced back-off algorithm. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.
Cite as
Seth Gilbert, Nancy Lynch, Calvin Newport, and Dominik Pajak. On Simple Back-Off in Unreliable Radio Networks. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{gilbert_et_al:LIPIcs.OPODIS.2018.27,
author = {Gilbert, Seth and Lynch, Nancy and Newport, Calvin and Pajak, Dominik},
title = {{On Simple Back-Off in Unreliable Radio Networks}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {27:1--27:17},
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.27},
URN = {urn:nbn:de:0030-drops-100877},
doi = {10.4230/LIPIcs.OPODIS.2018.27},
annote = {Keywords: radio networks, broadcast, unreliable links, distributed algorithm, robustness}
}
Document
Concurrent Specifications Beyond Linearizability
Abstract
With the advent of parallel architectures, distributed programs are used intensively and the question of how to formally specify the behaviors expected from such programs becomes crucial. A very general way to specify concurrent objects is to simply give the set of all the execution traces that we consider correct for the object. In many cases, one is only interested in studying a subclass of these concurrent specifications, and more convenient tools such as linearizability can be used to describe them.
In this paper, what we call a concurrent specification will be a set of execution traces that moreover satisfies a number of axioms. As we argue, these are actually the only concurrent specifications of interest: we prove that, in a reasonable computational model, every program satisfies all of our axioms. Restricting to this class of concurrent specifications allows us to formally relate our concurrent specifications with the ones obtained by linearizability, as well as its more recent variants (set- and interval-linearizability).
Cite as
Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent Specifications Beyond Linearizability. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{goubault_et_al:LIPIcs.OPODIS.2018.28,
author = {Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
title = {{Concurrent Specifications Beyond Linearizability}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {28:1--28: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.28},
URN = {urn:nbn:de:0030-drops-100888},
doi = {10.4230/LIPIcs.OPODIS.2018.28},
annote = {Keywords: concurrent specification, concurrent object, linearizability}
}
Document
Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings
Abstract
Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.
Cite as
Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour. Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{mirzaie_et_al:LIPIcs.OPODIS.2018.29,
author = {Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo},
title = {{Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {29:1--29:17},
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.29},
URN = {urn:nbn:de:0030-drops-100896},
doi = {10.4230/LIPIcs.OPODIS.2018.29},
annote = {Keywords: Parameterized synthesis, Self-stabilization, Formal methods}
}
Document
Loosely-Stabilizing Leader Election with Polylogarithmic Convergence Time
Abstract
A loosely-stabilizing leader election protocol with polylogarithmic convergence time in the population protocol model is presented in this paper. In the population protocol model, which is a common abstract model of mobile sensor networks, it is known to be impossible to design a self-stabilizing leader election protocol. Thus, in our prior work, we introduced the concept of loose-stabilization, which is weaker than self-stabilization but has similar advantage as self-stabilization in practice. Following this work, several loosely-stabilizing leader election protocols are presented. The loosely-stabilizing leader election guarantees that, starting from an arbitrary configuration, the system reaches a safe configuration with a single leader within a relatively short time, and keeps the unique leader for an sufficiently long time thereafter. The convergence times of all the existing loosely-stabilizing protocols, i.e., the expected time to reach a safe configuration, are polynomial in n where n is the number of nodes (while the holding times to keep the unique leader are exponential in n). In this paper, a loosely-stabilizing protocol with polylogarithmic convergence time is presented. Its holding time is not exponential, but arbitrarily large polynomial in n.
Cite as
Yuichi Sudo, Fukuhito Ooshita, Hirotsugu Kakugawa, Toshimitsu Masuzawa, Ajoy K. Datta, and Lawrence L. Larmore. Loosely-Stabilizing Leader Election with Polylogarithmic Convergence Time. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sudo_et_al:LIPIcs.OPODIS.2018.30,
author = {Sudo, Yuichi and Ooshita, Fukuhito and Kakugawa, Hirotsugu and Masuzawa, Toshimitsu and Datta, Ajoy K. and Larmore, Lawrence L.},
title = {{Loosely-Stabilizing Leader Election with Polylogarithmic Convergence Time}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {30:1--30: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.30},
URN = {urn:nbn:de:0030-drops-100901},
doi = {10.4230/LIPIcs.OPODIS.2018.30},
annote = {Keywords: Loose-stabilization, Population protocols, and Leader election}
}
Document
Self-Stabilizing Token Distribution with Constant-Space for Trees
Abstract
Self-stabilizing and silent distributed algorithms for token distribution in rooted tree networks are given. Initially, each process of a graph holds at most l tokens. Our goal is to distribute the tokens in the whole network so that every process holds exactly k tokens. In the initial configuration, the total number of tokens in the network may not be equal to nk where n is the number of processes in the network. The root process is given the ability to create a new token or remove a token from the network. We aim to minimize the convergence time, the number of token moves, and the space complexity. A self-stabilizing token distribution algorithm that converges within O(n l) asynchronous rounds and needs Theta(nh epsilon) redundant (or unnecessary) token moves is given, where epsilon = min(k,l-k) and h is the height of the tree network. Two novel ideas to reduce the number of redundant token moves are presented. One reduces the number of redundant token moves to O(nh) without any additional costs while the other reduces the number of redundant token moves to O(n), but increases the convergence time to O(nh l). All algorithms given have constant memory at each process and each link register.
Cite as
Yuichi Sudo, Ajoy K. Datta, Lawrence L. Larmore, and Toshimitsu Masuzawa. Self-Stabilizing Token Distribution with Constant-Space for Trees. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sudo_et_al:LIPIcs.OPODIS.2018.31,
author = {Sudo, Yuichi and Datta, Ajoy K. and Larmore, Lawrence L. and Masuzawa, Toshimitsu},
title = {{Self-Stabilizing Token Distribution with Constant-Space for Trees}},
booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
pages = {31:1--31: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.31},
URN = {urn:nbn:de:0030-drops-100918},
doi = {10.4230/LIPIcs.OPODIS.2018.31},
annote = {Keywords: token distribution, self-stabilization, constant-space algorithm}
}