FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony

Authors: Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer

Paper Information

Title:On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Authors:Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:software verification, model checking, message passing concurrency
Abstract:

ABSTRACT. 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.

Pages:19
Talk:Jul 17 14:45 (Session 121A: Concurrency)
Paper: