eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
0
0
10.4230/LIPIcs.OPODIS.2017
article
LIPIcs, Volume 95, OPODIS'17, Complete Volume
Aspnes, James
Bessani, Alysson
Felber, Pascal
Leitão, João
LIPIcs, Volume 95, OPODIS'17, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017/LIPIcs.OPODIS.2017.pdf
Distributed Systems, Performance of Systems, Concurrent Programming, Data Structures, Modes of Computation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
0:i
0:xx
10.4230/LIPIcs.OPODIS.2017.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Aspnes, James
Bessani, Alysson
Felber, Pascal
Leitão, João
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.0/LIPIcs.OPODIS.2017.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
2018-03-28
95
1:1
1:1
10.4230/LIPIcs.OPODIS.2017.1
article
Causality for the Masses: Offering Fresh Data, Low Latency, and High Throughput
Rodrigues, Luís
The problem of ensuring consistency in applications that manage replicated data is one of the main challenges of distributed computing. Among the several invariants that may be enforced, ensuring that updates are applied and made visible respecting causality has emerged as a key ingredient among the many consistency criteria and client session guarantees that have been proposed and implemented in the last decade.
Techniques to keep track of causal dependencies, and to subsequently ensure that messages are delivered in causal order, have been widely studied. It is today well known that, in order to accurately capture causality one may need to keep a large amounts of metadata, for instance, one vector clock for each data object. This metadata needs to be updated and piggybacked on update messages, such that updates that are received from remote datacenters can be applied locally without violating causality. This metadata can be compressed; ultimately, it is possible to preserve causal order using a single scalar as metadata, i.e., a Lamport’s clock. Unfortunately, when compressing metadada it may become impossible to distinguish if two events are concurrent or causally related. We denote such scenario a false dependency. False dependencies introduce unnecessary delays and impair the latency of update propagation. This problem is exacerbated when one wants to support partial replication.
Therefore, when building a geo-replicated large-scale system one is faced with a dilemma: one can use techniques that maintain few metadata and that fail to capture causality accurately, or one can use techniques that require large metadata (to be kept and exchanged) but have precise information about which updates are concurrent. The former usually offer good throughput at the cost of latency, while the latter offer lower latencies sacrificing throughput. This talk reports on Saturn[1] and Eunomia[2], two complementary systems that break this tradeoff by providing simultaneously high-throughput and low latency, even in face of partial replication. The key ingredient to the success of our approach is to decouple the metadata path from the data path and to serialize concurrent events (to reduce metadata), in the metadata path, in a way that minimizes the impact on the latency perceived by clients.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.1/LIPIcs.OPODIS.2017.1.pdf
Distributed Systems
Causal Consistency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
2:1
2:13
10.4230/LIPIcs.OPODIS.2017.2
article
piChain: When a Blockchain meets Paxos
Burchert, Conrad
Wattenhofer, Roger
We present a new fault-tolerant distributed state machine to inherit the best features of its “parents in spirit”: Paxos, providing strong consistency, and a blockchain, providing simplicity and availability. Our proposal is simple as it does not include any heavy weight distributed failure handling protocols such as leader election. In addition, our proposal has a few other valuable features, e.g., it is responsive, it scales well, and it does not send any overhead messages.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.2/LIPIcs.OPODIS.2017.2.pdf
Consensus
Crash Failures
Availability
Network Partition
Consistency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
3:1
3:21
10.4230/LIPIcs.OPODIS.2017.3
article
Broadcasting in an Unreliable SINR Model
Kuhn, Fabian
Schneider, Philipp
We investigate distributed algorithms for broadcasting in unreliable wireless networks. Our basic setting is the signal to noise and interference ratio (SINR) model, which captures the physical key characteristics of wireless communication. We consider a dynamic variant of this model in which an adversary can adaptively control the model parameters for each individual transmission. Moreover, we assume that the network devices have no information about the geometry or the topology of the network and do neither know the exact model parameters nor do they have any control over them.
Our model is intended to capture the inherently unstable and unreliable nature of real wireless transmission, where signal quality and reception depends on many different aspects that are often hard to measure or predict. We show that with moderate adaptations, the broadcast algorithm of Daum et al. [DISC 13] also works in such an adversarial, much more dynamic setting. The algorithm allows to broadcast a single message in a network of size n in time O(D·polylog(n+R)), where D is the diameter and R describes the granularity of the communication graph.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.3/LIPIcs.OPODIS.2017.3.pdf
radio networks
wireless networks
broadcast
SINR model
unreliable communication
dynamic networks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
4:1
4:16
10.4230/LIPIcs.OPODIS.2017.4
article
Deterministic Subgraph Detection in Broadcast CONGEST
Korhonen, Janne H.
Rybicki, Joel
We present simple deterministic algorithms for subgraph finding and enumeration in the broadcast CONGEST model of distributed computation:
- For any constant k, detecting k-paths and trees on k nodes can be done in O(1) rounds.
- For any constant k, detecting k-cycles and pseudotrees on k nodes can be done in O(n)
rounds.
- On d-degenerate graphs, cliques and 4-cycles can be enumerated in O(d + log n) rounds, and
5-cycles in O(d2 + log n) rounds.
In many cases, these bounds are tight up to logarithmic factors. Moreover, we show that the algorithms for d-degenerate graphs can be improved to O(d/logn) and O(d2/logn), respect- ively, in the supported CONGEST model, which can be seen as an intermediate model between CONGEST and the congested clique.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.4/LIPIcs.OPODIS.2017.4.pdf
distributed computing
subgraph detection
CONGEST model
lower bounds
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
5:1
5:19
10.4230/LIPIcs.OPODIS.2017.5
article
Distributed Distance-Bounded Network Design Through Distributed Convex Programming
Dinitz, Michael
Nazari, Yasamin
Solving linear programs is often a challenging task in distributed settings. While there are good algorithms for solving packing and covering linear programs in a distributed manner (Kuhn et al. 2006), this is essentially the only class of linear programs for which such an algorithm is known. In this work we provide a distributed algorithm for solving a different class of convex programs which we call “distance-bounded network design convex programs”. These can be thought of as relaxations of network design problems in which the connectivity requirement includes a distance constraint (most notably, graph spanners). Our algorithm runs in O((D/ε) log n) rounds in the LOCAL model and with high probability finds a (1+ε)-approximation to the optimal LP solution for any 0 < ε ≤ 1, where D is the largest distance constraint.
While solving linear programs in a distributed setting is interesting in its own right, this class of convex programs is particularly important because solving them is often a crucial step when designing approximation algorithms. Hence we almost immediately obtain new and improved distributed approximation algorithms for a variety of network design problems, including Basic 3- and 4-Spanner, Directed k-Spanner, Lowest Degree k-Spanner, and Shallow-Light Steiner Network Design with a spanning demand graph. Our algorithms do not require any “heavy” computation and essentially match the best-known centralized approximation algorithms, while previous approaches which do not use heavy computation give approximations which are worse than the best-known centralized bounds.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.5/LIPIcs.OPODIS.2017.5.pdf
distributed algorithms
approximation algorithms
convex programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
6:1
6:16
10.4230/LIPIcs.OPODIS.2017.6
article
Lower Bounds for Subgraph Detection in the CONGEST Model
Gonen, Tzlil
Oshman, Rotem
In the subgraph-freeness problem, we are given a constant-sized graph H, and wish to de- termine whether the network graph contains H as a subgraph or not. Until now, the only lower bounds on subgraph-freeness known for the CONGEST model were for cycles of length greater than 3; here we extend and generalize the cycle lower bound, and obtain polynomial lower bounds for subgraph-freeness in the CONGEST model for two classes of subgraphs.
The first class contains any graph obtained by starting from a 2-connected graph H for which we already know a lower bound, and replacing the vertices of H by arbitrary connected graphs. We show that the lower bound on H carries over to the new graph. The second class is constructed by starting from a cycle Ck of length k ≥ 4, and constructing a graph H ̃ from Ck by replacing each edge {i, (i + 1) mod k} of the cycle with a connected graph Hi, subject to some constraints on the graphs H_{0}, . . . , H_{k−1}. In this case we obtain a polynomial lower bound for the new graph H ̃, depending on the size of the shortest cycle in H ̃ passing through the vertices of the original k-cycle.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.6/LIPIcs.OPODIS.2017.6.pdf
subgraph freeness
CONGEST
lower bounds
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
7:1
7:17
10.4230/LIPIcs.OPODIS.2017.7
article
Extending Transactional Memory with Atomic Deferral
Zhou, Tingzhe
Luchangco, Victor
Spear, Michael
This paper introduces atomic deferral, an extension to TM that allows programmers to move long-running or irrevocable operations out of a transaction while maintaining serializability: the transaction and its de- ferred operation appear to execute atomically from the perspective of other transactions. Thus, program- mers can adapt lock-based programs to exploit TM with relatively little effort and without sacrificing scalability by atomically deferring the problematic operations. We demonstrate this with several use cases for atomic deferral, as well as an in-depth analysis of its use on the PARSEC dedup benchmark, where we show that atomic deferral enables TM to be competitive with well-designed lock-based code.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.7/LIPIcs.OPODIS.2017.7.pdf
Transactional Memory
Concurrency
Synchronization
I/O
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
8:1
8:17
10.4230/LIPIcs.OPODIS.2017.8
article
Lock Oscillation: Boosting the Performance of Concurrent Data Structures
Fatourou, Panagiota
Kallimanis, Nikolaos D.
In combining-based synchronization, two main parameters that affect performance are the com- bining degree of the synchronization algorithm, i.e. the average number of requests that each com- biner serves, and the number of expensive synchronization primitives (like CAS, Swap, etc.) that it performs. The value of the first parameter must be high, whereas the second must be kept low.
In this paper, we present Osci, a new combining technique that shows remarkable perform- ance when paired with cheap context switching. We experimentally show that Osci significantly outperforms all previous combining algorithms. Specifically, the throughput of Osci is higher than that of previously presented combining techniques by more than an order of magnitude. Notably, Osci’s throughput is much closer to the ideal than all previous algorithms, while keep- ing the average latency in serving each request low. We evaluated the performance of Osci in two different multiprocessor architectures, namely AMD and Intel.
Based on Osci, we implement and experimentally evaluate implementations of concurrent queues and stacks. These implementations outperform by far all current state-of-the-art concur- rent queue and stack implementations. Although the current version of Osci has been evaluated in an environment supporting user-level threads, it would run correctly on any threading library, preemptive or not (including kernel threads).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.8/LIPIcs.OPODIS.2017.8.pdf
Synchronization
concurrent data structures
combining
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
9:1
9:17
10.4230/LIPIcs.OPODIS.2017.9
article
Progress-Space Tradeoffs in Single-Writer Memory Implementations
Imbs, Damien
Kuznetsov, Petr
Rieutord, Thibault
Many algorithms designed for shared-memory distributed systems assume the single-writer multi- reader (SWMR) setting where each process is provided with a unique register that can only be written by the process and read by all. In a system where computation is performed by a bounded number n of processes coming from a large (possibly unbounded) set of potential participants, the assumption of an SWMR memory is no longer reasonable. If only a bounded number of multi- writer multi-reader (MWMR) registers are provided, we cannot rely on an a priori assignment of processes to registers. In this setting, implementing an SWMR memory, or equivalently, ensuring stable writes (i.e., every written value persists in the memory), is desirable.
In this paper, we propose an SWMR implementation that adapts the number of MWMR registers used to the desired progress condition. For any given k from 1 to n, we present an algorithm that uses n + k − 1 registers to implement a k-lock-free SWMR memory. In the special case of 2-lock-freedom, we also give a matching lower bound of n + 1 registers, which supports our conjecture that the algorithm is space-optimal. Our lower bound holds for the strictly weaker progress condition of 2-obstruction-freedom, which suggests that the space complexity for k-obstruction-free and k-lock-free SWMR implementations might coincide.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.9/LIPIcs.OPODIS.2017.9.pdf
Single-writer memory implementation
comparison-based algorithms
space complexity
progress conditions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
10:1
10:16
10.4230/LIPIcs.OPODIS.2017.10
article
The Teleportation Design Pattern for Hardware Transactional Memory
Cohen, Nachshon
Herlihy, Maurice
Petrank, Erez
Wald, Elias
We identify a design pattern for concurrent data structures, called teleportation, that uses best- effort hardware transactional memory to speed up certain kinds of legacy concurrent data struc- tures. Teleportation unifies and explains several existing data structure designs, and it serves as the basis for novel approaches to reducing the memory traffic associated with fine-grained locking, and with hazard pointer management for memory reclamation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.10/LIPIcs.OPODIS.2017.10.pdf
Hardware transactional memory
concurrent data structures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
11:1
11:16
10.4230/LIPIcs.OPODIS.2017.11
article
Evacuating an Equilateral Triangle in the Face-to-Face Model
Chuangpishit, Huda
Mehrabi, Saeed
Narayanan, Lata
Opatrny, Jaroslav
Consider k robots initially located at the centroid of an equilateral triangle T of sides of length one. The goal of the robots is to evacuate T through an exit at an unknown location on the boundary of T. Each robot can move anywhere in T independently of other robots with maximum speed one. The objective is to minimize the evacuation time, which is defined as the time required for all k robots to reach the exit. We consider the face-to-face communication model for the robots: a robot can communicate with another robot only when they meet in T.
In this paper, we give upper and lower bounds for the face-to-face evacuation time by k robots. We show that for any k, any algorithm for evacuating k >= 1 robots from T requires at least sqrt(3) time. This bound is asymptotically optimal, as we show that a straightforward strategy of evacuation by k robots gives an upper bound of sqrt(3) + 3/k. For k = 3, 4, 5, 6, we
show significant improvements on the obvious upper bound by giving algorithms with evacuation times of 2.0887, 1.9816, 1.876, and 1.827, respectively. For k = 2 robots, we give a lower bound of 1 + 2/sqrt(3) ~= 2.154, and an algorithm with upper bound of 2.3367 on the evacuation time.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.11/LIPIcs.OPODIS.2017.11.pdf
Distributed algorithms
Robots evacuation
Face-to-face communication
Equilateral triangle
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
12:1
12:16
10.4230/LIPIcs.OPODIS.2017.12
article
Model Checking of Robot Gathering
Doan, Ha Thi Thu
Bonnet, François
Ogata, Kazuhiro
Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.12/LIPIcs.OPODIS.2017.12.pdf
Mobile Robot
Robot Gathering
Formal Verification
Model Checking
Maude
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
13:1
13:17
10.4230/LIPIcs.OPODIS.2017.13
article
Plane Formation by Synchronous Mobile Robots without Chirality
Tomita, Yusaku
Yamauchi, Yukiko
Kijima, Shuji
Yamashita, Masafumi
We consider a distributed system consisting of autonomous mobile computing entities called robots moving in the three-dimensional space (3D-space). The robots are anonymous, oblivious, fully-synchronous and have neither any access to the global coordinate system nor any explicit communication medium. Each robot cooperates with other robots by observing the positions of other robots in its local coordinate system. One of the most fundamental agreement problems in 3D-space is the plane formation problem that requires the robots to land on a common plane, that is not predefined. This problem is not always solvable because of the impossibility of symmetry breaking. While existing results assume that the robots agree on the handedness of their local coordinate systems, we remove the assumption and consider the robots without chirality. The robots without chirality can never break the symmetry consisting of rotation symmetry and reflection symmetry. Such symmetry in 3D-space is fully described by 17 symmetry types each of which forms a group. We extend the notion of symmetricity [Suzuki and Yamashita, SIAM J. Compt. 1999] [Yamauchi et al., PODC 2016] to cover these 17 symmetry groups. Then we give a characterization of initial configurations from which the fully-synchronous robots without chirality can form a plane in terms of symmetricity.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.13/LIPIcs.OPODIS.2017.13.pdf
Autonomous mobile robots
plane formation problem
symmetry breaking
group theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
14:1
14:16
10.4230/LIPIcs.OPODIS.2017.14
article
Treasure Hunt with Barely Communicating Agents
Dobrev, Stefan
Královic, Rastislav
Pardubská, Dana
We consider the problem of fault-tolerant parallel exhaustive search, a.k.a. “Treasure Hunt”, introduced by Fraigniaud, Korman and Rodeh in [13]: Imagine an infinite list of “boxes”, one of which contains a “treasure”. The ordering of the boxes reflects the importance of finding the treasure in a given box. There are k agents, whose goal is to locate the treasure in the least amount of time. The system is synchronous; at every step, an agent can ”open” a box and see whether the treasure is there. The hunt finishes when the first agent locates the treasure.
The original paper [13] considers non-cooperating randomized agents, out of which at most f can fail, with the failure pattern determined by an adversary. In this paper, we consider deterministic agents and investigate two failure models: The failing-agents model from [13] and a “black hole” model: At most f boxes contain “black holes”, placed by the adversary. When an agent opens a box containing a black hole, the agent disappears without an observable trace.
The crucial distinction, however, is that we consider “barely communicating” or “indirectly weakly communicating” agents: When an agent opens a box, it can tell whether the box has been previously opened. There are no other means of direct or indirect communication between the agents.
We show that adding even such weak means of communication has very strong impact on the solvability and complexity of the Treasure Hunt problem. In particular, in the failing agents model it allows the agents to be 1-competitive w.r.t. an optimal algorithm which does not know the location of the treasure, but is instantly notified of agent failures. In the black holes model
(where there is no deterministic solution for non-communicating agents even in the presence of a single black hole) we show a lower bound of 2f + 1 and an upper bound of 4f + 1 for the number of agents needed to solve Treasure Hunt in presence of up to f black holes, as well as partial results about the hunt time in the presence of few black holes.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.14/LIPIcs.OPODIS.2017.14.pdf
parallel exhaustive search
treasure hunt
fault-tolerant search
weak coordination
black holes
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
15:1
15:17
10.4230/LIPIcs.OPODIS.2017.15
article
Anonymous Processors with Synchronous Shared Memory: Monte Carlo Algorithms
Chlebus, Bogdan S.
De Marco, Gianluca
Talo, Muhammed
We consider synchronous distributed systems in which processors communicate by shared read- write variables. Processors are anonymous and do not know their number n. The goal is to assign individual names by all the processors to themselves. We develop algorithms that accomplish this for each of the four cases determined by the following independent properties of the model: concurrently attempting to write distinct values into the same shared memory register either is allowed or not, and the number of shared variables either is a constant or it is unbounded. For each such a case, we give a Monte Carlo algorithm that runs in the optimum expected time and uses the expected number of O(n log n) random bits. All our algorithms produce correct output upon termination with probabilities that are 1−n^{−Ω(1)}, which is best possible when terminating almost surely and using O(n log n) random bits.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.15/LIPIcs.OPODIS.2017.15.pdf
anonymous processors
synchrony
shared memory
read-write registers
naming
Monte Carlo algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
16:1
16:18
10.4230/LIPIcs.OPODIS.2017.16
article
Lower Bounds on the Amortized Time Complexity of Shared Objects
Attiya, Hagit
Fouren, Arie
The amortized step complexity of an implementation measures its performance as a whole, rather than the performance of individual operations. Specifically, the amortized step complexity of an implementation is the average number of steps performed by invoked operations, in the worst case, taken over all possible executions. The amortized step complexity of a wide range of known lock- free implementations for shared data structures, like stacks, queues, linked lists, doubly-linked lists and binary trees, includes an additive factor linear in the point contention—the number of processes simultaneously active in the execution.
This paper shows that an additive factor, linear in the point contention, is inherent in the amortized step complexity for lock-free implementations of many distributed data structures, including stacks, queues, heaps, linked lists and search trees.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.16/LIPIcs.OPODIS.2017.16.pdf
monotone objects
stacks and queues
trees
step complexity
remote memory references
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
17:1
17:16
10.4230/LIPIcs.OPODIS.2017.17
article
Mutual Exclusion Algorithms with Constant RMR Complexity and Wait-Free Exit Code
Dvir, Rotem
Taubenfeld, Gadi
Two local-spinning queue-based mutual exclusion algorithms are presented that have several de- sired properties: (1) their exit codes are wait-free, (2) they satisfy FIFO fairness, (3) they have constant RMR complexity in both the CC and the DSM models, (4) it is not assumed that the number of processes, n, is a priori known, that is, processes may appear or disappear intermit- tently, (5) they use only O(n) shared memory locations, and (6) they make no assumptions on what and how memory is allocated.
The algorithms are inspired by J. M. Mellor-Crummey and M. L. Scott famous MCS queue- based algorithm [13] which, except for not having a wait-free exit code, satisfies similar properties. A drawback of the MCS algorithm is that executing the exit code (i.e., releasing a lock) requires spinning – a process executing its exit code may need to wait for the process that is behind it in the queue to take a step before it can proceed. The two new algorithms overcome this drawback while preserving the simplicity and elegance of the original algorithm.
Our algorithms use exactly the same atomic instruction set as the original MCS algorithm, namely: read, write, fetch-and-store and compare-and-swap. In our second algorithm it is possible to recycle memory locations so that if there are L mutual exclusion locks, and each process accesses at most one lock at a time, then the algorithm needs only O(L + n) space, as compared to O(Ln) needed by our first algorithm.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.17/LIPIcs.OPODIS.2017.17.pdf
Mutual exclusion
locks
local-spinning
cache coherent
distributed shared memory
RMR complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
18:1
18:17
10.4230/LIPIcs.OPODIS.2017.18
article
Remote Memory References at Block Granularity
Attiya, Hagit
Yavneh, Gili
The cost of accessing shared objects that are stored in remote memory, while neglecting accesses to shared objects that are cached in the local memory, can be evaluated by the number of remote memory references (RMRs) in an execution. Two flavours of this measure—cache-coherent (CC) and distributed shared memory (DSM)—model two popular shared-memory architectures. The number of RMRs, however, does not take into account the granularity of memory accesses, namely, the fact that accesses to the shared memory are performed in blocks.
This paper proposes a new measure, called block RMRs, counting the number of remote memory references while taking into account the fact that shared objects can be grouped into blocks. On the one hand, this measure reflects the fact that the RMR incurred for bringing a shared object to the local memory might save another RMR for bringing another object placed at the same block. On the other hand, this measure accounts for false sharing: the fact that an RMR may be incurred when accessing an object due to a concurrent access to another object in the same block.
This paper proves that in both the CC and the DSM models, finding an optimal placement is NP-hard when objects have different sizes, even for two processes. In the CC model, finding an optimal placement, i.e., grouping of objects into blocks, is NP-hard when a block can store three objects or more; the result holds even if the sequence of accesses is known in advance. In the DSM model, the answer depends on whether there is an efficient mechanism to inform processes that the data in their local memory is no longer valid, i.e., cache coherence is supported. If coherence is supported with cheap invalidation, then finding an optimal solution is NP-hard. If coherence is not supported, an optimal placement can be achieved by placing each object in the memory of the process that accesses it most often, if the sequence of accesses is known in advance.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.18/LIPIcs.OPODIS.2017.18.pdf
false sharing
cache coherence
distributed shared memory
NP-hardness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
19:1
19:17
10.4230/LIPIcs.OPODIS.2017.19
article
Constant-Space Population Protocols for Uniform Bipartition
Yasumi, Hiroto
Ooshita, Fukuhito
Yamaguchi, Ken'ichi
Inoue, Michiko
In this paper, we consider a uniform bipartition problem in a population protocol model. The goal of the uniform bipartition problem is to divide a population into two groups of the same size. We study the problem under various assumptions: 1) a population with or without a base station, 2) weak or global fairness, 3) symmetric or asymmetric protocols, and 4) designated or arbitrary initial states. As a result, we completely clarify constant-space solvability of the uniform bipartition problem and, if solvable, propose space-optimal protocols.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.19/LIPIcs.OPODIS.2017.19.pdf
population protocol
uniform bipartition
distributed protocol
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
20:1
20:21
10.4230/LIPIcs.OPODIS.2017.20
article
Fast Detection of Stable and Count Predicates in Parallel Computations
Chauhan, Himanshu
Garg, Vijay K.
Enumerating all consistent states of a parallel computation that satisfy a given predicate is an important problem in debugging and verification of parallel programs. We give a fast algorithm to enumerate all consistent states of a parallel computation that satisfy a stable predicate. In addi- tion, we define a new category of global predicates called count predicates and give an algorithm to enumerate all consistent states (of the computation) that satisfy it. All existing predicate detection algorithms, such as BFS, DFS and Lex algorithms, do not exploit the knowledge about the nature of the predicates, and thus may visit all global states of the computation in the worst case. In comparison, our algorithms only visit the states that satisfy the given predicate, and thus take time and space that is a polynomial function of the number of states of interest. In doing so, they provide a significant reduction — exponential in many cases — in time complexities in comparison to existing algorithms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.20/LIPIcs.OPODIS.2017.20.pdf
Algorithms
Theory
Predicate Detection
Parallel Programs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
21:1
21:20
10.4230/LIPIcs.OPODIS.2017.21
article
Fast Distributed Approximation for TAP and 2-Edge-Connectivity
Censor-Hillel, Keren
Dory, Michal
The tree augmentation problem (TAP) is a fundamental network design problem, in which the input is a graph G and a spanning tree T for it, and the goal is to augment T with a minimum set of edges Aug from G, such that T ∪ Aug is 2-edge-connected.
TAP has been widely studied in the sequential setting. The best known approximation ratio of 2 for the weighted case dates back to the work of Frederickson and JáJá, SICOMP 1981. Recently, a 3/2-approximation was given for the unweighted case by Kortsarz and Nutov, TALG 2016, and recent breakthroughs by Adjiashvili, SODA 2017, and by Fiorini et al., 2017, give approximations better than 2 for bounded weights.
In this paper, we provide the first fast distributed approximations for TAP. We present a distributed 2-approximation for weighted TAP which completes in O(h) rounds, where h is the height of T . When h is large, we show a much faster 4-approximation algorithm for the unweighted case, completing in O(D + (√n) log^{*} n) rounds, where n is the number of vertices and D is the diameter of G.
Immediate consequences of our results are an O(D)-round 2-approximation algorithm for the minimum size 2-edge-connected spanning subgraph, which significantly improves upon the running time of previous approximation algorithms, and an O(hMST + (√n)log^{*} n)-round 3- approximation algorithm for the weighted case, where hMST is the height of the MST of the graph. Additional applications are algorithms for verifying 2-edge-connectivity and for augment- ing the connectivity of any connected spanning subgraph to 2.
Finally, we complement our study with proving lower bounds for distributed approximations of TAP.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.21/LIPIcs.OPODIS.2017.21.pdf
approximation algorithms
distributed network design
connectivity augmentation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
22:1
22:16
10.4230/LIPIcs.OPODIS.2017.22
article
Schlegel Diagram and Optimizable Immediate Snapshot Protocol
Nishimura, Susumu
In the topological study of distributed systems, the immediate snapshot is the fundamental computation block for the topological characterization of wait-free solvable tasks. However, in reality, the immediate snapshot is not available as a native built-in operation on shared memory distributed systems. Borowsky and Gafni have proposed a wait-free multi-round protocol that implements the immediate snapshot using more primitive operations, namely the atomic reads and writes.
In this paper, up to an appropriate reformulation on the original protocol by Borowsky and Gafni, we establish a tight link between each round of the protocol and a topological operation of subdivision using Schlegel diagram. Due to the fact shown by Kozlov that the standard chromatic subdivision is obtained by iterated subdivision using Schlegel diagram, the reformulated version is proven to compute the immediate snapshot in a topologically smoother way. We also show that the reformulated protocol is amenable to optimization: Since each round restricts the possible candidates of output to an iteratively smaller region of finer subdivision, each process executing the protocol can decide at an earlier round, beyond which the same final output is reached no matter how the remaining rounds are executed. This reduces the number of read and write operations involved in the overall execution of the protocol, relieving the bottleneck of access to shared memory.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.22/LIPIcs.OPODIS.2017.22.pdf
Immediate snapshot protocol
Schlegel diagram
chromatic subdivision
program specialization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
23:1
23:17
10.4230/LIPIcs.OPODIS.2017.23
article
Designing a Planetary-Scale IMAP Service with Conflict-free Replicated Data Types
Jungnickel, Tim
Oldenburg, Lennart
Loibl, Matthias
Modern geo-replicated software serving millions of users across the globe faces the consequences of the CAP dilemma, i.e., the inevitable conflicts that arise when multiple nodes accept writes on shared state. The underlying problem is commonly known as fault-tolerant multi-leader replica- tion; actively researched in the distributed systems and database communities. As a more recent theoretical framework, Conflict-free Replicated Data Types (CRDTs) propose a solution to this problem by offering a set of always converging primitives. However, modeling non-trivial system state with CRDT primitives is a challenging and error-prone task. In this work, we propose a solution for a geo-replicated online service with fault-tolerant multi-leader replication based on CRDTs. We chose IMAP as use case due to its prevalence and simplicity. Therefore, we modeled an IMAP-CRDT and verified its correctness with the interactive theorem prover Isabelle/HOL. In order to bridge the gap between theory and practice, we implemented an open-source proto- type pluto and an IMAP benchmark for write-intensive workloads. We evaluated our prototype against the standard IMAP server Dovecot on a multi-continent public cloud. The results ex- pose the limitations of Dovecot with respect to response time performance and replication lag. Our prototype was able to leverage its conceptual advantages and outperformed Dovecot. We find that our approach is promising when facing the multitude of potential concurrency bugs in development of systems at planetary scale.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.23/LIPIcs.OPODIS.2017.23.pdf
Geo-Replication
CRDT
Distributed Systems
IMAP
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
24:1
24:19
10.4230/LIPIcs.OPODIS.2017.24
article
Non-Uniform Replication
Cabrita, Gonçalo
Preguiça, Nuno
Replication is a key technique in the design of efficient and reliable distributed systems. As information grows, it becomes difficult or even impossible to store all information at every replica. A common approach to deal with this problem is to rely on partial replication, where each replica maintains only a part of the total system information. As a consequence, a remote replica might need to be contacted for computing the reply to some given query, which leads to high latency costs particularly in geo-replicated settings. In this work, we introduce the concept of non- uniform replication, where each replica stores only part of the information, but where all replicas store enough information to answer every query. We apply this concept to eventual consistency and conflict-free replicated data types. We show that this model can address useful problems and present two data types that solve such problems. Our evaluation shows that non-uniform replication is more efficient than traditional replication, using less storage space and network bandwidth.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.24/LIPIcs.OPODIS.2017.24.pdf
Non-uniform Replication
Partial Replication
Replicated Data Types
Eventual Consistency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
25:1
25:19
10.4230/LIPIcs.OPODIS.2017.25
article
Solida: A Blockchain Protocol Based on Reconfigurable Byzantine Consensus
Abraham, Ittai
Malkhi, Dahlia
Nayak, Kartik
Ren, Ling
Spiegelman, Alexander
The decentralized cryptocurrency Bitcoin has experienced great success but also encountered many challenges. One of the challenges has been the long confirmation time. Another chal- lenge is the lack of incentives at certain steps of the protocol, raising concerns for transaction withholding, selfish mining, etc. To address these challenges, we propose Solida, a decentralized blockchain protocol based on reconfigurable Byzantine consensus augmented by proof-of-work. Solida improves on Bitcoin in confirmation time, and provides safety and liveness assuming the adversary control less than (roughly) one-third of the total mining power.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.25/LIPIcs.OPODIS.2017.25.pdf
Cryptocurrency
Blockchain
Byzantine fault tolerance
Reconfiguration
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
26:1
26:17
10.4230/LIPIcs.OPODIS.2017.26
article
Efficient and Modular Consensus-Free Reconfiguration for Fault-Tolerant Storage
Alchieri, Eduardo
Bessani, Alysson
Greve, Fabíola
Fraga, Joni da Silva
Quorum systems are useful tools for implementing consistent and available storage in the presence of failures. These systems usually comprise of a static set of servers that provide a fault-tolerant read/write register accessed by a set of clients. We consider a dynamic variant of these systems and propose FreeStore, a set of fault-tolerant protocols that emulates a register in dynamic asynchronous systems in which processes are able to join/leave the set of servers during the execution. These protocols use a new abstraction called view generators, that captures the agreement requirements of reconfiguration and can be implemented in different system models with different properties. Particularly interesting, we present a reconfiguration protocol that is modular, efficient, consensus-free and loosely coupled with read/write protocols. An analysis and an experimental evaluation show that the proposed protocols improve the overall system performance when compared with previous solutions.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.26/LIPIcs.OPODIS.2017.26.pdf
Distributed Systems
Reconfiguration
Fault-Tolerant Quorum Systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
27:1
27:20
10.4230/LIPIcs.OPODIS.2017.27
article
Hardening Cassandra Against Byzantine Failures
Friedman, Roy
Licher, Roni
Cassandra is one of the most widely used distributed data stores. In this work, we analyze Cassandra’s vulnerabilities when facing Byzantine failures and propose protocols for hardening Cassandra against them. We examine several alternative design choices and compare between them both qualitatively and empirically by using the Yahoo! Cloud Serving Benchmark (YCSB) performance benchmark.
Some of our proposals include novel combinations of quorum access protocols with MAC signatures arrays and elliptic curve public key cryptography so that in the normal data path, there are no public key verifications and only a single relatively cheap elliptic curve signature made by the client. Yet, these enable data recovery and authentication despite Byzantine failures and across membership configuration changes. In the experiments, we demonstrate that our best design alternative obtains roughly half the performance of plain (non-Byzantine) Cassandra.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.27/LIPIcs.OPODIS.2017.27.pdf
Cassandra
Byzantine Fault Tolerance
Distributed Storage
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
28:1
28:16
10.4230/LIPIcs.OPODIS.2017.28
article
Vulnerability-Tolerant Transport Layer Security
Joaquim, André
Pardal, Miguel L.
Correia, Miguel
SSL/TLS communication channels play a very important role in Internet security, including cloud computing and server infrastructures. There are often concerns about the strength of the encryption mechanisms used in TLS channels. Vulnerabilities can lead to some of the cipher suites once thought to be secure to become insecure and no longer recommended for use or in urgent need of a software update. However, the deprecation/update process is very slow and weeks or months can go by before most web servers and clients are protected, and some servers and clients may never be updated. In the meantime, the communications are at risk of being intercepted and tampered by attackers.
In this paper we propose an alternative to TLS to mitigate the problem of secure commu- nication channels being susceptible to attacks due to unexpected vulnerabilities in its mechan- isms. Our solution, called Vulnerability-Tolerant Transport Layer Security (vtTLS), is based on diversity and redundancy of cryptographic mechanisms and certificates to ensure a secure communication even when one or more mechanisms are vulnerable. Our solution relies on a combination of k cipher suites which ensure that even if k − 1 cipher suites are insecure or vul- nerable, the remaining cipher suite keeps the communication channel secure. The performance and cost of vtTLS were evaluated and compared with OpenSSL, one of the most widely used implementations of TLS.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.28/LIPIcs.OPODIS.2017.28.pdf
Secure communication channels
Transport layer security
SSL/TLS
Diversity
Redundancy
Vulnerability tolerance
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
29:1
29:20
10.4230/LIPIcs.OPODIS.2017.29
article
Asynchronous Message Orderings Beyond Causality
Shimi, Adam
Hurault, Aurélie
Quéinnec, Philippe
In the asynchronous setting, distributed behavior is traditionally studied through computa- tions, the Happened-Before posets of events generated by the system. An equivalent perspective considers the linear extensions of the generated computations: each linear extension defines a sequence of events, called an execution. Both perspective were leveraged in the study of asyn- chronous point-to-point message orderings over computations; yet neither allows us to interpret message orderings defined over executions. Can we nevertheless make sense of such an ordering, maybe even use it to understand asynchronicity better?
We provide a general answer by defining a topology on the set of executions which captures the fundamental assumptions of asynchronicity. This topology links each message ordering over executions with two sets of computations: its closure, the computations for which at least one linear extension satisfies the predicate; and its interior, the computations for which all linear ex- tensions satisfy it. These sets of computations represent respectively the uncertainty brought by asynchronicity – the computations where the predicate is satisfiable – and the certainty available despite asynchronicity – the computations where the predicate must hold. The paper demon- strates the use of this topological approach by examining closures and interiors of interesting orderings over executions.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.29/LIPIcs.OPODIS.2017.29.pdf
Asynchronous computations
Point-to-point message orderings
Causality
Topology
Interior
Closure
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
30:1
30:16
10.4230/LIPIcs.OPODIS.2017.30
article
Constant Space and Non-Constant Time in Distributed Computing
Lempiäinen, Tuomo
Suomela, Jukka
While the relationship of time and space is an established topic in traditional centralised com- plexity theory, this is not the case in distributed computing. We aim to remedy this by studying the time and space complexity of algorithms in a weak message-passing model of distributed com- puting. While a constant number of communication rounds implies a constant number of states visited during the execution, the other direction is not clear at all. We show that indeed, there exist non-trivial graph problems that are solvable by constant-space algorithms but that require a non-constant running time. Somewhat surprisingly, this holds even when restricted to the class of only cycle and path graphs. Our work provides us with a new complexity class for distributed computing and raises interesting questions about the existence of further combinations of time and space complexity.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.30/LIPIcs.OPODIS.2017.30.pdf
distributed computing
space complexity
constant-space algorithms
weak models
Thue-Morse sequence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
31:1
31:16
10.4230/LIPIcs.OPODIS.2017.31
article
Shape Formation by Programmable Particles
Di Luna, Giuseppe A.
Flocchini, Paola
Santoro, Nicola
Viglietta, Giovanni
Yamauchi, Yukiko
Shape formation (or pattern formation) is a basic distributed problem for systems of compu- tational mobile entities. Intensively studied for systems of autonomous mobile robots, it has recently been investigated in the realm of programmable matter, where entities are assumed to be small and with severely limited capabilities. Namely, it has been studied in the geometric Amoebot model, where the anonymous entities, called particles, operate on a hexagonal tessella- tion of the plane and have limited computational power (they have constant memory), strictly local interaction and communication capabilities (only with particles in neighboring nodes of the grid), and limited motorial capabilities (from a grid node to an empty neighboring node); their activation is controlled by an adversarial scheduler. Recent investigations have shown how, start- ing from a well-structured configuration in which the particles form a (not necessarily complete) triangle, the particles can form a large class of shapes. This result has been established under several assumptions: agreement on the clockwise direction (i.e., chirality), a sequential activation schedule, and randomization (i.e., particles can flip coins to elect a leader).
In this paper we provide a characterization of which shapes can be formed deterministically starting from any simply connected initial configuration of n particles. The characterization is constructive: we provide a universal shape formation algorithm that, for each feasible pair of shapes (S_0,S_F), allows the particles to form the final shape SF (given in input) starting from the initial shape S_0, unknown to the particles. The final configuration will be an appropriate scaled-up copy of S_F depending on n.
If randomization is allowed, then any input shape can be formed from any initial (simply connected) shape by our algorithm, provided that there are enough particles.
Our algorithm works without chirality, proving that chirality is computationally irrelevant for shape formation. Furthermore, it works under a strong adversarial scheduler, not necessarily sequential.
We also consider the complexity of shape formation both in terms of the number of rounds and the total number of moves performed by the particles executing a universal shape formation algorithm. We prove that our solution has a complexity of O(n^2) rounds and moves: this number of moves is also asymptotically worst-case optimal.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.31/LIPIcs.OPODIS.2017.31.pdf
Shape formation
pattern formation
programmable matter
Amoebots
leader election
distributed algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-28
95
32:1
32:20
10.4230/LIPIcs.OPODIS.2017.32
article
Synthesis of Distributed Algorithms with Parameterized Threshold Guards
Lazic, Marijana
Konnov, Igor
Widder, Josef
Bloem, Roderick
Fault-tolerant distributed algorithms are notoriously hard to get right. In this paper we introduce an automated method that helps in that process: the designer provides specifications (the problem to be solved) and a sketch of a distributed algorithm that keeps arithmetic details unspecified. Our tool then automatically fills the missing parts.
Fault-tolerant distributed algorithms are typically parameterized, that is, they are designed to work for any number n of processes and any number t of faults, provided some resilience condition holds; e.g., n > 3t. In this paper we automatically synthesize distributed algorithms that work for all parameter values that satisfy the resilience condition. We focus on threshold- guarded distributed algorithms, where actions are taken only if a sufficiently large number of messages is received, e.g., more than t or n/2. Both expressions can be derived by choosing the right values for the coefficients a, b, and c, in the sketch of a threshold a·n+b·t+c. Our method takes as input a sketch of an asynchronous threshold-based fault-tolerant distributed algorithm — where the guards are missing exact coefficients—and then iteratively picks the values for the coefficients.
Our approach combines recent progress in parameterized model checking of distributed algo- rithms with counterexample-guided synthesis. Besides theoretical results on termination of the synthesis procedure, we experimentally evaluate our method and show that it can synthesize sev- eral distributed algorithms from the literature, e.g., Byzantine reliable broadcast and Byzantine one-step consensus. In addition, for several new variations of safety and liveness specifications, our tool generates new distributed algorithms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol095-opodis2017/LIPIcs.OPODIS.2017.32/LIPIcs.OPODIS.2017.32.pdf
fault-tolerant distributed algorithms
byzantine faults
parameterized model checking
program synthesis