Safety Verification of Wait-Only Non-Blocking Broadcast Protocols

TL;DR

This paper analyzes the safety verification of wait-only non-blocking broadcast protocols, showing that certain coverability problems become computationally easier under this restriction.

Contribution

It proves that for wait-only protocols, the state and configuration coverability problems are P-complete and PSPACE-complete, respectively, simplifying their complexity.

Findings

Coverability problems are decidable and Ackermann-hard in general.

Restrictions to wait-only protocols reduce complexity to P and PSPACE.

The results improve understanding of protocol verification complexity.

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.