# On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony

arXiv: https://arxiv.org/abs/1804.06612 · HTML: https://mlsanity.com/paper/1804.06612/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Apr 2018.

## Built on by (most cited first, 2 of 2)

- [A partial order view of message-passing communication models](https://mlsanity.com/paper/2210.13062/) (2022)
- [Weakly synchronous systems with three machines are Turing powerful](https://mlsanity.com/paper/2308.10578/) (2023)

## Abstract (arXiv)

We address the problem of verifying message passing programs, defined as a set of parallel processes communicating through unbounded FIFO buffers. We introduce a bounded analysis that explores a special type of computations, called k-synchronous. These computations can be viewed as (unbounded) sequences of interaction phases, each phase allowing at most k send actions (by different processes), followed by a sequence of receives corresponding to sends in the same phase. We give a procedure for deciding k-synchronizability of a program, i.e., whether every computation is equivalent (has the same happens-before relation) to one of its k-synchronous computations. We also show that reachability over k-synchronous computations and checking k-synchronizability are both PSPACE-complete. Furthermore, we introduce a class of programs called em flow-bounded for which the problem of deciding whether there exists a k>0 for which the program is k-synchronizable, is decidable.