On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony

Abstract

We address the problem of verifying message passing programs, defined as a set of 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 show that reachability over k -synchronous computations and checking k -synchronizability are both PSPACE-complete. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.