On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony

Ahmed Bouajjani (1) , Constantin Enea (1) , Kailiang Ji (2) , Shaz Qadeer (3)

1 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
2 PI.R2 - Design, study and implementation of languages for proofs and programs
3 Microsoft Corporation [Redmond]

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.

Domaines: Langage de programmation [cs.PL]

Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer. On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. International Conference on Computer Aided Verification, CAV 2018: Computer Aided Verification, Springer International Publishing, pp.372-391, 2018. ⟨hal-01947855⟩