eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
0
0
10.4230/LIPIcs.OPODIS.2018
article
LIPIcs, Volume 125, OPODIS'18, Complete Volume
Cao, Jiannong
Ellen, Faith
Rodrigues, Luis
Ferreira, Bernardo
LIPIcs, Volume 125, OPODIS'18, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018/LIPIcs.OPODIS.2018.pdf
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,
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
0:i
0:xx
10.4230/LIPIcs.OPODIS.2018.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Cao, Jiannong
Ellen, Faith
Rodrigues, Luis
Ferreira, Bernardo
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.0/LIPIcs.OPODIS.2018.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
1:1
1:1
10.4230/LIPIcs.OPODIS.2018.1
article
Complexity of Multi-Valued Register Simulations: A Retrospective (Keynote)
Welch, Jennifer L.
1
Department of Computer Science and Engineering, Texas A&M University, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.1/LIPIcs.OPODIS.2018.1.pdf
Distributed Systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
2:1
2:1
10.4230/LIPIcs.OPODIS.2018.2
article
Distributed Systems and Databases of the Globe Unite! The Cloud, the Edge and Blockchains (Keynote)
Abbadi, Amr El
1
Department of Computer Science, University of California, Santa Barbara, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.2/LIPIcs.OPODIS.2018.2.pdf
Consensus
Commitment
Cloud
Edge Computing
Blockchain
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
3:1
3:1
10.4230/LIPIcs.OPODIS.2018.3
article
How to Make Decisions (Optimally) (Keynote)
Sen, Siddhartha
1
Microsoft Research New York City, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.3/LIPIcs.OPODIS.2018.3.pdf
reinforcement learning
distributed systems
counterfactual evaluation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
4:1
4:17
10.4230/LIPIcs.OPODIS.2018.4
article
Sparse Matrix Multiplication and Triangle Listing in the Congested Clique Model
Censor-Hillel, Keren
1
Leitersdorf, Dean
1
Turner, Elia
1
Department of Computer Science, Technion, Israel
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].
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.4/LIPIcs.OPODIS.2018.4.pdf
congested clique
matrix multiplication
triangle listing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
5:1
5:16
10.4230/LIPIcs.OPODIS.2018.5
article
Large-Scale Distributed Algorithms for Facility Location with Outliers
Inamdar, Tanmay
1
Pai, Shreyas
1
Pemmaraju, Sriram V.
1
Department of Computer Science, The University of Iowa, Iowa, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.5/LIPIcs.OPODIS.2018.5.pdf
Distributed Algorithms
Clustering with Outliers
Metric Facility Location
Massively Parallel Computation
k-machine model
Congested Clique
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
6:1
6:16
10.4230/LIPIcs.OPODIS.2018.6
article
Equilibria of Games in Networks for Local Tasks
Collet, Simon
1
Fraigniaud, Pierre
1
Penna, Paolo
2
CNRS and University Paris Diderot, France
ETH Zurich, Switzerland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.6/LIPIcs.OPODIS.2018.6.pdf
Local distributed computing
Locally checkable labelings
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
7:1
7:16
10.4230/LIPIcs.OPODIS.2018.7
article
The Sparsest Additive Spanner via Multiple Weighted BFS Trees
Censor-Hillel, Keren
1
Paz, Ami
2
Ravid, Noam
1
Department of Computer Science, Technion, Haifa, Israel
IRIF, CNRS and Paris Diderot University, Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.7/LIPIcs.OPODIS.2018.7.pdf
Distributed graph algorithms
congest model
weighted BFS trees
additive spanners
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
8:1
8:17
10.4230/LIPIcs.OPODIS.2018.8
article
The Amortized Analysis of a Non-blocking Chromatic Tree
Ko, Jeremy
1
Department of Computer Science, University of Toronto, Canada
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.8/LIPIcs.OPODIS.2018.8.pdf
amortized analysis
non-blocking
lock-free
balanced binary search trees
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
9:1
9:16
10.4230/LIPIcs.OPODIS.2018.9
article
Lock-Free Search Data Structures: Throughput Modeling with Poisson Processes
Atalar, Aras
1
Renaud-Goud, Paul
2
Tsigas, Philippas
1
Chalmers University of Technology, S-41296 Göteborg, Sweden
Informatics Research Institute of Toulouse, F-31062 Toulouse, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.9/LIPIcs.OPODIS.2018.9.pdf
Lock-free
Search Data Structures
Performance
Modeling
Analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
10:1
10:16
10.4230/LIPIcs.OPODIS.2018.10
article
Concurrent Robin Hood Hashing
Kelly, Robert
1
https://orcid.org/0000-0001-8266-2961
Pearlmutter, Barak A.
2
https://orcid.org/0000-0003-0521-4553
Maguire, Phil
1
https://orcid.org/0000-0002-8993-8403
Maynooth University Department of Computer Science, Maynooth, Ireland
Maynooth University Department of Computer Science and Hamilton Institute, Maynooth, Ireland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.10/LIPIcs.OPODIS.2018.10.pdf
concurrency
Robin Hood Hashing
data-structures
hash tables
non-blocking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
11:1
11:16
10.4230/LIPIcs.OPODIS.2018.11
article
Parallel Combining: Benefits of Explicit Synchronization
Aksenov, Vitaly
1
Kuznetsov, Petr
2
Shalyto, Anatoly
3
ITMO University, Saint-Petersburg, Russia and Inria, Paris, France
LTCI, Télécom ParisTech, Université Paris-Saclay, Paris, France
ITMO University, Saint-Petersburg, Russia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.11/LIPIcs.OPODIS.2018.11.pdf
concurrent data structure
parallel batched data structure
combining
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
12:1
12:16
10.4230/LIPIcs.OPODIS.2018.12
article
Specification and Implementation of Replicated List: The Jupiter Protocol Revisited
Wei, Hengfeng
1
Huang, Yu
1
Lu, Jian
1
State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.12/LIPIcs.OPODIS.2018.12.pdf
Collaborative text editing systems
Replicated list
Concurrency control
Strong/weak list specification
Operational transformation
Jupiter protocol
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
13:1
13:17
10.4230/LIPIcs.OPODIS.2018.13
article
Local Fast Segment Rerouting on Hypercubes
Foerster, Klaus-Tycho
1
https://orcid.org/0000-0003-4635-4480
Parham, Mahmoud
1
https://orcid.org/0000-0002-6211-077X
Schmid, Stefan
1
https://orcid.org/0000-0002-7798-1711
Wen, Tao
2
https://orcid.org/0000-0002-0772-5296
University of Vienna, Vienna, Austria
University of Electronic Science and Technology of China, Chengdu, China
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.13/LIPIcs.OPODIS.2018.13.pdf
segment routing
local fast failover
link failures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
14:1
14:16
10.4230/LIPIcs.OPODIS.2018.14
article
Effects of Topology Knowledge and Relay Depth on Asynchronous Appoximate Consensus
Sakavalas, Dimitris
1
Tseng, Lewis
1
Vaidya, Nitin H.
2
Boston College, USA
Georgetown University, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.14/LIPIcs.OPODIS.2018.14.pdf
Asynchrony
crash
consensus
incomplete graphs
topology knowledge
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
15:1
15:16
10.4230/LIPIcs.OPODIS.2018.15
article
Hybrid Fault-Tolerant Consensus in Asynchronous and Wireless Embedded Systems
Xu, Wenbo
1
Rüsch, Signe
1
Li, Bijun
1
Kapitza, Rüdiger
1
Technische Universität Braunschweig, Braunschweig, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.15/LIPIcs.OPODIS.2018.15.pdf
Distributed system
consensus
fault tolerance
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
16:1
16:16
10.4230/LIPIcs.OPODIS.2018.16
article
Correctness of Tendermint-Core Blockchains
Amoussou-Guenou, Yackolley
1
Del Pozzo, Antonella
2
Potop-Butucaru, Maria
3
Tucci-Piergiovanni, Sara
2
Institut LIST, CEA, Université Paris-Saclay, F-91120, Palaiseau, France , Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, F-75005 Paris, France
Institut LIST, CEA, Université Paris-Saclay, F-91120, Palaiseau, France
Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, F-75005 Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.16/LIPIcs.OPODIS.2018.16.pdf
Blockchain
Consensus
Proof-of-Stake
Fairness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
17:1
17:16
10.4230/LIPIcs.OPODIS.2018.17
article
Federated Byzantine Quorum Systems
García-Pérez, Álvaro
1
Gotsman, Alexey
1
IMDEA Software Institute, Madrid, Spain
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.17/LIPIcs.OPODIS.2018.17.pdf
Blockchain
Stellar
Byzantine quorum systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
18:1
18:17
10.4230/LIPIcs.OPODIS.2018.18
article
Characterizing Asynchronous Message-Passing Models Through Rounds
Shimi, Adam
1
Hurault, Aurélie
1
Quéinnec, Philippe
1
IRIT - Université de Toulouse, 2 rue Camichel, F-31000 Toulouse, France, http://www.irit.fr
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.18/LIPIcs.OPODIS.2018.18.pdf
Message-passing
Asynchronous Rounds
Dominant Strategies
Failures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
19:1
19:17
10.4230/LIPIcs.OPODIS.2018.19
article
You Only Live Multiple Times: A Blackbox Solution for Reusing Crash-Stop Algorithms In Realistic Crash-Recovery Settings
Kozhaya, David
1
Maric, Ognjen
2
Pignolet, Yvonne-Anne
1
ABB Corporate Research, Switzerland
Digital Asset, Switzerland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.19/LIPIcs.OPODIS.2018.19.pdf
Crash recovery
consensus
asynchrony
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
20:1
20:16
10.4230/LIPIcs.OPODIS.2018.20
article
Causal Broadcast: How to Forget?
Nédelec, Brice
1
Molli, Pascal
1
Mostéfaoui, Achour
1
LS2N, University of Nantes, 2 rue de la Houssinière, BP 92208, 44322 Nantes Cedex 3, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.20/LIPIcs.OPODIS.2018.20.pdf
Causal broadcast
complexity trade-off
large and dynamic systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
21:1
21:16
10.4230/LIPIcs.OPODIS.2018.21
article
Output-Oblivious Stochastic Chemical Reaction Networks
Chugg, Ben
1
Hashemi, Hooman
1
Condon, Anne
1
https://orcid.org/0000-0003-1458-1259
The University of British Columbia, Canada
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.21/LIPIcs.OPODIS.2018.21.pdf
Chemical Reaction Networks
Stable Function Computation
Output-Oblivious
Output-Monotonic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
22:1
22:16
10.4230/LIPIcs.OPODIS.2018.22
article
The Synergy of Finite State Machines
Afek, Yehuda
1
Emek, Yuval
2
Kolikant, Noa
1
Tel Aviv University, Tel Aviv, Israel
Technion - Israel Institute of Technology, Haifa, Israel
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.22/LIPIcs.OPODIS.2018.22.pdf
finite state machines
stone-age model
beeping communication scheme
distributed network computability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
23:1
23:13
10.4230/LIPIcs.OPODIS.2018.23
article
Task Computability in Unreliable Anonymous Networks
Kuznetsov, Petr
1
Yanagisawa, Nayuta
2
LTCI, Télécom ParisTec, Université Paris-Saclay, France
DeNA Co., Ltd., Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.23/LIPIcs.OPODIS.2018.23.pdf
Distributed tasks
anonymous broadcast
fault-tolerance
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
24:1
24:16
10.4230/LIPIcs.OPODIS.2018.24
article
Optimal Rendezvous L-Algorithms for Asynchronous Mobile Robots with External-Lights
Okumura, Takashi
1
Wada, Koichi
2
Défago, Xavier
3
https://orcid.org/0000-0002-2377-205X
Graduate School of Science and Engineering, Hosei University, Tokyo, 184-8485, Japan
Faculty of Science and Engineering, Hosei University, Tokyo, 184-8485, Japan, http://ai.k.hosei.ac.jp/staff/wada
School of Computing, Tokyo Institute of Technology, Tokyo, Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.24/LIPIcs.OPODIS.2018.24.pdf
Autonomous mobile robots
Rendezvous
Lights
L-algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
25:1
25:16
10.4230/LIPIcs.OPODIS.2018.25
article
Linear Rendezvous with Asymmetric Clocks
Czyzowicz, Jurek
1
Killick, Ryan
2
Kranakis, Evangelos
2
Département d'informatique, Université du Québec en Outaouais, Gatineau, Canada
School of Computer Science, Carleton University, Ottawa, Canada
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.25/LIPIcs.OPODIS.2018.25.pdf
anonymous
asymmetric clock
infinite line
rendezvous
mobile robot
speed
competitive ratio
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
26:1
26:16
10.4230/LIPIcs.OPODIS.2018.26
article
Approximate Neighbor Counting in Radio Networks
Newport, Calvin
1
Zheng, Chaodong
2
Georgetown University, Washington, D.C., United States
State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.26/LIPIcs.OPODIS.2018.26.pdf
Radio networks
neighborhood size estimation
approximate counting
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
27:1
27:17
10.4230/LIPIcs.OPODIS.2018.27
article
On Simple Back-Off in Unreliable Radio Networks
Gilbert, Seth
1
Lynch, Nancy
2
Newport, Calvin
3
Pajak, Dominik
2
National University of Singapore, Singapore
MIT, Cambridge, MA, USA
Georgetown University, Washington, DC, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.27/LIPIcs.OPODIS.2018.27.pdf
radio networks
broadcast
unreliable links
distributed algorithm
robustness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
28:1
28:16
10.4230/LIPIcs.OPODIS.2018.28
article
Concurrent Specifications Beyond Linearizability
Goubault, Éric
1
Ledent, Jérémy
1
Mimram, Samuel
1
École Polytechnique, Palaiseau, France
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.28/LIPIcs.OPODIS.2018.28.pdf
concurrent specification
concurrent object
linearizability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
29:1
29:17
10.4230/LIPIcs.OPODIS.2018.29
article
Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings
Mirzaie, Nahal
1
Faghih, Fathiyeh
1
Jacobs, Swen
2
https://orcid.org/0000-0002-9051-4050
Bonakdarpour, Borzoo
3
https://orcid.org/0000-0003-1800-5419
University of Tehran, North Kargar St., Tehran, Iran
CISPA Helmholtz Center i.G., Saarbrücken, Germany
Iowa State University, 207 Atanasoff Hall, Ames, IA 50011, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.29/LIPIcs.OPODIS.2018.29.pdf
Parameterized synthesis
Self-stabilization
Formal methods
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
30:1
30:16
10.4230/LIPIcs.OPODIS.2018.30
article
Loosely-Stabilizing Leader Election with Polylogarithmic Convergence Time
Sudo, Yuichi
1
Ooshita, Fukuhito
2
Kakugawa, Hirotsugu
1
Masuzawa, Toshimitsu
1
Datta, Ajoy K.
3
Larmore, Lawrence L.
3
Graduate School of Information Science and Technology, Osaka University, Japan
Graduate School of Science and Technology, Nara Institute of Science and Technology, Japan
Department of Computer Science, University of Nevada, Las Vegas, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.30/LIPIcs.OPODIS.2018.30.pdf
Loose-stabilization
Population protocols
and Leader election
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-15
125
31:1
31:16
10.4230/LIPIcs.OPODIS.2018.31
article
Self-Stabilizing Token Distribution with Constant-Space for Trees
Sudo, Yuichi
1
Datta, Ajoy K.
2
Larmore, Lawrence L.
2
Masuzawa, Toshimitsu
1
Graduate School of Information Science and Technology, Osaka University, Japan
Department of Computer Science, University of Nevada, Las Vegas, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol125-opodis2018/LIPIcs.OPODIS.2018.31/LIPIcs.OPODIS.2018.31.pdf
token distribution
self-stabilization
constant-space algorithm