12 Search Results for "Johnen, Colette"

Document
DOI: 10.4230/LIPIcs.OPODIS.2025.21
Solving Tasks with Fewer Registers Than Processes

Authors: Eli Gafni, Giuliano Losa, Michel Raynal, and Gadi Taubenfeld

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
This paper studies distributed-computing tasks through the lens of space complexity in the read/write wait-free model, defined as the number of multi-reader-multi-writer atomic read/write registers needed to solve a task using a wait-free algorithm. Surprisingly, even though the read/write wait-free model is at the foundation of distributed computing, previous work on space complexity has focused on synchronization primitives stronger than read/write registers or on weaker progress conditions. The paper reveals that the read/write wait-free model offers a rich space-complexity landscape: (1) assuming non-anonymous processes, it shows that there is an infinite hierarchy of tasks of increasing space complexity; (2) it shows that space complexity separates anonymous from non-anonymous memory; (3) regardless of process or register anonymity, it exhibits a task of space complexity two, which is the minimal non-trivial space complexity; (4) finally, it shows that subcases of the adopt-commit task have different space complexity in non-anonymous memory under bounded wait-freedom.
Cite as

Eli Gafni, Giuliano Losa, Michel Raynal, and Gadi Taubenfeld. Solving Tasks with Fewer Registers Than Processes. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gafni_et_al:LIPIcs.OPODIS.2025.21,
  author =	{Gafni, Eli and Losa, Giuliano and Raynal, Michel and Taubenfeld, Gadi},
  title =	{{Solving Tasks with Fewer Registers Than Processes}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.21},
  URN =		{urn:nbn:de:0030-drops-251947},
  doi =		{10.4230/LIPIcs.OPODIS.2025.21},
  annote =	{Keywords: Asynchrony, Read/write registers, Wait-freedom, Tasks, Covering argument, Lower bound, Space complexity, Anonymous Processes, Anonymous Memory}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.17
Deterministic Synchronous Self-Stabilizing BFS Construction with Constant Space Complexity

Authors: Lélia Blin, Franck Petit, and Sébastien Tixeuil

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
In this paper, we resolve a long-standing open problem in self-stabilization asking whether it is possible to construct a spanning tree using constant memory per node in a synchronous semi-uniform networks, i.e., networks in which one node is distinguished. We design a synchronous self-stabilizing algorithm that constructs a breadth-first search (BFS) tree in any anonymous semi-uniform network using only a constant number of bits of memory per node. Crucially, our approach operates without any prior knowledge of global network parameters such as maximum degree, diameter, or number of nodes. In contrast to traditional self-stabilizing methods - such as pointer-to-neighbors, distance-to-root, or identifiers - that are unsuitable under strict memory constraints, our solution employs an innovative constant-space token dissemination mechanism. This mechanism effectively eliminates cycles and rectifies errors in the BFS structure, ensuring both correctness and memory efficiency. The proposed algorithm not only meets the stringent requirements of memory-constrained distributed systems, but also opens new avenues for research in the design of self-stabilizing protocols under severe resource limitations: constant space-complexity may not systematically prevent the existence of self-stabilizing algorithms for important non-trivial tasks.
Cite as

Lélia Blin, Franck Petit, and Sébastien Tixeuil. Deterministic Synchronous Self-Stabilizing BFS Construction with Constant Space Complexity. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{blin_et_al:LIPIcs.DISC.2025.17,
  author =	{Blin, L\'{e}lia and Petit, Franck and Tixeuil, S\'{e}bastien},
  title =	{{Deterministic Synchronous Self-Stabilizing BFS Construction with Constant Space Complexity}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{17:1--17:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.17},
  URN =		{urn:nbn:de:0030-drops-248349},
  doi =		{10.4230/LIPIcs.DISC.2025.17},
  annote =	{Keywords: Distributed algorithms, fault-tolerance, transient faults, self-stabilization, memory optimization}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.19
Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability

Authors: Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Synchronous unison is a classical clock synchronization problem in distributed computing, and especially in self-stabilization. This paper explores the self-stabilization of a synchronous unison algorithm proposed by Arora et al. using a propositional satisfiability-based approach. We give a logical formulation of the algorithm. This formulation includes the uniqueness of clock values at each node, the updates of clocks based on the minimum clock value in the neighborhood, and the detection of convergence or divergence. To optimize the models, additional constraints are introduced to reduce redundant cases of initial configurations to be analyzed. Our approach not only verifies the algorithm’s behaviour but also offers insights into enhancing its robustness and applicability to broader distributed systems.
Cite as

Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoualdia_et_al:LIPIcs.CP.2025.19,
  author =	{Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
  title =	{{Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{19:1--19:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.19},
  URN =		{urn:nbn:de:0030-drops-238806},
  doi =		{10.4230/LIPIcs.CP.2025.19},
  annote =	{Keywords: Self-stabilization, Synchronous Unison, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.30
Being Efficient in Time, Space, and Workload: a Self-Stabilizing Unison and Its Consequences

Authors: Stéphane Devismes, David Ilcinkas, Colette Johnen, and Frédéric Mazoit

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We present a self-stabilizing algorithm for the unison problem which is efficient in time, workload, and space in a weak model. Precisely, our algorithm is defined in the atomic-state model and works in anonymous asynchronous connected networks in which even local ports are unlabeled. It makes no assumption on the daemon and thus stabilizes under the weakest one: the distributed unfair daemon. In an n-node network of diameter D and assuming the knowledge B ≥ 2D+2, our algorithm only requires Θ(log(B)) bits per node and is fully polynomial as it stabilizes in at most 2D+2 rounds and O(min(n²B, n³)) moves. In particular, it is the first self-stabilizing unison for arbitrary asynchronous anonymous networks achieving an asymptotically optimal stabilization time in rounds using a bounded memory at each node. Furthermore, we show that our solution can be used to efficiently simulate synchronous self-stabilizing algorithms in asynchronous environments. For example, this simulation allows us to design a new state-of-the-art algorithm solving both the leader election and the BFS (Breadth-First Search) spanning tree construction in any identified connected network which, to the best of our knowledge, beats all existing solutions in the literature.
Cite as

Stéphane Devismes, David Ilcinkas, Colette Johnen, and Frédéric Mazoit. Being Efficient in Time, Space, and Workload: a Self-Stabilizing Unison and Its Consequences. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{devismes_et_al:LIPIcs.STACS.2025.30,
  author =	{Devismes, St\'{e}phane and Ilcinkas, David and Johnen, Colette and Mazoit, Fr\'{e}d\'{e}ric},
  title =	{{Being Efficient in Time, Space, and Workload: a Self-Stabilizing Unison and Its Consequences}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.30},
  URN =		{urn:nbn:de:0030-drops-228568},
  doi =		{10.4230/LIPIcs.STACS.2025.30},
  annote =	{Keywords: Self-stabilization, unison, time complexity, synchronizer}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.6
DULL: A Fast Scalable Detectable Unrolled Lock-Based Linked List

Authors: Ahmed Fahmy and Wojciech Golab

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
Persistent memory (PM) has emerged as a promising technology that enables data structures to preserve their consistent state after recovering from system failures. Detectable data structures have been proposed to detect the response of the last operation of a crashed process. Various lock-free detectable and recoverable concurrent data structures have been developed in the literature. However, designing detectable lock-based structures is challenging due to the need to preserve the correctness properties of the underlying locks, such as mutual exclusion and deadlock-freedom, across failures. Therefore, lock-based detectable and persistent data structures are not as common as lock-free structures. In this work, we introduce DULL: a fast, scalable and Detectable Unrolled Lock-based Linked list. This paper presents the design and implementation of DULL, along with an evaluation of its recoverability and scalability. Experimental Results show that DULL is several-fold faster than the competition in all workloads that involve updates. Moreover, as opposed to some of the previous works, our algorithm is scalable when the multiprocessor is oversubscribed. DULL is a demonstration of the feasibility of using lock-based data structures with detectability in PM environments. We believe that DULL opens up new research directions for designing and analyzing detectable lock-based data structures.
Cite as

Ahmed Fahmy and Wojciech Golab. DULL: A Fast Scalable Detectable Unrolled Lock-Based Linked List. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fahmy_et_al:LIPIcs.OPODIS.2024.6,
  author =	{Fahmy, Ahmed and Golab, Wojciech},
  title =	{{DULL: A Fast Scalable Detectable Unrolled Lock-Based Linked List}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.6},
  URN =		{urn:nbn:de:0030-drops-225429},
  doi =		{10.4230/LIPIcs.OPODIS.2024.6},
  annote =	{Keywords: detectability, lock-based, mutual exclusion, linked list, fault-tolerance, persistent memory, concurrency}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.18
Stabilizing Consensus Is Impossible in Lossy Iterated Immediate Snapshot Models

Authors: Stephan Felber and Hugo Rincon Galeana

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
A substantial portion of distributed computing research is dedicated to terminating problems like consensus and similar agreement problems. However, non-terminating problems have been intensively studied in the context of self-stabilizing distributed algorithms, where processes may start from arbitrary initial states and can tolerate arbitrary transient faults. In between lie stabilizing problems, where the processes start from a well-defined initial state, but do not need to decide irrevocably and are allowed to change their decision finitely often until a stable decision is eventually reached. Stabilizing consensus has been studied within the context of synchronous message adversaries. In particular, Charron-Bost and Moran showed that a necessary condition for stabilizing consensus is the existence of at least one process that reaches all others infinitely often (a perpetual broadcaster). However, it was left open whether this is also a sufficient condition for solving stabilizing consensus. In this paper, we introduce the novel Delayed Lossy-Link (DLL) model, and the Lossy Iterated Immediate Snapshot Model (LIIS), for which we show stabilizing consensus to be impossible. The DLL model is introduced as a variant of the well-known Lossy-Link model, which admits silence periods of arbitrary but finite length. The LIIS model is a variant of the Iterated Immediate Snapshot (IIS), model which admits finite length periods of at most f omission faults per layer. In particular, we show that stabilizing consensus is impossible even when f = 1. Our results show that even in a model with very strong connectivity, namely, the Iterated Immediate Snapshot (IIS) model, a single omission fault per layer effectively disables stabilizing consensus. Furthermore, since the DLL model always has a perpetual broadcaster, the mere existence of a perpetual broadcaster, even in a crash-free setting, is not sufficient for solving stabilizing consensus, negatively answering the open question posed by Charron-Bost and Moran.
Cite as

Stephan Felber and Hugo Rincon Galeana. Stabilizing Consensus Is Impossible in Lossy Iterated Immediate Snapshot Models. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{felber_et_al:LIPIcs.OPODIS.2024.18,
  author =	{Felber, Stephan and Rincon Galeana, Hugo},
  title =	{{Stabilizing Consensus Is Impossible in Lossy Iterated Immediate Snapshot Models}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.18},
  URN =		{urn:nbn:de:0030-drops-225544},
  doi =		{10.4230/LIPIcs.OPODIS.2024.18},
  annote =	{Keywords: distributed systems, dynamic networks, dynamic graphs, message adversaries, stabilizing consensus, asynchronous message passing}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.33
Self-Stabilizing Fully Adaptive Maximal Matching

Authors: Shimon Bitton, Yuval Emek, Taisuke Izumi, and Shay Kutten

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
A self-stabilizing randomized algorithm for mending maximal matching (MM) in synchronous networks is presented. Starting from a legal MM configuration and assuming that the network undergoes k faults or topology changes (that may occur in multiple batches), the algorithm is guaranteed to stabilize back to a legal MM configuration in time O(log k) in expectation and with high probability (in k), using constant size messages. The algorithm is simple to implement and is uniform in the sense that it does not assume unique identifiers, nor does it assume any global knowledge of the communication graph including its size. It relies on a generic probabilistic phase synchronization technique that may be useful for other self-stabilizing problems. The algorithm compares favorably with the existing self-stabilizing MM algorithms in terms of the dependence of its run-time on k, a.k.a. fully adaptive run-time. In fact, this dependence is asymptotically optimal for uniform algorithms that use constant size messages.
Cite as

Shimon Bitton, Yuval Emek, Taisuke Izumi, and Shay Kutten. Self-Stabilizing Fully Adaptive Maximal Matching. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bitton_et_al:LIPIcs.OPODIS.2024.33,
  author =	{Bitton, Shimon and Emek, Yuval and Izumi, Taisuke and Kutten, Shay},
  title =	{{Self-Stabilizing Fully Adaptive Maximal Matching}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.33},
  URN =		{urn:nbn:de:0030-drops-225698},
  doi =		{10.4230/LIPIcs.OPODIS.2024.33},
  annote =	{Keywords: self-stabilization, maximal matching, fully adaptive run-time, dynamic graphs}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.36
The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets

Authors: Petr Jančar and Jérôme Leroux

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

Abstract
A set of configurations H is a home-space for a set of configurations X of a Petri net if every configuration reachable from (any configuration in) X can reach (some configuration in) H. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations X, H, if H is a home-space for X. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when X is a singleton and H is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any linear set of configurations L we can effectively compute a semilinear set C of configurations, called a non-reachability core for L, such that for every set X the set L is not a home-space for X if, and only if, C is reachable from X. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.
Cite as

Petr Jančar and Jérôme Leroux. The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jancar_et_al:LIPIcs.CONCUR.2023.36,
  author =	{Jan\v{c}ar, Petr and Leroux, J\'{e}r\^{o}me},
  title =	{{The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{36:1--36: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.36},
  URN =		{urn:nbn:de:0030-drops-190300},
  doi =		{10.4230/LIPIcs.CONCUR.2023.36},
  annote =	{Keywords: Petri nets, home-space property, semilinear sets, Ackermannian complexity}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2022.4
Efficient Wait-Free Queue Algorithms with Multiple Enqueuers and Multiple Dequeuers

Authors: Colette Johnen, Adnane Khattabi, and Alessia Milani

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

Abstract
Despite the widespread usage of FIFO queues in distributed applications, designing efficient wait-free implementations of queues remains a challenge. The majority of wait-free queue implementations restrict either the number of dequeuers or the number of enqueuers that can operate on the queue, even when they use strong synchronization primitives, like the Compare&Swap. If we do not limit the number of processes that can perform enqueue and dequeue operations, the best-known upper bound on the worst case step complexity for a wait-free queue is given by [Khanchandani and Wattenhofer, 2018]. In particular, they present an implementation of a multiple dequeuer multiple enqueuer wait-free queue whose worst case step complexity is in O(√n), where n is the number of processes. In this work, we investigate whether it is possible to improve this bound. In particular, we present a wait-free FIFO queue implementation that supports n enqueuers and k dequeuers where the worst case step complexity of an Enqueue operation is in O(log n) and of a Dequeue operation is in O(k log n). Then, we show that if the semantics of the queue can be relaxed, by allowing concurrent Dequeue operations to retrieve the same element, then we can achieve O(log n) worst-case step complexity for both the Enqueue and Dequeue operations.
Cite as

Colette Johnen, Adnane Khattabi, and Alessia Milani. Efficient Wait-Free Queue Algorithms with Multiple Enqueuers and Multiple Dequeuers. In 26th International Conference on Principles of Distributed Systems (OPODIS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 253, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{johnen_et_al:LIPIcs.OPODIS.2022.4,
  author =	{Johnen, Colette and Khattabi, Adnane and Milani, Alessia},
  title =	{{Efficient Wait-Free Queue Algorithms with Multiple Enqueuers and Multiple Dequeuers}},
  booktitle =	{26th International Conference on Principles of Distributed Systems (OPODIS 2022)},
  pages =	{4:1--4:19},
  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.4},
  URN =		{urn:nbn:de:0030-drops-176240},
  doi =		{10.4230/LIPIcs.OPODIS.2022.4},
  annote =	{Keywords: Distributed computing, distributed algorithms, FIFO queue, shared memory, fault tolerance, concurrent data structures, relaxed specifications, complexity}
}
Document
DOI: 10.4230/LITES.8.2.2
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:36},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  URN =		{urn:nbn:de:0030-drops-192942},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2016.10
Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps

Authors: Stéphane Devismes, David Ilcinkas, and Colette Johnen

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
We deal with the problem of maintaining a shortest-path tree rooted at some process r in a network that may be disconnected after topological changes. The goal is then to maintain a shortest-path tree rooted at r in its connected component, V_r, and make all processes of other components detecting that r is not part of their connected component. We propose, in the composite atomicity model, a silent self-stabilizing algorithm for this problem working in semi-anonymous networks under the distributed unfair daemon (the most general daemon) without requiring any a priori knowledge about global parameters of the network. This is the first algorithm for this problem that is proven to achieve a polynomial stabilization time in steps. Namely, we exhibit a bound in O(W_{max} * n_{maxCC}^3 * n), where W_{max} is the maximum weight of an edge, n_{maxCC} is the maximum number of non-root processes in a connected component, and n is the number of processes. The stabilization time in rounds is at most 3n_{maxCC} + D, where D is the hop-diameter of V_r.
Cite as

Stéphane Devismes, David Ilcinkas, and Colette Johnen. Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{devismes_et_al:LIPIcs.OPODIS.2016.10,
  author =	{Devismes, St\'{e}phane and Ilcinkas, David and Johnen, Colette},
  title =	{{Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.10},
  URN =		{urn:nbn:de:0030-drops-70792},
  doi =		{10.4230/LIPIcs.OPODIS.2016.10},
  annote =	{Keywords: distributed algorithm, self-stabilization, routing algorithm, shortest path, disconnected network, shortest-path tree}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2015.12
On the Uncontended Complexity of Anonymous Consensus

Authors: Claire Capdevielle, Colette Johnen, Petr Kuznetsov, and Alessia Milani

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

Abstract
Consensus is one of the central distributed abstractions. By enabling a collection of processes to agree on one of the values they propose, consensus can be used to implement any generic replicated service in a consistent and fault-tolerant way. In this paper, we study uncontended complexity of anonymous consensus algorithms, counting the number of memory locations used and the number of memory updates performed in operations that encounter no contention. We assume that contention-free operations on a consensus object perform "fast" reads and writes, and resort to more expensive synchronization primitives, such as CAS, only when contention is detected. We call such concurrent implementations interval-solo-fast and derive one of the first nontrivial tight bounds on space complexity of anonymous interval-solo-fast consensus.
Cite as

Claire Capdevielle, Colette Johnen, Petr Kuznetsov, and Alessia Milani. On the Uncontended Complexity of Anonymous Consensus. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{capdevielle_et_al:LIPIcs.OPODIS.2015.12,
  author =	{Capdevielle, Claire and Johnen, Colette and Kuznetsov, Petr and Milani, Alessia},
  title =	{{On the Uncontended Complexity of Anonymous Consensus}},
  booktitle =	{19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
  pages =	{12:1--12: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.12},
  URN =		{urn:nbn:de:0030-drops-66034},
  doi =		{10.4230/LIPIcs.OPODIS.2015.12},
  annote =	{Keywords: space and time complexity, lower bounds, consensus, interval contention, solo-fast}
}
  • Refine by Type
  • 12 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 6 2025
  • 2 2023
  • 1 2022
  • 1 2017
  • Show More...

  • Refine by Author
  • 4 Johnen, Colette
  • 3 Devismes, Stéphane
  • 2 Ilcinkas, David
  • 2 Milani, Alessia
  • 2 Tixeuil, Sébastien
  • Show More...

  • Refine by Series/Journal
  • 11 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 5 Theory of computation → Distributed algorithms
  • 3 Theory of computation → Distributed computing models
  • 2 Computer systems organization → Fault-tolerant network topologies
  • 2 Theory of computation → Design and analysis of algorithms
  • 2 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 3 self-stabilization
  • 2 Self-stabilization
  • 2 distributed algorithm
  • 2 dynamic graphs
  • 2 fault-tolerance
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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