The paper is motivated by non-deterministic synchronizations in MPI (Message Passing Interface), where some send operations and collective operations may or may not synchronize; a correctly written MPI program should count with both options. Here we focus on the deadlock detection in such systems and propose the following reduction of the explored state space. The system is first analyzed without forcing the respective synchronizations, by applying standard partial-order reduction methods. Then a suggested algorithm is used that searches for potentially missed deadlocks caused by synchronization. In practical examples this approach leads to major reductions of the explored state-space in comparison to encoding the synchronization options into the state-space search directly. The algorithm is presented as a stand-alone abstract framework that can be also applied to the future versions of MPI as well as to other related problem domains.
展开▼
