Date: October 14th 2024, VERIMAG, Grenoble

Location: Imag Building (room 206)

Programme

9h00-9h30 Welcome & Project news

9h30-10h00 Michael Raskin (LABRI): Modular Population Protocols

Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved changing their states based on each other’s states. Population protocols are often studied in terms of reaching a consensus on whether the input configuration satisfied some predicate. A desirable property of a computation model is modularity, the ability to combine existing simpler computations in a straightforward way. In the present paper we present a more general notion of functionality implemented by a population protocol in terms of multisets of inputs and outputs. This notion allows to design multiphase protocols as combinations of independently defined phases. The additional generality also increases the range of behaviours that can be captured in applications (e.g. maintaining the role distribution in a fleet of servers). We show that the composition of protocols can be performed in a uniform mechanical way, and that the expressive power is essentially semilinear, similar to the predicate expressive power in the original population protocol setting.

10h00-10h30 Nicolas Waldburger (IRISA): Verification of Population Protocols with Unordered Data

Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, i. e., the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP’23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power. We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in ExpSpace. We also provide a lower complexity bound, namely coNExpTime-hardness.

10h30-10h45 Coffee break

10h45-11h15 Romain Delpy (LABRI): An automata-based approach for synchronizable mailbox communication

We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is Pspace-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (Pspace) of several questions considered in previous literature.

11h15-11h45 Lucie Guillou (IRIF): Reachability in Wait-Only Broadcast Networks

In this ongoing work, we investigate networks composed of an unbounded number of agents that communicate via broadcasts. All agents execute the same protocol, described as a finite-state machine. The reachability problem asks whether, given a protocol and a target state, there exists a number of agents and a sequence of actions that leads to a configuration where all agents are in the specified target state. This problem is known to be undecidable in the general case. However, we focus on Wait-Only protocols, where no state allows an agent to both broadcast and receive messages. Under this restriction, we show that the reachability problem becomes decidable, though it is as hard as the reachability problem for Petri nets. This is joint work with Arnaud Sangnier and Tali Sznajder.

11h45-13h30 Lunch break

13h30-14h00 Igor Walukiewicz (LABRI): Distributed race detection

We aim to develop methods for distributed monitoring of program executions to detect concurrency errors at runtime. The goal is to create a technique that can instrument program code to report potential violations of important consistency rules. Our focus is on ensuring that the methods have minimal impact on the program’s original performance, which is why the distributed nature of the monitoring process is crucial. The objective is not to just report if an error happened, but if an error could happen under a different scheduling of the observed execution. This is very powerful as there may be exponentially many schedulings of the same execution, and an error can appear only in particular corner cases. We will present a simple construction of such a distributed monitor for races, discuss its shortcomings, and sketch a more efficient solution.

14h00-14h30 Corto Mascle (LABRI): Verification of dynamic systems with locks and variables

We study the verification of distributed systems where processes have three kinds of operations: taking and releasing locks, reading and writing in shared variables and spawning other processes. While this problem is in general undecidable, we present techniques to decide it in restricted cases with a tree automata-based construction, as well as ongoing work on an extension to synthesis.

14h30-14h45 Coffee break

14h45-15h15 Neven Villani (VERIMAG): Counting Abstraction for the Verification of Structured Parameterized Networks

We present a technique to automatically prove safety properties of a class of (infinite) families of networks, which includes heterogeneous inductive architectures given by network grammars, and synchronization between processes in the form of bounded rendezvous. We tackle the verification problem by computing a reduction from the language of the network grammar (an infinite family of Petri Nets) to a finite number of instances. The safety property of the system, expressed as a coverability problem, is decidable on the reduced system by automated tools.

15h15-15h45 Mathieu Laurent (IRISA): Towards Efficient Verification of Parallel Applications with Mc SimGrid

Assessing the correctness of distributed and parallel applications is notoriously difficult due to the complexity of the concurrent behaviors and the difficulty to reproduce bugs. In this context, Dynamic Partial Order Reduction (DPOR) techniques have proved successful in exploiting concurrency to verify applications without exploring all their behaviors. However, they may lack of efficiency when tracking non-systematic bugs of real size applications. In this paper, we propose two adaptations of the Optimal Dynamic Partial Order (ODPOR) algorithm with a particular focus on bug finding and explanation. The first algorithm proposes an out-of-order version called BeFS ODPOR which purpose is to avoid being stuck in uninteresting large parts of the state space. Once a bug is found, the second adaptation takes advantage of ODPOR principles to efficiently find the origins of the bug. Joint work with Thierry Jéron and Martin Quinson.

15h45-16h00 Closing