Document

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

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.

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

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

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

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

Invited Talk

**Published in:** LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Much discussion exists about what is computation, but less about is a computational problem. Turing’s definition of computation was based on computing functions. When we move from sequential computing to interactive computing, discussions concentrate on computations that do not terminate, overlooking notions of distributed problems. Many models where concurrency happens have been proposed, ranging from those equivalent to a Turing machine, to those where much heated discussion has taken place, claiming that interactive models are fundamentally different from Turing machines.
It is argued here that there is no need to go all the way to non-terminating interaction, to appreciate how different distributed computation is from sequential computation. The discussion concentrates on the various ways that exist of representing a distributed decision problem. Each process of a distributed system starts with an initial private input value, and after communicating with other processes in the system, produces a local output value. An input/output relation is needed, to specify which output values are legal for a particular assignment of input values to the processes.
An overview is provided of some results that show how rich the topic of distributed decision problems can be, when asynchronous processes can fail, but mostly independent of particular models of distributed computing and their many intricate details (types of failures and of communication). We are in a world very different from that of the functions of sequential computation; moving away from the world of graphs beyond binary relations, to the world of simplicial complexes.

Sergio Rajsbaum. Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 3:1-3:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{rajsbaum:LIPIcs.CONCUR.2022.3, author = {Rajsbaum, Sergio}, title = {{Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations}}, booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)}, pages = {3:1--3:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-246-4}, ISSN = {1868-8969}, year = {2022}, volume = {243}, editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.3}, URN = {urn:nbn:de:0030-drops-170660}, doi = {10.4230/LIPIcs.CONCUR.2022.3}, annote = {Keywords: Distributed decision tasks, simplicial complex, linearizability, interval-linearizability, Arrow’s impossibility, Speedup theorems} }

Document

**Published in:** LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

The standard semantics of multi-agent epistemic logic S5_n is based on Kripke models whose accessibility relations are reflexive, symmetric and transitive. This one dimensional structure contains implicit higher-dimensional information beyond pairwise interactions, that we formalized as pure simplicial models in a previous work in Information and Computation 2021 [Éric Goubault et al., 2021]. Here we extend the theory to encompass simplicial models that are not necessarily pure. The corresponding class of Kripke models are those where the accessibility relation is symmetric and transitive, but might not be reflexive. Such models correspond to the epistemic logic KB4_n. Impure simplicial models arise in situations where two possible worlds may not have the same set of agents. We illustrate it with distributed computing examples of synchronous systems where processes may crash.

Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum. A Simplicial Model for KB4_n: Epistemic Logic with Agents That May Die. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.STACS.2022.33, author = {Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio}, title = {{A Simplicial Model for KB4\underlinen: Epistemic Logic with Agents That May Die}}, booktitle = {39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)}, pages = {33:1--33:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-222-8}, ISSN = {1868-8969}, year = {2022}, volume = {219}, editor = {Berenbrink, Petra and Monmege, Benjamin}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.33}, URN = {urn:nbn:de:0030-drops-158434}, doi = {10.4230/LIPIcs.STACS.2022.33}, annote = {Keywords: Epistemic logic, Simplicial complexes, Distributed computing} }

Document

**Published in:** LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)

The celebrated 1999 Asynchronous Computability Theorem (ACT) of Herlihy and Shavit characterized distributed tasks that are wait-free solvable and uncovered deep connections with combinatorial topology. We provide an alternative characterization of those tasks by means of the novel concept of continuous tasks, which have an input/output specification that is a continuous function between the geometric realizations of the input and output complex: We state and prove a precise characterization theorem (CACT) for wait-free solvable tasks in terms of continuous tasks. Its proof utilizes a novel chromatic version of a foundational result in algebraic topology, the simplicial approximation theorem, which is also proved in this paper. Apart from the alternative proof of the ACT implied by our CACT, we also demonstrate that continuous tasks have an expressive power that goes beyond classic task specifications, and hence open up a promising venue for future research: For the well-known approximate agreement task, we show that one can easily encode the desired proportion of the occurrence of specific outputs, namely, exact agreement, in the continuous task specification.

Hugo Rincon Galeana, Sergio Rajsbaum, and Ulrich Schmid. Continuous Tasks and the Asynchronous Computability Theorem. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 73:1-73:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{galeana_et_al:LIPIcs.ITCS.2022.73, author = {Galeana, Hugo Rincon and Rajsbaum, Sergio and Schmid, Ulrich}, title = {{Continuous Tasks and the Asynchronous Computability Theorem}}, booktitle = {13th Innovations in Theoretical Computer Science Conference (ITCS 2022)}, pages = {73:1--73:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-217-4}, ISSN = {1868-8969}, year = {2022}, volume = {215}, editor = {Braverman, Mark}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.73}, URN = {urn:nbn:de:0030-drops-156696}, doi = {10.4230/LIPIcs.ITCS.2022.73}, annote = {Keywords: Wait-free computability, topology, distributed computing, decision tasks, shared memory} }

Document

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

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.

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.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

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

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.

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

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

We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k<l, indicating when the cardinality of the set of inputs becomes "small" or "large", respectively. We study the solvability of this task depending on those two parameters. First, we show that the task is solvable whenever k+2 <= l. For the remaining cases (l = k+1), we use various combinatorial topology techniques to obtain two impossibility results: the task is unsolvable if either k <= n/2 or n-k is odd. The remaining cases are still open.

Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum. Wait-Free Solvability of Equality Negation Tasks. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2019.21, author = {Goubault, \'{E}ric and Lazi\'{c}, Marijana and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio}, title = {{Wait-Free Solvability of Equality Negation Tasks}}, booktitle = {33rd International Symposium on Distributed Computing (DISC 2019)}, pages = {21:1--21:16}, 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.21}, URN = {urn:nbn:de:0030-drops-113288}, doi = {10.4230/LIPIcs.DISC.2019.21}, annote = {Keywords: Equality negation, distributed computability, combinatorial topology} }

Document

**Published in:** Dagstuhl Reports, Volume 8, Issue 5 (2019)

The Dagstuhl Seminar "Formal Methods and Fault-Tolerant
Distributed Computing: Forging an Alliance" took place May 22-25,
2018. Its goal was to strengthen the interaction between researchers
from formal methods and from distributed computing, and help the two
communities to better identify common research challenges.

Javier Esparza, Pierre Fraignaud, Anca Muscholl, and Sergio Rajsbaum. Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211). In Dagstuhl Reports, Volume 8, Issue 5, pp. 60-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{esparza_et_al:DagRep.8.5.60, author = {Esparza, Javier and Fraignaud, Pierre and Muscholl, Anca and Rajsbaum, Sergio}, title = {{Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211)}}, pages = {60--79}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2018}, volume = {8}, number = {5}, editor = {Esparza, Javier and Fraignaud, Pierre and Muscholl, Anca and Rajsbaum, Sergio}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.5.60}, URN = {urn:nbn:de:0030-drops-98933}, doi = {10.4230/DagRep.8.5.60}, annote = {Keywords: distributed computing, distributed systems, formal verification} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors, only if sufficiently many different verdicts can be emitted by each monitor. We revisit this impossibility result in the context of LTL semantics for RV. We show that employing the four-valued logic Rv-LTL will result in inconsistent distributed monitoring for some formulas. Our first main contribution is a family of logics, called Ltl2k+4, that refines Rv-Ltl incorporating 2k + 4 truth values, for each k >= 0. The truth values of Ltl2k+4 can be effectively used by each monitor to reach a consistent global set of verdicts for each given formula, provided k is sufficiently large. Our second main contribution is an algorithm for monitor construction enabling fault-tolerant distributed monitoring based on the aggregation of the individual verdicts by each monitor.

Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers. Decentralized Asynchronous Crash-Resilient Runtime Verification. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bonakdarpour_et_al:LIPIcs.CONCUR.2016.16, author = {Bonakdarpour, Borzoo and Fraigniaud, Pierre and Rajsbaum, Sergio and Rosenblueth, David A. and Travers, Corentin}, title = {{Decentralized Asynchronous Crash-Resilient Runtime Verification}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {16:1--16:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.16}, URN = {urn:nbn:de:0030-drops-61856}, doi = {10.4230/LIPIcs.CONCUR.2016.16}, annote = {Keywords: Runtime monitoring, Distributed algorithms, Fault-tolerance} }