Safety Verification of Wait-Only Non-Blocking Broadcast Protocols

Abstract:Broadcast protocols are programs designed to be executed by networks of processes. Each process runs the same protocol, and communication between them occurs in synchronously in two ways: broadcast, where one process sends a message to all others, and rendez-vous, where one process sends a message to at most one other process. In both cases, communication is non-blocking, meaning the message is sent even if no process is able to receive it. We consider two coverability problems: the state coverability problem asks whether there exists a number of processes that allows reaching a given state of the protocol, and the configuration coverability problem asks whether there exists a number of processes that allows covering a given configuration. These two problems are known to be decidable and Ackermann-hard. We show that when the protocol is Wait-Only (i.e., it has no state from which a process can both send and receive messages), these problems become P-complete and PSPACE-complete, respectively.

Logic in Computer Science (cs.LO); Computation and Language (cs.CL); Multiagent Systems (cs.MA)

arXiv:2403.18591 [cs.LO]

(or arXiv:2403.18591v3 [cs.LO] for this version)