On the completeness of verifying message passing programs under bounded asynchrony

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

Cited in

(28)

This page was built for publication: On the completeness of verifying message passing programs under bounded asynchrony

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6043166)