Advertisement
Published in:
2010 | OriginalPaper | Chapter
Dynamic Verification of Hybrid Programs
Authors : Wei-Fan Chiang, Grzegorz Szubzda, Ganesh Gopalakrishnan, Rajeev Thakur
Published in: Recent Advances in the Message Passing Interface
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Hybrid (mixed MPI/thread) programs are extremely important for efficiently programming future HPC systems. In this paper, we report our experience adapting ISP [3,4,5], our dynamic verifier for MPI programs, to verify a large hybrid MPI/Pthread program called Eddy Murphi [1]. ISP is a stateless model checker that works by replaying schedules leading up to previously recorded non-deterministic selection points, and pursuing new behaviors out of these points. The main difficulty we faced was the inability to
deterministically replay
up to these selection points because ISP instruments only the MPI calls issued by an application, whereas thread level scheduling non-determinism may change the course of execution. Instrumenting both MPI and Pthreads API calls requires an invasive modification of ISP which was not favored. The novelty of our solution is to determinize thread schedules using a record/replay daemon and demonstrating that this approach works on a realistic hybrid application: the Eddy Murphi model checker.