Programme
(voir aussi ici)
Lundi 8 novembre
- 12h00 - Déjeuner
- 14h30 - (LaBRI)
We consider a synchronous systems with fixed constant number $N$ of processes communicating through a dynamic network that ensures recurrent connectivity. These systems are model with the Class $T^CR$ of Time varying Graph formalism. Initially, processes only know the number of processes $N$ in the system and their own identifier. The processes discover the membership of the system during the executing the algorithm. Due to the dynamics of the network links, messages can be lost. In these systems, we present a total order broadcast algorithm (i.e. atomic broadcast) that uses FIFO broadcast and deliver primitives. A total order broadcast algorithm ensures that all processes deliver messages in the same order. Moreover, the proposed algorithm preserves the causality relationship between broadcast primitive invocations. Total order or Fifo order broadcast algorithms have been implemented on top of unreliable static networks. FIFO broadcast delivers the messages of a sender in their sending order. We also present a FIFO broadcast algorithm with termination detection. The message size is bounded to $2N + \mathrm{msgSize} + O(\log(N))$ bits where $\mathrm{msgSize}$ is the bound size in bits of the broadcast data. Moreover, at any point of time the number of message in transit is at most $n^{N^2}$.
- 15h00 - (Vérimag)
PADEC is a framework to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, tools for time complexity and composition of algorithms, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions. This talk is a summary of the libraries developed in PADEC.
- 15h30 - Pause café
- 16h00 - (IRISA)
This talk will explain why consistency criteria and progress conditions are at the heart of distributed computing but not in sequential computing. We will present why we cannot guarantee the strongest properties and why it is not easy to choose from the available bestiary.
- 17h00 - Fin des exposés
- 19h15 - Apéritif
- 20h00 - Repas
Mardi 9 novembre
- 8h00 - Petit déjeuner
- 9h00 - (Vérimag)
Modern networks (e.g., MANET, VANET, and DTN) are prone to both faults and frequent alteration of their topology (i.e., the addition or removal of links). Self-stabilization is a versatile fault-tolerant property. In this talk, I will present recent advances in self-stabilization for highly dynamic systems. I will focus on the fundamental problem of leader election.
- 9h30 - (LaBRI)
Dans cet exposé, je parlerai d'analogues au concept d'arbre couvrant dans les graphes temporels. Comme de tels arbres n'existent pas toujours, la définition est assouplie à celle de spanneurs préservant la connexité temporelle. Je présenterai d'abord quelques résultats d'impossibilité en général, puis quelques résultats positifs pour les cas particuliers où (1) le graphe sous-jacent est complet avec des temps déterministes, et (2) le graphe sous-jacent est quelconque avec des temps aléatoires.
- 10h30 - Pause café
- 11h00 - (IRIF)
In this talk, we ask the following question : Can we design randomized distributed algorithms using non adaptive sampling? Such questions can lead to surprising implications in designing space constrained algorithms for various problems. We specifically focus on the $(\!\Delta\!+1)$ graph colouring problem, where we demonstrate the proof of a graph sparsification theorem by analysing the question of non adaptive sampling based distributed algorithm, which in turn implies a one pass semi streaming algorithm as a corollary. This talk is based on the paper "Sublinear Algorithms for $(\!\Delta\!+1)$ Vertex Colouring" by Sephr Assadi et al.
- 11h30 - (IRIF)
We will consider the problem of temporalisation: starting from a static multigraph, assign appearing times to edges in order to obtain a temporal graph where reachability between pairs of nodes is maximised. Motivated by the application to public transit networks, where edges cannot be scheduled independently one of another, we consider the setting where the edges are grouped into certain walks (called trips) in a digraph and where assigning the appearing time to the first edge of a trip forces the appearing times of the subsequent edges.
- 12h00 - Fin des exposés
- 12h15 - Déjeuner
- 14h30 - (invité IRIF)
We describe two setting where we have recently studied communication complexity aspects of distributed computing. First, when considering wait-free computability, the class of solvable tasks has been characterized, and turns out to be the same in various similar message-passing and shared-memory models. But only full-information protocols have been considered, where the number of bits communicated grows with the number of rounds. We show in a SIROCCO’20 paper with Delporte and Fauconnier that for two processes, it is possible to solve any wait-free solvable task using mostly 1-bit messages, without incurring any cost in the optimal number of communication rounds. We identify an additional type of information that needs to be communicated, using a dynamic network graphs model. Second, in failure-free computation, we consider the problem of $A$ privately transmitting information to $B$ by a public announcement overheard by an eavesdropper $C$. To do so by a deterministic protocol, the inputs of the players must be correlated. Dependent inputs are traditionally represented using a deck of cards. We overview results of our SIROCCO’21 and a sequel SERGIO’21 paper with Leyva and Pascual that present a novel perspective inspired by distributed computing theory is provided, to analyze the amount of information that $A$ needs to send, while preventing $C$ from learning a single card of her hand.
- 15h30 - Pause café
- 16h00 - (LIP6)
We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends the dynamic I/O Automata formalism from Attie & Lynch to probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton. Our work extends to probabilistic settings all these features. Furthermore, we prove necessary and sufficient conditions to obtain both (*) the implementation monotonicity with respect to automata creation and destruction and (**) the secure-emulation monotonicity with respect to automata creation and destruction for extending composable secure-emulation defined by Canetti & al. to dynamic settings, an important tool towards the formal verification of protocols combining probabilistic distributed systems and cryptography in dynamic settings (e.g. blockchains, secure distributed computation, cybersecure distributed protocols etc).
- 16h30 - (IRISA)
This talk will introduce a new reliable broadcast communication abstraction suited to $n$-process asynchronous message-passing systems in which up to $t$ processes may behave arbitrarily (Byzantine processes) and where (due to transient disconnections or message losses) up to $d$ correct processes may not receive a message broadcast by a correct (i.e., non-Byzantine) process. Then an algorithm implementing such a communication abstraction will be presented for the system parameters $n$ and $t$ such that $>3t+2d$.
- 17h00 - (LaBRI)
Several frameworks for verification of distributed computing results via proof assistants exist. These frameworks are developed by proof assistant experts, usually with the help of distributed computing experts. Sébastien Bouchard and I wanted to know how much these frameworks could be used without relying on coq experts, or at the very least without relying on the coq experts that designed such frameworks. For this purpose, Sebastien and I tried to verify in Coq a not-so-hard but also not-completely-trivial result about graph exploration by mobile robots. This talk is a feedback about this (eventually successful) experiment.
- 17h30 - Fin des exposés
- 19h15 - Apéritif
- 20h00 - Repas
Mercredi 10 novembre
- 8h00 - Petit déjeuner
- 9h30 - (LaBRI)
Une propriété d'un graphe $G$ est robuste si elle est satisfaite dans tous les sous-graphes couvrants connexes de $G$. Cette notion de robustesse est un type d'hérédité de propriété motivée par les réseaux dynamiques. Nous allons présenter des résultats sur la caractérisation des graphes ayant un diamètre robuste. Le diamètre est important en algorithmique distribuée car il intervient souvent comme paramètre de complexité des algorithmes. Le fait qu'il soit robuste implique alors que la complexité ne se dégradera pas à mesure que le réseau se détériore (c.à.d. perd des liens définitivement), du moment qu'il reste connexe. Nous montrerons que le problème de décider si le diamètre d'un graphe est robuste est co-NP-complet. À l'inverse, décider si la distance entre deux sommets donnés est robuste peut se faire simplement. Ce résultat repose sur la reconnaissance des graphes série-parallèle et une façon de les caractériser via l'exclusion de mineur enraciné.
- 10h00 - (LaBRI/LIS)
Relaxing the sequential specification of shared objects has been proposed as a promising approach to obtain implementations with better complexity. We study the step complexity of relaxed variants of two common shared objects: max registers and counters. In particular, we consider the $k$-multiplicative-accurate max register and the $k$-multiplicative-accurate counter, where read operations are allowed to err by a multiplicative factor of $k$ (for some integer $k$). More accurately, reads are allowed to return an approximate value $x$ of the maximum value $v$ previously written to the max register, or of the number $v$ of increments previously applied to the counter, respectively, such that $v/k \le x \le vk$. We provide upper and lower bounds on the complexity of implementing these objects in a wait-free manner in the shared memory model.
- 10h30 - Pause café
- 11h00 - (IRISA)
During this talk, we will learn why concurrent algorithms that use the special hardware instructions Compare&Swap cannot have a constant space complexity and why this allows us to draw a continuum between wait-free computing and lock-free computing.
- 11h30 - Fin des exposés
- 11h45 - Repas (livré pour 10h20 - possibilité de l'emporter)
- 13h00 - Fin de la réunion
Photos de la réunion
Organisateurs
 |
 |
 |
 |
 |