Author name cluster

Matthieu Roy

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

I&C Journal 2023 Journal Article

Synchronous t-resilient consensus in arbitrary graphs

Armando Castañeda
Pierre Fraigniaud
Ami Paz
Sergio Rajsbaum
Matthieu Roy
Corentin Travers

We study the number of rounds needed to solve consensus in a synchronous network G where at most t nodes may fail by crashing. This problem has been thoroughly studied when G is a complete graph, but very little is known when G is arbitrary. We define a notion of radius ( G, t ), that extends the standard graph theoretical notion of radius, for considering all the ways in which t nodes may crash, and we present an algorithm that solves consensus in radius ( G, t ) rounds. Then we derive a lower bound showing that, among oblivious algorithms, our algorithm is optimal for a large family of graphs including all vertex-transitive graphs.

Details DOI

I&C Journal 2023 Journal Article

Tasks in modular proofs of concurrent algorithms

Armando Castañeda
Aurélie Hurault
Philippe Quéinnec
Matthieu Roy

Proving the correctness of distributed or concurrent algorithms is a complex process. Errors in the reasoning are hard to find, calling for computer-checked proof systems like Coq or TLA+. To use these tools, sequential specifications of base objects are required to build modular proofs by composition. Unfortunately, many concurrent objects lack a sequential specification. This article describes a method to transform any task, a specification of a concurrent one-shot distributed problem, into a sequential specification involving two calls, set and get. This enables designers to compose proofs, facilitating modular computer-checked proofs of algorithms built using tasks and sequential objects as building blocks. Moir & Anderson implementation of renaming using splitters, wait-free concurrent objects, is an algorithm designed by composition, but it is not modular. Using our transformation, a modular description of the algorithm is given in TLA+ and mechanically verified using the TLA+ Proof System. As far as we know, this is the first time this algorithm is mechanically verified.

Details DOI

TCS Journal 2021 Journal Article

A topological perspective on distributed network algorithms

Armando Castañeda
Pierre Fraigniaud
Ami Paz
Sergio Rajsbaum
Matthieu Roy
Corentin Travers

More than two decades ago, combinatorial topology was shown to be useful for analyzing distributed fault-tolerant algorithms in shared memory systems and in message passing systems. In this work, we show that combinatorial topology can also be useful for analyzing distributed algorithms in failure-free networks of arbitrary structure. To illustrate this, we analyze consensus, set-agreement, and approximate agreement in networks, and derive lower bounds for these problems under classical computational settings, such as the local model and dynamic networks.

Details DOI