TY - GEN
T1 - Verification of MPI Java programs using software model checking
AU - Ur Rehman, Waqas
AU - Ayub, Muhammad Sohaib
AU - Siddiqui, Junaid Haroon
N1 - Publisher Copyright:
© 2016 ACM.
PY - 2016/2/27
Y1 - 2016/2/27
N2 - Development of concurrent software requires the programmer to be aware of non-determinism, data races, and deadlocks. MPI (message passing interface) is a popular standard for writing message oriented distributed applications. Some messages in MPI systems can be processed by one of the many machines and in many possible orders. This non-determinism can affect the result of an MPI application. The alternate results may or may not be correct. To verify MPI applications, we need to check all these possible orderings and use an application specific oracle to decide if these orderings give correct output. MPJ Express is an open source Java implementation of the MPI standard.We developed a Java based model of MPJ Express, where processes are modeled as threads, and which can run unmodified MPI Java programs on a single system. This enabled us to adapt the Java PathFinder explicit state software model checker (JPF) using a custom listener to verify our model running real MPI Java programs. We evaluated our approach using small examples where model checking revealed message orders that would result in incorrect system behavior.
AB - Development of concurrent software requires the programmer to be aware of non-determinism, data races, and deadlocks. MPI (message passing interface) is a popular standard for writing message oriented distributed applications. Some messages in MPI systems can be processed by one of the many machines and in many possible orders. This non-determinism can affect the result of an MPI application. The alternate results may or may not be correct. To verify MPI applications, we need to check all these possible orderings and use an application specific oracle to decide if these orderings give correct output. MPJ Express is an open source Java implementation of the MPI standard.We developed a Java based model of MPJ Express, where processes are modeled as threads, and which can run unmodified MPI Java programs on a single system. This enabled us to adapt the Java PathFinder explicit state software model checker (JPF) using a custom listener to verify our model running real MPI Java programs. We evaluated our approach using small examples where model checking revealed message orders that would result in incorrect system behavior.
KW - Java PathFinder(JPF)
KW - Message Passing Interface in Java (MPJ)
KW - Model Checking
UR - https://www.scopus.com/pages/publications/84963754660
U2 - 10.1145/2851141.2851192
DO - 10.1145/2851141.2851192
M3 - Conference Publication
AN - SCOPUS:84963754660
T3 - Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP
BT - 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016 - Proceedings
PB - Association for Computing Machinery
T2 - 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016
Y2 - 12 March 2016 through 16 March 2016
ER -