Fang Yu
Shun-Ching Yang
ABSTRACT
We present a symbolic approach for checking consistency of OpenMP parallel programs. A parallel program is consistent if it yields the same result as its sequential version despite the execution order among threads. We find race conditions of an OpenMP parallel program, construct the formal model of its raced segments under relaxed memory models, and perform guided symbolic simulation to search consistency violations. The simulation terminates when (1) a witness has been found (the program is inconsistent), or (2) all reachable states have been explored (the program is consistent). We have developed the tool Pathg by incorporating Omega library to solve race constraints and Red symbolic simulator to perform guided search. We show that Pathg can prove consistency of programs, identify races that modern OpenMP checkers failed to report, and find inconsistency witnesses effectively against benchmarks from the OpenMP Source Code Repository and the NAS Parallel benchmark suite.
- Sarita V. Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, 1996. Google Scholar
Digital Library
- Amittai Aviram and Bryan Ford. Deterministic OpenMP for Race-Free Parallelism. In 3rd USENIX Workshop on Hot Topics in Parallelism (HotPar11), 2011. Google ScholarDigital Library
- D. Bailey, T. Harris, W. Saphir, R. Van Der Wijngaart, A. Woo, and M. Yarrow. The NAS parallel benchmarks 2.0. Technical report, Citeseer, 1995.Google Scholar
- V. Basupalli, Tomofumi Yuki, Sanjay V. Rajopadhye, Antoine Morvan, Steven Derrien, Patrice Quinton, and David Wonnacott. ompverify: Polyhedral analysis for the openmp programmer. In IWOMP, pages 37--53, 2011. Google ScholarDigital Library
- OpenMP Architecture Review Board. OpenMP application interface version 3.0. 2008.Google Scholar
- Hans-Juergen Boehm and Sarita V. Adve. Foundations of the c++ concurrency memory model. In PLDI, pages 68--78, 2008. Google ScholarDigital Library
- Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. JACM, 30(2):p323--342, 1983. Google ScholarDigital Library
- Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. Check-fence: checking consistency of concurrent data types on relaxed memory models. In PLDI, pages 12--21, 2007. Google ScholarDigital Library
- Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan. Line-up: a complete and automatic linearizability checker. In PLDI, pages 330--340, 2010. Google ScholarDigital Library
- Y. Byun, B. Sanders, and C.-S. Keum. Design patterns of communicating extended finite state machines in sdl. In 8th Conference on Pattern Languages of Programs (PLoP'01), 2001.Google Scholar
- M. Said C. Wang and A. Gupta. Coverage guided systematic concurrency testing. In International Conference on Software Engineering (ICSE'11), Honolulu, Hawaii, May 2011. Google ScholarDigital Library
- A.J. Dorta, C. Rodriguez, and F. de Sande. The OpenMP source code repository. In Parallel, Distributed and Network-Based Processing, 2005. PDP 2005. 13th Euromicro Conference on, pages 244--250. IEEE, 2005. Google ScholarDigital Library
- J. Ellsberger, D. Hogrefe D., and A. Sarma. SDL: Formal Object-Oriented Language For Communicating Systems. Prentrice Hall, Harlow, England, 1997.Google Scholar
- Malay K. Ganai and Aarti Gupta. Efficient modeling of concurrent systems in bmc. In SPIN, pages 114--133, 2008. Google ScholarDigital Library
- Matthew Hennessy. Semantics of programming languages - an elementary introduction using structural operational semantics. Wiley, 1990. Google ScholarDigital Library
- Mun-Hye Kang, Ok-Kyoon Ha, Sang-Woo Jun, and Yong-Kee Jun. A tool for detecting first races in openmp programs. In PaCT, pages 299--303, 2009. Google ScholarDigital Library
- Wayne Kelly, Vadim Maslov, William Pugh, Evan Rosser, Tatiana Shpeisman, and David Wonnacott. The omega library interface guide. Technical report, College Park, MD, USA, 1995. Google ScholarDigital Library
- Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric. Static and precise detection of concurrency errors in systems code using smt solvers. In CAV, pages 509--524, 2009. Google ScholarDigital Library
- Y. Lin. Static nonconcurrency analysis of openmp programs. OpenMP Shared Memory Parallel Programming, pages 36--50, 2008. Google ScholarCross Ref
- Jeremy Manson, William Pugh, and Sarita V. Adve. The java memory model. In POPL, pages 378--391, 2005. Google ScholarDigital Library
- Stephen P. Masticola and Barbara G. Ryder. Non-concurrency analysis. In PPOPP, pages 129--138, 1993. Google ScholarDigital Library
- Vijay Menon, Keshav Pingali, and Nikolay Mateev. Fractal symbolic analysis. ACM Trans. Program. Lang. Syst., 25(6):776--813, 2003. Google ScholarDigital Library
- Microsoft. Concurrency runtime. http://msdn.microsoft.com/en-us/library/dd504870.aspx.Google Scholar
- Madan Musuvathi and Shaz Qadeer. Chess: Systematic stress testing of concurrent software. In LOPSTR, pages 15--16, 2006. Google ScholarDigital Library
- Paul Petersen and Sanjiv Shah. Openmp support in the intel thread checker. In WOMPAT, pages 1--12, 2003. Google ScholarDigital Library
- Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In TACAS, pages 93--107, 2005. Google ScholarDigital Library
- Shaz Qadeer and Dinghao Wu. Kiss: keep it simple and sequential. In PLDI, pages 14--24, 2004. Google ScholarDigital Library
- Ishai Rabinovitz and Orna Grumberg. Bounded model checking of concurrent programs. In CAV, pages 82--97, 2005. Google ScholarDigital Library
- Arch D. Robison. Intel. In Encyclopedia of Parallel Computing, pages 955--964. 2011.Google ScholarCross Ref
- Paul Sack, Brian E. Bliss, Zhiqiang Ma, Paul Petersen, and Josep Torrellas. Accurate and efficient filtering for the Intel thread checker race detector. In ASID, pages 34--41, 2006. Google ScholarDigital Library
- Caitlin Sadowski, Stephen N. Freund, and Cormac Flanagan. Single-track: A dynamic determinism checker for multithreaded programs. In ESOP, pages 394--409, 2009. Google ScholarDigital Library
- Christian Terboven. Comparing intel thread checker and sun thread analyzer. In PARCO, pages 669--676, 2007.Google Scholar
- Emina Torlak, Mandana Vaziri, and Julian Dolby. Memsat: checking axiomatic specifications of memory models. In PLDI, pages 341--350, 2010. Google ScholarDigital Library
- Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. Relay: static race detection on millions of lines of code. In ESEC/SIGSOFT FSE, pages 205--214, 2007. Google ScholarDigital Library
- Farn Wang. Symbolic simulation checking of dense-time automata. In 5th FORMATS (International Conference on Formal Modelling and Analysis of Timed Systems), volume LNCS 4763. Springer-Verlag, October 2007. Google ScholarDigital Library
- Farn Wang, Li-Wei Yao, and Ya-Lan Yang. Efficient verification of distributed real-time systems with broadcasting behaviors. To appear in Real-Time System Journal, Online First, 13 April 2011. Google ScholarDigital Library
- Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom. Memory-model-sensitive data race analysis. In ICFEM, pages 30--45, 2004.Google ScholarCross Ref
Index Terms
- Symbolic consistency checking of OpenMp parallel programs
Recommendations
Symbolic consistency checking of OpenMp parallel programs
LCTES '12We present a symbolic approach for checking consistency of OpenMP parallel programs. A parallel program is consistent if it yields the same result as its sequential version despite the execution order among threads. We find race conditions of an OpenMP ...
Model Checking Race-Freedom When “Sequential Consistency for Data-Race-Free Programs” is Guaranteed
Computer Aided VerificationAbstractMany parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning ...
Compiling data-parallel programs for clusters of SMPs: Research Articles
Compilers for Parallel ComputersClusters of shared-memory multiprocessors (SMPs) have become the most promising parallel computing platforms for scientific computing. However, SMP clusters significantly increase the complexity of user application development when using the low-level ...
Comments