Search Results

Documents authored by Attiya, Hagit

Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2024.42
Brief Announcement: Solvability of Three-Process General Tasks

Authors: Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum

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

Abstract
The topological view on distributed computing represents a task T as a relation Δ between the complex ℐ of its inputs and the complex 𝒪 of its outputs. A cornerstone result in the field is an elegant computability characterization of the solvability of colorless tasks in terms of ℐ, 𝒪 and Δ. Essentially, a colorless task is wait-free solvable if and only if there is a continuous map from the geometric realization of ℐ to that of 𝒪 that respects Δ. This paper makes headway towards providing an analogous characterization for general tasks, which are not necessarily colorless, by concentrating on the case of three-process inputless tasks. Our key contribution is identifying local articulation points as an obstacle for the solvability of general tasks, and defining a topological deformation on the output complex of a task T, which eliminates these points by splitting them, to obtain a new task T', with an adjusted relation Δ' between the input complex ℐ and an output complex 𝒪' without articulation points. We obtain a new characterization of wait-free solvability of three-process general tasks: T is wait-free solvable if and only if there is a continuous map from the geometric realization of ℐ to that of 𝒪' that respects Δ'.
Cite as

Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum. Brief Announcement: Solvability of Three-Process General Tasks. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 42:1-42:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2024.42,
  author =	{Attiya, Hagit and Fraigniaud, Pierre and Paz, Ami and Rajsbaum, Sergio},
  title =	{{Brief Announcement: Solvability of Three-Process General Tasks}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{42:1--42:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.42},
  URN =		{urn:nbn:de:0030-drops-212700},
  doi =		{10.4230/LIPIcs.DISC.2024.42},
  annote =	{Keywords: Wait-free computing, lower bounds, topology}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2023.4
The Synchronization Power of Auditable Registers

Authors: Hagit Attiya, Antonella Del Pozzo, Alessia Milani, Ulysse Pavloff, and Alexandre Rapetti

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

Abstract
Auditability allows to track all the read operations performed on a register. It abstracts the need of data owners to control access to their data, tracking who read which information. This work considers possible formalizations of auditing and their ramification for the possibility of providing it. The natural definition is to require a linearization of all write, read and audit operations together (atomic auditing). The paper shows that atomic auditing is a powerful tool, as it can be used to solve consensus. The number of processes that can solve consensus using atomic audit depends on the number of processes that can read or audit the register. If there is a single reader or a single auditor (the writer), then consensus can be solved among two processes. If multiple readers and auditors are possible, then consensus can be solved among the same number of processes. This means that strong synchronization primitives are needed to support atomic auditing. We give implementations of atomic audit when there are either multiple readers or multiple auditors (but not both) using primitives with consensus number 2 (swap and fetch&add). When there are multiple readers and multiple auditors, the implementation uses compare&swap. These findings motivate a weaker definition, in which audit operations are not linearized together with read and write operations (regular auditing). We prove that regular auditing can be implemented from ordinary reads and writes on atomic registers.
Cite as

Hagit Attiya, Antonella Del Pozzo, Alessia Milani, Ulysse Pavloff, and Alexandre Rapetti. The Synchronization Power of Auditable Registers. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2023.4,
  author =	{Attiya, Hagit and Del Pozzo, Antonella and Milani, Alessia and Pavloff, Ulysse and Rapetti, Alexandre},
  title =	{{The Synchronization Power of Auditable Registers}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.4},
  URN =		{urn:nbn:de:0030-drops-194940},
  doi =		{10.4230/LIPIcs.OPODIS.2023.4},
  annote =	{Keywords: Auditability, atomic register, fault tolerance, consensus number}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2023.6
Multi-Valued Connected Consensus: A New Perspective on Crusader Agreement and Adopt-Commit

Authors: Hagit Attiya and Jennifer L. Welch

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

Abstract
Algorithms to solve fault-tolerant consensus in asynchronous systems often rely on primitives such as crusader agreement, adopt-commit, and graded broadcast, which provide weaker agreement properties than consensus. Although these primitives have a similar flavor, they have been defined and implemented separately in ad hoc ways. We propose a new problem called connected consensus that has as special cases crusader agreement, adopt-commit, and graded broadcast, and generalizes them to handle multi-valued inputs. The generalization is accomplished by relating the problem to approximate agreement on graphs. We present three algorithms for multi-valued connected consensus in asynchronous message-passing systems, one tolerating crash failures and two tolerating malicious (unauthenticated Byzantine) failures. We extend the definition of binding, a desirable property recently identified as supporting binary consensus algorithms that are correct against adaptive adversaries, to the multi-valued input case and show that all our algorithms satisfy the property. Our crash-resilient algorithm has failure-resilience and time complexity that we show are optimal. When restricted to the case of binary inputs, the algorithm has improved time complexity over prior algorithms. Our two algorithms for malicious failures trade off failure resilience and time complexity. The first algorithm has time complexity that we prove is optimal but worse failure-resilience, while the second has failure-resilience that we prove is optimal but worse time complexity. When restricted to the case of binary inputs, the time complexity (as well as resilience) of the second algorithm matches that of prior algorithms. The contributions of the paper are first, a deeper insight into the connections between primitives commonly used to solve the fundamental problem of fault-tolerant consensus, and second, implementations of these primitives that can contribute to improved consensus algorithms.
Cite as

Hagit Attiya and Jennifer L. Welch. Multi-Valued Connected Consensus: A New Perspective on Crusader Agreement and Adopt-Commit. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2023.6,
  author =	{Attiya, Hagit and Welch, Jennifer L.},
  title =	{{Multi-Valued Connected Consensus: A New Perspective on Crusader Agreement and Adopt-Commit}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.6},
  URN =		{urn:nbn:de:0030-drops-194967},
  doi =		{10.4230/LIPIcs.OPODIS.2023.6},
  annote =	{Keywords: graded broadcast, gradecast, binding, approximate agreement}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2023.24
Recoverable and Detectable Self-Implementations of Swap

Authors: Tomer Lev Lehman, Hagit Attiya, and Danny Hendler

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

Abstract
Recoverable algorithms tolerate failures and recoveries of processes by using non-volatile memory. Of particular interest are self-implementations of key operations, in which a recoverable operation is implemented from its non-recoverable counterpart (in addition to reads and writes). This paper presents two self-implementations of the swap operation. One works in the system-wide failures model, where all processes fail and recover together, and the other in the independent failures model, where each process crashes and recovers independently of the other processes. Both algorithms are wait-free in crash-free executions, but their recovery code is blocking. We prove that this is inherent for the independent failures model. The impossibility result is proved for implementations of distinguishable operations using interfering functions, and in particular, it applies to a recoverable self-implementation of swap.
Cite as

Tomer Lev Lehman, Hagit Attiya, and Danny Hendler. Recoverable and Detectable Self-Implementations of Swap. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{levlehman_et_al:LIPIcs.OPODIS.2023.24,
  author =	{Lev Lehman, Tomer and Attiya, Hagit and Hendler, Danny},
  title =	{{Recoverable and Detectable Self-Implementations of Swap}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{24:1--24:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.24},
  URN =		{urn:nbn:de:0030-drops-195140},
  doi =		{10.4230/LIPIcs.OPODIS.2023.24},
  annote =	{Keywords: Multi-core algorithms, persistent memory, non-volatile memory, recoverable objects, detectablitly}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2023.32
Bounds on Worst-Case Responsiveness for Agreement Algorithms

Authors: Hagit Attiya and Jennifer L. Welch

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

Abstract
We study the worst-case time complexity of solving two agreement problems, consensus and broadcast, in systems with n processes subject to no more than t process failures. In both problems, correct processes must decide on a common value; in the consensus problem, each process has an input and if the inputs of correct processes are all the same, then that must be the common decision, whereas in the broadcast problem, only one process (the sender) has an input and if the sender is correct, then its input must be the common decision. We focus on systems where there is an upper bound Δ on the message delivery time but it is expected that typically, messages arrive much faster, say within some time d. While Δ may or may not be known in advance, d is inherently unknown and specific to each execution. The goal is to design deterministic algorithms whose running times have minimal to no dependence on Δ, a property called responsiveness. We present a generic algorithm transformation that, when applied to appropriate eventually-synchronous consensus (or broadcast) algorithms, results in consensus (or broadcast) algorithms for send omission failures, authenticated Byzantine failures, and unauthenticated Byzantine failures whose running times have no dependence on Δ; their worst-case time complexities are all O(td), which is asymptotically optimal. The algorithm for send omission failures requires n > 2t, while those for Byzantine failures, both authenticated and unauthenticated, require n > 3t. The failure-resilience of the unauthenticated Byzantine algorithm is optimal. For authenticated Byzantine failures, existing agreement algorithms provide worst-case time complexity O(t Δ) when n is at most 3t. (When n ≤ 2t, broadcast is solvable while consensus is not.) We prove a lower bound on the worst-case time complexity of ⌊(3t-n)/2⌋ d + Δ when n is at most 3t. Although lower bounds of Δ and (t+1)d were already known, our new lower bound indicates that, at least when n ≤ 2t, it is impossible for an algorithm to pay these bounds in parallel.
Cite as

Hagit Attiya and Jennifer L. Welch. Bounds on Worst-Case Responsiveness for Agreement Algorithms. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2023.32,
  author =	{Attiya, Hagit and Welch, Jennifer L.},
  title =	{{Bounds on Worst-Case Responsiveness for Agreement Algorithms}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.32},
  URN =		{urn:nbn:de:0030-drops-195229},
  doi =		{10.4230/LIPIcs.OPODIS.2023.32},
  annote =	{Keywords: bounded-delay model, basic round model, omission failures, Byzantine failures}
}
Document
DOI: 10.4230/LIPIcs.DISC.2023.4
One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks

Authors: Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
The paper compares two generic techniques for deriving lower bounds and impossibility results in distributed computing. First, we prove a speedup theorem (a-la Brandt, 2019), for wait-free colorless algorithms, aiming at capturing the essence of the seminal round-reduction proof establishing a lower bound on the number of rounds for 3-coloring a cycle (Linial, 1992), and going by backward induction. Second, we consider FLP-style proofs, aiming at capturing the essence of the seminal consensus impossibility proof (Fischer, Lynch, and Paterson, 1985) and using forward induction. We show that despite their very different natures, these two forms of proof are tightly connected. In particular, we show that for every colorless task Π, if there is a round-reduction proof establishing the impossibility of solving Π using wait-free colorless algorithms, then there is an FLP-style proof establishing the same impossibility. For 1-dimensional colorless tasks (for an arbitrarily number n ≥ 2 of processes), we prove that the two proof techniques have exactly the same power, and more importantly, both are complete: if a 1-dimensional colorless task is not wait-free solvable by n ≥ 2 processes, then the impossibility can be proved by both proof techniques. Moreover, a round-reduction proof can be automatically derived, and an FLP-style proof can be automatically generated from it. Finally, we illustrate the use of these two techniques by establishing the impossibility of solving any colorless covering task of arbitrary dimension by wait-free algorithms.
Cite as

Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum. One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2023.4,
  author =	{Attiya, Hagit and Fraigniaud, Pierre and Paz, Ami and Rajsbaum, Sergio},
  title =	{{One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.4},
  URN =		{urn:nbn:de:0030-drops-191304},
  doi =		{10.4230/LIPIcs.DISC.2023.4},
  annote =	{Keywords: Wait-free computing, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.DISC.2023.5
Topological Characterization of Task Solvability in General Models of Computation

Authors: Hagit Attiya, Armando Castañeda, and Thomas Nowak

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.
Cite as

Hagit Attiya, Armando Castañeda, and Thomas Nowak. Topological Characterization of Task Solvability in General Models of Computation. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2023.5,
  author =	{Attiya, Hagit and Casta\~{n}eda, Armando and Nowak, Thomas},
  title =	{{Topological Characterization of Task Solvability in General Models of Computation}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{5:1--5:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.5},
  URN =		{urn:nbn:de:0030-drops-191315},
  doi =		{10.4230/LIPIcs.DISC.2023.5},
  annote =	{Keywords: task solvability, combinatorial topology, point-set topology}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2023.36
Brief Announcement: Multi-Valued Connected Consensus: A New Perspective on Crusader Agreement and Adopt-Commit

Authors: Hagit Attiya and Jennifer L. Welch

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
Algorithms to solve fault-tolerant consensus in asynchronous systems often rely on primitives such as crusader agreement, adopt-commit, and graded broadcast, which provide weaker agreement properties than consensus. Although these primitives have a similar flavor, they have been defined and implemented separately in ad hoc ways. We propose a new problem called connected consensus that has as special cases crusader agreement, adopt-commit, and graded broadcast, and generalizes them to handle multi-valued (non-binary) inputs. The generalization is accomplished by relating the problem to approximate agreement on graphs. We present three algorithms for multi-valued connected consensus in asynchronous message-passing systems, one tolerating crash failures and two tolerating malicious (unauthenticated Byzantine) failures. We extend the definition of binding, a desirable property recently identified as supporting binary consensus algorithms that are correct against adaptive adversaries, to the multi-valued input case and show that all our algorithms satisfy the property. Our crash-resilient algorithm has failure-resilience and time complexity that we show are optimal. When restricted to the case of binary inputs, the algorithm has improved time complexity over prior algorithms. Our two algorithms for malicious failures trade off failure resilience and time complexity. The first algorithm has time complexity that we prove is optimal but worse failure-resilience, while the second has failure-resilience that we prove is optimal but worse time complexity. When restricted to the case of binary inputs, the time complexity (as well as resilience) of the second algorithm matches that of prior algorithms.
Cite as

Hagit Attiya and Jennifer L. Welch. Brief Announcement: Multi-Valued Connected Consensus: A New Perspective on Crusader Agreement and Adopt-Commit. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 36:1-36:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2023.36,
  author =	{Attiya, Hagit and Welch, Jennifer L.},
  title =	{{Brief Announcement: Multi-Valued Connected Consensus: A New Perspective on Crusader Agreement and Adopt-Commit}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{36:1--36:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.36},
  URN =		{urn:nbn:de:0030-drops-191620},
  doi =		{10.4230/LIPIcs.DISC.2023.36},
  annote =	{Keywords: graded broadcast, gradecast, binding, approximate agreement}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2023.44
Brief Announcement: Recoverable and Detectable Self-Implementations of Swap

Authors: Tomer Lev Lehman, Hagit Attiya, and Danny Hendler

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
Recoverable algorithms tolerate failures and recoveries of processes by using non-volatile memory. Of particular interest are self-implementations of key operations, in which a recoverable operation is implemented from its non-recoverable counterpart (in addition to reads and writes). This paper presents two self-implementations of the SWAP operation. One works in the system-wide failures model, where all processes fail and recover together, and the other in the independent failures model, where each process crashes and recovers independently of the other processes. Both algorithms are wait-free in crash-free executions, but their recovery code is blocking. We prove that this is inherent for the independent failures model. The impossibility result is proved for implementations of distinguishable operations using interfering functions, and in particular, it applies to a recoverable self-implementation of swap.
Cite as

Tomer Lev Lehman, Hagit Attiya, and Danny Hendler. Brief Announcement: Recoverable and Detectable Self-Implementations of Swap. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 44:1-44:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{levlehman_et_al:LIPIcs.DISC.2023.44,
  author =	{Lev Lehman, Tomer and Attiya, Hagit and Hendler, Danny},
  title =	{{Brief Announcement: Recoverable and Detectable Self-Implementations of Swap}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{44:1--44:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.44},
  URN =		{urn:nbn:de:0030-drops-191704},
  doi =		{10.4230/LIPIcs.DISC.2023.44},
  annote =	{Keywords: Persistent memory, non-volatile memory, recoverable objects, detectablitly}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.27
Faithful Simulation of Randomized BFT Protocols on Block DAGs

Authors: Hagit Attiya, Constantin Enea, and Shafik Nassar

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Byzantine Fault-Tolerant (BFT) protocols that are based on Directed Acyclic Graphs (DAGs) are attractive due to their many advantages in asynchronous blockchain systems. These DAG-based protocols can be viewed as a simulation of some BFT protocol on a DAG. Many DAG-based BFT protocols rely on randomization, since they are used for agreement and ordering of transactions, which cannot be achieved deterministically in asynchronous systems. Randomization is achieved either through local sources of randomness, or by employing shared objects that provide a common source of randomness, e.g., common coins. A DAG simulation of a randomized protocol should be faithful, in the sense that it precisely preserves the properties of the original BFT protocol, and in particular, their probability distributions. We argue that faithfulness is ensured by a forward simulation. We show how to faithfully simulate any BFT protocol that uses public coins and shared objects, like common coins.
Cite as

Hagit Attiya, Constantin Enea, and Shafik Nassar. Faithful Simulation of Randomized BFT Protocols on Block DAGs. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.CONCUR.2023.27,
  author =	{Attiya, Hagit and Enea, Constantin and Nassar, Shafik},
  title =	{{Faithful Simulation of Randomized BFT Protocols on Block DAGs}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.27},
  URN =		{urn:nbn:de:0030-drops-190210},
  doi =		{10.4230/LIPIcs.CONCUR.2023.27},
  annote =	{Keywords: Byzantine failures, Hyperproperties, Forward Simulation}
}
Document
DOI: 10.4230/DagRep.12.12.27
Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492)

Authors: Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova

Published in: Dagstuhl Reports, Volume 12, Issue 12 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22492 "Formal Methods and Distributed Computing: Stronger Together", held in December 2022.
Cite as

Hagit Attiya, Constantin Enea, Sergio Rajsbaum, and Ana Sokolova. Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492). In Dagstuhl Reports, Volume 12, Issue 12, pp. 27-53, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{attiya_et_al:DagRep.12.12.27,
  author =	{Attiya, Hagit and Enea, Constantin and Rajsbaum, Sergio and Sokolova, Ana},
  title =	{{Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492)}},
  pages =	{27--53},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{12},
  editor =	{Attiya, Hagit and Enea, Constantin and Rajsbaum, Sergio and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.12.27},
  URN =		{urn:nbn:de:0030-drops-178452},
  doi =		{10.4230/DagRep.12.12.27},
  annote =	{Keywords: automated verification and reasoning, concurrent data structures and transactions, distributed algorithms, large-scale replication}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2022.6
The Step Complexity of Multidimensional Approximate Agreement

Authors: Hagit Attiya and Faith Ellen

Published in: LIPIcs, Volume 253, 26th International Conference on Principles of Distributed Systems (OPODIS 2022)

Abstract
Approximate agreement allows a set of n processes to obtain outputs that are within a specified distance ε > 0 of one another and within the convex hull of the inputs. When the inputs are real numbers, there is a wait-free shared-memory approximate agreement algorithm [Moran, 1995] whose step complexity is in O(n log(S/ε)), where S, the spread of the inputs, is the maximal distance between inputs. There is another wait-free algorithm [Schenk, 1995] that avoids the dependence on n and achieves O(log(M/ε)) step complexity where M, the magnitude of the inputs, is the absolute value of the maximal input. This paper considers whether it is possible to obtain an approximate agreement algorithm whose step complexity depends on neither n nor the magnitude of the inputs, which can be much larger than their spread. On the negative side, we prove that Ω(min{(log M)/(log log M), (√log n)/(log log n)}) is a lower bound on the step complexity of approximate agreement, even when the inputs are real numbers. On the positive side, we prove that a polylogarithmic dependence on n and S/ε can be achieved, by presenting an approximate agreement algorithm with O(log n (log n + log(S/ε))) step complexity. Our algorithm works for multidimensional domains. The step complexity can be further restricted to be in O(min{log n (log n + log (S/ε)), log(M/ε)}) when the inputs are real numbers.
Cite as

Hagit Attiya and Faith Ellen. The Step Complexity of Multidimensional Approximate Agreement. In 26th International Conference on Principles of Distributed Systems (OPODIS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 253, pp. 6:1-6:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2022.6,
  author =	{Attiya, Hagit and Ellen, Faith},
  title =	{{The Step Complexity of Multidimensional Approximate Agreement}},
  booktitle =	{26th International Conference on Principles of Distributed Systems (OPODIS 2022)},
  pages =	{6:1--6:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-265-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{253},
  editor =	{Hillel, Eshcar and Palmieri, Roberto and Rivi\`{e}re, Etienne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2022.6},
  URN =		{urn:nbn:de:0030-drops-176261},
  doi =		{10.4230/LIPIcs.OPODIS.2022.6},
  annote =	{Keywords: approximate agreement, conflict detection, shared memory, wait-freedom, step complexity}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2021.29
Recoverable and Detectable Fetch&Add

Authors: Liad Nahum, Hagit Attiya, Ohad Ben-Baruch, and Danny Hendler

Published in: LIPIcs, Volume 217, 25th International Conference on Principles of Distributed Systems (OPODIS 2021)

Abstract
The emergence of systems with non-volatile main memory (NVRAM) increases the need for persistent concurrent objects. Of specific interest are recoverable implementations that, in addition to being robust to crash-failures, are also detectable. Detectability ensures that upon recovery, it is possible to infer whether the failed operation took effect or not and, in the former case, obtain its response. This work presents two recoverable detectable Fetch&Add (FAA) algorithms that are self-implementations, i.e, use only a fetch&add base object, in addition to read/write registers. The algorithms target two different models for recovery: the global-crash model and the individual-crash model. In both algorithms, operations are wait-free when there are no crashes, but the recovery code may block if there are repeated failures. We also prove that in the individual-crash model, there is no implementation of recoverable and detectable FAA using only read, write and fetch&add primitives in which all operations, including recovery, are lock-free.
Cite as

Liad Nahum, Hagit Attiya, Ohad Ben-Baruch, and Danny Hendler. Recoverable and Detectable Fetch&Add. In 25th International Conference on Principles of Distributed Systems (OPODIS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 217, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{nahum_et_al:LIPIcs.OPODIS.2021.29,
  author =	{Nahum, Liad and Attiya, Hagit and Ben-Baruch, Ohad and Hendler, Danny},
  title =	{{Recoverable and Detectable Fetch\&Add}},
  booktitle =	{25th International Conference on Principles of Distributed Systems (OPODIS 2021)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-219-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{217},
  editor =	{Bramas, Quentin and Gramoli, Vincent and Milani, Alessia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2021.29},
  URN =		{urn:nbn:de:0030-drops-158043},
  doi =		{10.4230/LIPIcs.OPODIS.2021.29},
  annote =	{Keywords: Multi-core algorithms, persistent memory, non-volatile memory}
}
Document
DOI: 10.4230/LIPIcs.DISC.2021.7
Impossibility of Strongly-Linearizable Message-Passing Objects via Simulation by Single-Writer Registers

Authors: Hagit Attiya, Constantin Enea, and Jennifer L. Welch

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)

Abstract
A key way to construct complex distributed systems is through modular composition of linearizable concurrent objects. A prominent example is shared registers, which have crash-tolerant implementations on top of message-passing systems, allowing the advantages of shared memory to carry over to message-passing. Yet linearizable registers do not always behave properly when used inside randomized programs. A strengthening of linearizability, called strong linearizability, has been shown to preserve probabilistic behavior, as well as other "hypersafety" properties. In order to exploit composition and abstraction in message-passing systems, it is crucial to know whether there exist strongly-linearizable implementations of registers in message-passing. This paper answers the question in the negative: there are no strongly-linearizable fault-tolerant message-passing implementations of multi-writer registers, max-registers, snapshots or counters. This result is proved by reduction from the corresponding result by Helmi et al. The reduction is a novel extension of the BG simulation that connects shared-memory and message-passing, supports long-lived objects, and preserves strong linearizability. The main technical challenge arises from the discrepancy between the potentially minuscule fraction of failures to be tolerated in the simulated message-passing algorithm and the large fraction of failures that can afflict the simulating shared-memory system. The reduction is general and can be viewed as the inverse of the ABD simulation of shared memory in message-passing.
Cite as

Hagit Attiya, Constantin Enea, and Jennifer L. Welch. Impossibility of Strongly-Linearizable Message-Passing Objects via Simulation by Single-Writer Registers. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2021.7,
  author =	{Attiya, Hagit and Enea, Constantin and Welch, Jennifer L.},
  title =	{{Impossibility of Strongly-Linearizable Message-Passing Objects via Simulation by Single-Writer Registers}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.7},
  URN =		{urn:nbn:de:0030-drops-148096},
  doi =		{10.4230/LIPIcs.DISC.2021.7},
  annote =	{Keywords: Concurrent Objects, Message-passing systems, Strong linearizability, Impossibility proofs, BG simulation, Shared registers}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2020.16
Optimal Resilience in Systems That Mix Shared Memory and Message Passing

Authors: Hagit Attiya, Sweta Kumari, and Noa Schiller

Published in: LIPIcs, Volume 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020)

Abstract
We investigate the minimal number of failures that can partition a system where processes communicate both through shared memory and by message passing. We prove that this number precisely captures the resilience that can be achieved by algorithms that implement a variety of shared objects, like registers and atomic snapshots, and solve common tasks, like randomized consensus, approximate agreement and renaming. This has implications for the m&m-model of [Aguilera et al., 2018] and for the hybrid, cluster-based model of [Damien Imbs and Michel Raynal, 2013; Michel Raynal and Jiannong Cao, 2019].
Cite as

Hagit Attiya, Sweta Kumari, and Noa Schiller. Optimal Resilience in Systems That Mix Shared Memory and Message Passing. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2020.16,
  author =	{Attiya, Hagit and Kumari, Sweta and Schiller, Noa},
  title =	{{Optimal Resilience in Systems That Mix Shared Memory and Message Passing}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{16:1--16:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-176-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{184},
  editor =	{Bramas, Quentin and Oshman, Rotem and Romano, Paolo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.16},
  URN =		{urn:nbn:de:0030-drops-135019},
  doi =		{10.4230/LIPIcs.OPODIS.2020.16},
  annote =	{Keywords: fault resilience, m\&m model, cluster-based model, randomized consensus, approximate agreement, renaming, register implementations, atomic snapshots}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2020.18
Locally Solvable Tasks and the Limitations of Valency Arguments

Authors: Hagit Attiya, Armando Castañeda, and Sergio Rajsbaum

Published in: LIPIcs, Volume 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020)

Abstract
An elegant strategy for proving impossibility results in distributed computing was introduced in the celebrated FLP consensus impossibility proof. This strategy is local in nature as at each stage, one configuration of a hypothetical protocol for consensus is considered, together with future valencies of possible extensions. This proof strategy has been used in numerous situations related to consensus, leading one to wonder why it has not been used in impossibility results of two other well-known tasks: set agreement and renaming. This paper provides an explanation of why impossibility proofs of these tasks have been of a global nature. It shows that a protocol can always solve such tasks locally, in the following sense. Given a configuration and all its future valencies, if a single successor configuration is selected, then the protocol can reveal all decisions in this branch of executions, satisfying the task specification. This result is shown for both set agreement and renaming, implying that there are no local impossibility proofs for these tasks.
Cite as

Hagit Attiya, Armando Castañeda, and Sergio Rajsbaum. Locally Solvable Tasks and the Limitations of Valency Arguments. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2020.18,
  author =	{Attiya, Hagit and Casta\~{n}eda, Armando and Rajsbaum, Sergio},
  title =	{{Locally Solvable Tasks and the Limitations of Valency Arguments}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-176-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{184},
  editor =	{Bramas, Quentin and Oshman, Rotem and Romano, Paolo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.18},
  URN =		{urn:nbn:de:0030-drops-135037},
  doi =		{10.4230/LIPIcs.OPODIS.2020.18},
  annote =	{Keywords: Wait-freedom, Set agreement, Weak symmetry breaking, Impossibility proofs}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.DISC.2020
LIPIcs, Volume 179, DISC 2020, Complete Volume

Authors: Hagit Attiya

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

Abstract
LIPIcs, Volume 179, DISC 2020, Complete Volume
Cite as

34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 1-768, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{attiya:LIPIcs.DISC.2020,
  title =	{{LIPIcs, Volume 179, DISC 2020, Complete Volume}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{1--768},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020},
  URN =		{urn:nbn:de:0030-drops-130777},
  doi =		{10.4230/LIPIcs.DISC.2020},
  annote =	{Keywords: LIPIcs, Volume 179, DISC 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.DISC.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Hagit Attiya

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{attiya:LIPIcs.DISC.2020.0,
  author =	{Attiya, Hagit},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020.0},
  URN =		{urn:nbn:de:0030-drops-130787},
  doi =		{10.4230/LIPIcs.DISC.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.2
Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs That Use Concurrent Objects

Authors: Hagit Attiya and Constantin Enea

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

Abstract
It has been observed that linearizability, the prevalent consistency condition for implementing concurrent objects, does not preserve some probability distributions. A stronger condition, called strong linearizability has been proposed, but its study has been somewhat ad-hoc. This paper investigates strong linearizability by casting it in the context of observational refinement of objects. We present a strengthening of observational refinement, which generalizes strong linearizability, obtaining several important implications. When a concrete concurrent object refines another, more abstract object - often sequential - the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This means that trace properties of a program using the concrete object can be proved by considering the program with the abstract object. This, however, does not hold for hyperproperties, including many security properties and probability distributions of events. We define strong observational refinement, a strengthening of refinement that preserves hyperproperties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability. This implies that strong linearizability is also equivalent to forward simulation, and shows that strongly linearizable implementations can be composed both horizontally (i.e., locality) and vertically (i.e., with instantiation). For situations where strongly linearizable implementations do not exist (or are less efficient), we argue that reasoning about hyperproperties of programs can be simplified by strong observational refinement of non-atomic abstract objects.
Cite as

Hagit Attiya and Constantin Enea. Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs That Use Concurrent Objects. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.DISC.2019.2,
  author =	{Attiya, Hagit and Enea, Constantin},
  title =	{{Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs That Use Concurrent Objects}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.2},
  URN =		{urn:nbn:de:0030-drops-113095},
  doi =		{10.4230/LIPIcs.DISC.2019.2},
  annote =	{Keywords: Concurrent Objects, Linearizability, Hyperproperties, Forward Simulations}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.24
Privatization-Safe Transactional Memories

Authors: Artem Khyzha, Hagit Attiya, and Alexey Gotsman

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

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

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

Copy BibTex To Clipboard

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

Authors: Hagit Attiya and Arie Fouren

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract
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.
Cite as

Hagit Attiya and Arie Fouren. Lower Bounds on the Amortized Time Complexity of Shared Objects. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2017.16,
  author =	{Attiya, Hagit and Fouren, Arie},
  title =	{{Lower Bounds on the Amortized Time Complexity of Shared Objects}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.16},
  URN =		{urn:nbn:de:0030-drops-86513},
  doi =		{10.4230/LIPIcs.OPODIS.2017.16},
  annote =	{Keywords: monotone objects, stacks and queues, trees, step complexity, remote memory references}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2017.18
Remote Memory References at Block Granularity

Authors: Hagit Attiya and Gili Yavneh

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract
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.
Cite as

Hagit Attiya and Gili Yavneh. Remote Memory References at Block Granularity. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2017.18,
  author =	{Attiya, Hagit and Yavneh, Gili},
  title =	{{Remote Memory References at Block Granularity}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.18},
  URN =		{urn:nbn:de:0030-drops-86538},
  doi =		{10.4230/LIPIcs.OPODIS.2017.18},
  annote =	{Keywords: false sharing, cache coherence, distributed shared memory, NP-hardness}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2015.31
Nontrivial and Universal Helping for Wait-Free Queues and Stacks

Authors: Hagit Attiya, Armando Castaneda, and Danny Hendler

Published in: LIPIcs, Volume 46, 19th International Conference on Principles of Distributed Systems (OPODIS 2015)

Abstract
This paper studies two approaches to formalize helping in wait-free implementations of shared objects. The first approach is based on operation valency, and it allows us to make the important distinction between trivial and nontrivial helping. We show that a wait-free implementation of a queue from common2 objects (e.g., Test&Set) requires nontrivial helping. In contrast, there is a wait-free implementation of a stack from Common2 objects with only trivial helping. This separation might shed light on the difficulty of implementing a queue from Common2 objects. The other approach formalizes the helping mechanism employed by Herlihy's universal wait-free construction and is based on having an operation by one process restrict the possible linearizations of operations by other processes. We show that objects possessing such universal helping can be used to solve consensus.
Cite as

Hagit Attiya, Armando Castaneda, and Danny Hendler. Nontrivial and Universal Helping for Wait-Free Queues and Stacks. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2015.31,
  author =	{Attiya, Hagit and Castaneda, Armando and Hendler, Danny},
  title =	{{Nontrivial and Universal Helping for Wait-Free Queues and Stacks}},
  booktitle =	{19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-98-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{46},
  editor =	{Anceaume, Emmanuelle and Cachin, Christian and Potop-Butucaru, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2015.31},
  URN =		{urn:nbn:de:0030-drops-66201},
  doi =		{10.4230/LIPIcs.OPODIS.2015.31},
  annote =	{Keywords: helping, wait-free, nonblocking, queues, stacks, common2}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2015.36
Poly-Logarithmic Adaptive Algorithms Require Unconditional Primitives

Authors: Hagit Attiya and Arie Fouren

Published in: LIPIcs, Volume 46, 19th International Conference on Principles of Distributed Systems (OPODIS 2015)

Abstract
This paper studies the step complexity of adaptive algorithms using primitives stronger than reads and writes. We first consider unconditional primitives, like fetch&inc, which modify the value of the register to which they are applied, regardless of its current value. Unconditional primitives admit snapshot algorithms with O(log(k)) step complexity, where k is the total or the point contention. These algorithms combine a renaming algorithm with a mechanism for propagating values so they can be quickly collected. When only conditional primitives, e.g., compare&swap or LL/SC, are used (in addition to reads and writes), we show that any collect algorithm must perform Omega(k) steps, in an execution with total contention k in O(log(log(n))). The lower bound applies for snapshot and renaming, both one-shot and long-lived. Note that there are snapshot algorithms whose step complexity is polylogarithmic in n using only reads and writes, but there are no adaptive algorithms whose step complexity is polylogarithmic in the contention, even when compare&swap and LL/SC are used.
Cite as

Hagit Attiya and Arie Fouren. Poly-Logarithmic Adaptive Algorithms Require Unconditional Primitives. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2015.36,
  author =	{Attiya, Hagit and Fouren, Arie},
  title =	{{Poly-Logarithmic Adaptive Algorithms Require Unconditional Primitives}},
  booktitle =	{19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-98-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{46},
  editor =	{Anceaume, Emmanuelle and Cachin, Christian and Potop-Butucaru, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2015.36},
  URN =		{urn:nbn:de:0030-drops-66793},
  doi =		{10.4230/LIPIcs.OPODIS.2015.36},
  annote =	{Keywords: collect, atomic snapshot, renaming, fetch\&inc, compare\&swap}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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