Verification of MPI Java programs using software model checking
| Autor: | Waqas Ur Rehman, Muhammad Sohaib Ayub, Junaid Haroon Siddiqui |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Java
Computer science Message Passing Interface 02 engineering and technology Thread (computing) Software_PROGRAMMINGTECHNIQUES computer.software_genre Oracle Software Real time Java 020204 information systems 0202 electrical engineering electronic engineering information engineering Programmer Java applet computer.programming_language business.industry Programming language strictfp Generics in Java Deadlock Java concurrency Computer Graphics and Computer-Aided Design Operating system Java pathfinder business computer Java annotation Java Modeling Language |
| Zdroj: | PPOPP |
| ISSN: | 1558-1160 0362-1340 |
| DOI: | 10.1145/3016078.2851192 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|