2018/04/18 by Ahmed Bouajjani, Bouajjani, Ahmed, Constantin Enea +5 · 3 citations
Computer Science · #Distributed systems and fault tolerance #Parallel Computing and Optimization Techniques #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.1804.06612
We address the problem of verifying message passing programs, defined as a\nset of parallel processes communicating through unbounded FIFO buffers. We\nintroduce a bounded analysis that explores a special type of computations,\ncalled k-synchronous. These computations can be viewed as (unbounded) sequences\nof interaction phases, each phase allowing at most k send actions (by different\nprocesses), followed by a sequence of receives corresponding to sends in the\nsame phase. We give a procedure for deciding k-synchronizability of a program,\ni.e., whether every computation is equivalent (has the same happens-before\nrelation) to one of its k-synchronous computations. We also show that\nreachability over k-synchronous computations and checking k-synchronizability\nare both PSPACE-complete. Furthermore, we introduce a class of programs called\n em flow-bounded for which the problem of deciding whether there exists a k>0\nfor which the program is k-synchronizable, is decidable.\n