Paper Info
Title
Detecting MPI Zero Buffer Incompatibility by SMT Encoding.
Abstract
A prevalent asynchronous message passing standard is the Message Passing Interface (MPI). There are two runtime semantics for MPI: zero buffer (messages have no buffering) and infinite buffer (messages are copied into a runtime buffer on the API call). A problem in any MPI program, intended or otherwise, is zero buffer incompatibility. A zero buffer incompatible MPI program deadlocks. This problem is difficult to predict because a developer does not know if the deadlock is based on the buffering semantics or a bad program. This paper presents an algorithm that encodes a single-path MPI program as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible schedule, such that it proves the program is zero buffer compatible. This encoding is also adaptable to checking assertion violation for correct computation. To support MPI semantics, this algorithm correctly defines the point-to-point communication and collective communication with respective rules for both infinite buffer semantics and zero buffer semantics. The novelty in this paper is considering only the schedules that strictly alternate sends and receives leading to an intuitive zero buffer encoding. This paper proves that the set of all the strictly alternating schedules is capable of covering all the message communication that may occur in any execution under zero buffer semantics. Experiments demonstrate that the SMT encoding is correct and highly efficient for a set of benchmarks compared with two state-of-art MPI verifiers.
Year
DOI
Venue
2015
10.1007/978-3-319-17524-9_16
Lecture Notes in Computer Science
Keywords
Field
DocType
MPI,SMT,Message Passing
Asynchronous communication,Programming language,Computer science,Parallel computing,Deadlock,Schedule,Message Passing Interface,Message passing,Semantics,Encoding (memory),Satisfiability modulo theories
Conference
Volume
ISSN
Citations 
9058
0302-9743
4
PageRank 
References 
Authors
0.38
18
2
Name
Order
Citations
PageRank
Yu Huang1101.15
eric mercer212511.06