7 Search Results for "Castaneda, Armando"

Document
DOI: 10.4230/DagRep.13.7.34
Epistemic and Topological Reasoning in Distributed Systems (Dagstuhl Seminar 23272)

Authors: Armando Castañeda, Hans van Ditmarsch, Roman Kuznets, Yoram Moses, and Ulrich Schmid

Published in: Dagstuhl Reports, Volume 13, Issue 7 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23272 "Epistemic and Topological Reasoning in Distributed Systems." The seminar brought together experts in combinatorial topology and epistemic logic interested in distributed systems, with the aim of exploring the directions that the recent interaction between those approaches can take, identifying challenges and opportunities.
Cite as

Armando Castañeda, Hans van Ditmarsch, Roman Kuznets, Yoram Moses, and Ulrich Schmid. Epistemic and Topological Reasoning in Distributed Systems (Dagstuhl Seminar 23272). In Dagstuhl Reports, Volume 13, Issue 7, pp. 34-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{castaneda_et_al:DagRep.13.7.34,
  author =	{Casta\~{n}eda, Armando and van Ditmarsch, Hans and Kuznets, Roman and Moses, Yoram and Schmid, Ulrich},
  title =	{{Epistemic and Topological Reasoning in Distributed Systems (Dagstuhl Seminar 23272)}},
  pages =	{34--65},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{7},
  editor =	{Casta\~{n}eda, Armando and van Ditmarsch, Hans and Kuznets, Roman and Moses, Yoram and Schmid, Ulrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.7.34},
  URN =		{urn:nbn:de:0030-drops-197742},
  doi =		{10.4230/DagRep.13.7.34},
  annote =	{Keywords: combinatorial topology, distributed systems, epistemic logic, multi-agent systems, interpreted systems, dynamic epistemic logic, simplicial semantics, knowledge-based approach, distributed computing}
}
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-dev.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
DOI: 10.4230/LIPIcs.DISC.2022.12
Liveness and Latency of Byzantine State-Machine Replication

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

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

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

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

Copy BibTex To Clipboard

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

Authors: Armando Castañeda and Miguel Piña

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

Abstract
It is known that any algorithm for work-stealing in the standard asynchronous shared memory model must use expensive Read-After-Write synchronization patterns or atomic Read-Modify-Write instructions. There have been proposed algorithms for relaxations in the standard model and algorithms in restricted models that avoid the impossibility result, but only in some operations. This paper considers work-stealing with multiplicity, a relaxation in which every task is taken by at least one operation, with the requirement that any process can extract a task at most once. Two versions of the relaxation are considered and two fully Read/Write algorithms are presented in the standard asynchronous shared memory model, both devoid of Read-After-Write synchronization patterns in all its operations, the second algorithm additionally being fully fence-free, namely, no specific ordering among the algorithm’s instructions is required, beyond what is implied by data dependence. To our knowledge, these are the first algorithms for work-stealing possessing all these properties. Our algorithms are also wait-free solutions of relaxed versions of single-enqueue multi-dequeuer queues. The algorithms are obtained by reducing work-stealing with multiplicity and weak multiplicity to MaxRegister and RangeMaxRegister, a relaxation of MaxRegister which might be of independent interest. An experimental evaluation shows that our fully fence-free algorithm exhibits better performance than Cilk THE, Chase-Lev and Idempotent Work-Stealing algorithms.
Cite as

Armando Castañeda and Miguel Piña. Fully Read/Write Fence-Free Work-Stealing with Multiplicity. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{castaneda_et_al:LIPIcs.DISC.2021.16,
  author =	{Casta\~{n}eda, Armando and Pi\~{n}a, Miguel},
  title =	{{Fully Read/Write Fence-Free Work-Stealing with Multiplicity}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{16:1--16:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.16},
  URN =		{urn:nbn:de:0030-drops-148181},
  doi =		{10.4230/LIPIcs.DISC.2021.16},
  annote =	{Keywords: Correctness condition, Linearizability, Nonblocking, Relaxed data type, Set-linearizability, Wait-freedom, Work-stealing}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2020.13
Relaxed Queues and Stacks from Read/Write Operations

Authors: Armando Castañeda, Sergio Rajsbaum, and Michel Raynal

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

Abstract
Considering asynchronous shared memory systems in which any number of processes may crash, this work identifies and formally defines relaxations of queues and stacks that can be non-blocking or wait-free while being implemented using only read/write operations. Set-linearizability and Interval-linearizability are used to specify the relaxations formally, and precisely identify the subset of executions which preserve the original sequential behavior. The relaxations allow for an item to be returned more than once by different operations, but only in case of concurrency; we call such a property multiplicity. The stack implementation is wait-free, while the queue implementation is non-blocking. Interval-linearizability is used to describe a queue with multiplicity, with the additional relaxation that a dequeue operation can return weak-empty, which means that the queue might be empty. We present a read/write wait-free interval-linearizable algorithm of a concurrent queue. As far as we know, this work is the first that provides formalizations of the notions of multiplicity and weak-emptiness, which can be implemented on top of read/write registers only.
Cite as

Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Relaxed Queues and Stacks from Read/Write Operations. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{castaneda_et_al:LIPIcs.OPODIS.2020.13,
  author =	{Casta\~{n}eda, Armando and Rajsbaum, Sergio and Raynal, Michel},
  title =	{{Relaxed Queues and Stacks from Read/Write Operations}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{13:1--13:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.13},
  URN =		{urn:nbn:de:0030-drops-134983},
  doi =		{10.4230/LIPIcs.OPODIS.2020.13},
  annote =	{Keywords: Asynchrony, Correctness condition, Linearizability, Nonblocking, Process crash, Relaxed data type, Set-linearizability, Wait-freedom, Work-stealing}
}
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-dev.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
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-dev.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}
}
  • Refine by Author
  • 5 Castañeda, Armando
  • 3 Attiya, Hagit
  • 2 Rajsbaum, Sergio
  • 1 Bravo, Manuel
  • 1 Castaneda, Armando
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Distributed computing models
  • 4 Computing methodologies → Distributed algorithms
  • 3 Computing methodologies → Concurrent algorithms
  • 3 Theory of computation → Concurrent algorithms
  • 3 Theory of computation → Distributed algorithms
  • Show More...

  • Refine by Keyword
  • 3 Wait-freedom
  • 2 Correctness condition
  • 2 Linearizability
  • 2 Nonblocking
  • 2 Relaxed data type
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 3 2021
  • 1 2016
  • 1 2022
  • 1 2023
  • 1 2024

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