Scheduling considerations for building dynamic verification tools for MPI

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Scheduling considerations for building dynamic verification tools for MPI

Full text

Pdf (135 KB)

Source

International Symposium on Software Testing and Analysis archive
Proceedings of the 6th workshop on Parallel and distributed systems: testing, analysis, and debugging table of contents

Seattle, Washington

Article No. 3

Year of Publication: 2008

ISBN:978-1-60558-052-4

Authors

Sarvani Vakkalanka	University of Utah, Salt Lake City, UT
Michael DeLisi	University of Utah, Salt Lake City, UT
Ganesh Gopalakrishnan	University of Utah, Salt Lake City, UT
Robert M. Kirby	University of Utah, Salt Lake City, UT

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 43, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1390841.1390844 What is a DOI?

ABSTRACT

Dynamic verification methods are the natural choice for formally verifying real world programs when model extraction and maintenance are expensive. Message passing programs written using the MPI library often fall under this category, especially when these programs have to be verified after being ported to new platforms and iteratively optimized. However, implementing dynamic verification tools for MPI requires solving many problems pertaining to the scheduling realities of the MPI runtime. In this paper, we describe the progression of our ideas during the development of our dynamic verification tool for MPI programs, called in-situ partial order (ISP). Each idea developed in this progression relates to our dual goals of ensuring full coverage of all representative interleavings (in the sense of partial order reduction) among MPI processes, and forcing the MPI runtime to affect these interleavings. We briefly examine similar issued faced by other builders of dynamic verification tools. We conclude with observations backing the growing importance of addressing scheduling issues in future dynamic verification tools for various concurrency APIs.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
	2	Klaus Havelund and Thomas Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4), April 2000.
	3	Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
	4	Madanlal Musuvathi , Shaz Qadeer, Iterative context bounding for systematic testing of multithreaded programs, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
	5	Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert M. Kirby. Distributed dynamic partial order reduction based verification of threaded software. In Lecture Notes in Computer Science, volume 4595, pages 58--75, 2007.
	6	http://research.microsoft.com/projects/CHESS/.
	7	Koushik Sen and Gul Agha. Concolic testing of multithreaded programs and its application to testing security protocols. Technical Report UIUCDCS-R-2006-2676, University of Illinois at Urbana Champaign, 2006.
	8	Sarvani Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby. Dynamic verification of mpi programs with reductions in presence of split operations and relaxed orderings. In Computer Aided Verification, 2008. Accepted.
	9	2007. Personal conversation with Shaz Qadeer.
	10	http://www.cs.utah.edu/formal_verification/padtad08.
	11	Bettina Krammer and Michael M. Resch. Correctness checking of MPI one-sided communication using marmot. In Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI), LNCS 4192, pages 105--114, 2006.
	12	Orit Edelstein, Eitan Farchi, Evgeny Goldin, Yarden Nir, Gil Ratsaby, and Shmuel Ur. Framework for testing multi-threaded java programs. Concurrency and Computation: Practice and Experience, 15(3--5):485--499, 2003.
	13	Marc Snir , Steve Otto, MPI-The Complete Reference: The MPI Core, MIT Press, Cambridge, MA, 1998
	14	William D. Gropp and Ewing Lusk. Using mpi-2: A problem-based approach, 2007. Tutorial.
	15	Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
	16	Salman Pervez, Robert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp. Practical model checking method for verifying correctness of mpi programs. In EuroPVM/MPI, pages 344--353, 2007.