Stephen F. Siegel
Manchun Zheng
Matthew B. Dwyer
ABSTRACT
There are many ways to express parallel programs: message-passing libraries (MPI) and multithreading/GPU language extensions such as OpenMP, Pthreads, and CUDA, are but a few. This multitude creates a serious challenge for developers of software verification tools: it takes enormous effort to develop such tools, but each development effort typically targets one small part of the concurrency landscape, with little sharing of techniques and code among efforts.
To address this problem, we present CIVL: the Concurrency Intermediate Verification Language. CIVL provides a general concurrency model capable of representing programs in a variety of concurrency dialects, including those listed above. The CIVL framework currently includes front-ends for the four dialects, and a back-end verifier which uses model checking and symbolic execution to check a number of properties, including the absence of deadlocks, race conditions, assertion violations, illegal pointer dereferences and arithmetic, memory leaks, divisions by zero, and out-of-bound array indexing; it can also check that two programs are functionally equivalent.
- ABC: ANTLR-Based C front-end. http://vsl.cis.udel.edu/abc. Accessed Jul. 28, 2015.Google Scholar
- T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: Exploiting program structure for model checking concurrent software. In Procedings of CONCUR, pages 1--15, 2004.Google ScholarCross Ref
- J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang. Prentice Hall Europe, Herfordshire, UK, second edition, 1996. Google ScholarDigital Library
- P. Balaji, J. Dinan, T. Hoefler, and R. Thakur. Advanced MPI programming. Tutorial at SC13: International Conference on High Performance Computing, Networking, Storage, and Analysis, Denver, Colorado, November 2013. Accessed Feb. 6, 2015.Google Scholar
- J. Barnat, L. Brim, V. Havel, J. Havlícek, J. Kriho, M. Lenco, P. Rockai, V. Still, and J. Weiser. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In N. Sharygina and H. Veith, editors, Proceedings of CAV, pages 863--868, 2013.Google Scholar
- C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, and C. Tinelli. CVC4. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of CAV, pages 171--177, 2011. Google ScholarDigital Library
- C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, Proceedings of CAV, pages 298--302, 2007. Google ScholarDigital Library
- C OpenMP examples. http://people.sc.fsu.edu/~jburkardt/c_src/openmp/openmp.html. Accessed Feb. 8, 2015.Google Scholar
- Center for Development of Advanced Computing. hyPACK 2013: MPI-OpenMP Programs. http://cdac.in/index.aspx?id=ev_hpc_hypack_mpi_openmp_programs. Accessed Apr. 17, 2015.Google Scholar
- Center for Development of Advanced Computing. Programming on Multi-Core Processors Using MPI - Pthreads. http://cdac.in/index.aspx?id=ev_hpc_hypack_mpi_pthreads overview. Accessed Apr. 17, 2015.Google Scholar
- The Chapel parallel programming language. http://chapel.cray.com/. Accessed Feb. 8, 2015.Google Scholar
- B. Chapman, G. Jost, and R. van der Pas. Using OpenMP: Portable Shared Memory Parallel Programming. MIT Press, Cambridge, Massachusetts, 2008. (examples). Google ScholarDigital Library
- J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Păsăreanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of ICSE, pages 439--448, 2000. Google ScholarDigital Library
- CUDA Samples. http://docs.nvidia.com/cuda/cuda-samples/. Accessed Apr. 15, 2015.Google Scholar
- CUDA Programming Guide Version 5.0. http://docs.nvidia.com/cuda/cuda-c-programming-guide/. Accessed Feb. 8, 2015.Google Scholar
- L. de Moura and N. Bjorner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and J. Rehof, editors, Proceedings of TACAS, pages 337--340, 2008. Google ScholarDigital Library
- M. B. Dwyer, J. Hatcliff, Robby, and V. P. Ranganath. Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Form. Methods Syst. Des., 25:199--240, September 2004. Google ScholarDigital Library
- J.-C. Filliâtre and A. Paskevich. Why3: Where programs meet provers. In M. Felleisen and P. Gardner, editors, Proceedings of ESOP, pages 125--128, 2013. Google ScholarDigital Library
- B. Fischer, O. Inverso, and G. Parlato. CSeq: A sequentialization tool for C. In N. Piterman and S. A. Smolka, editors, Proceedings of TACAS, pages 616--618, 2013. Google ScholarDigital Library
- M. Flatt and PLT. The Racket reference, version 5.3.1. http://docs.racket-lang.org/reference/. Accessed Feb. 6, 2015.Google Scholar
- M. Frigo, C. E. Leiserson, and K. H. Randall. The implementation of the Cilk-5 multithreaded language. In Proceedings of PLDI, pages 212--223, 1998. Google ScholarDigital Library
- M. Garland, M. Kudlur, and Y. Zheng. Designing a unified programming model for heterogeneous machines. In Proceedings of Supercomputing, Nov. 2012. Google ScholarDigital Library
- P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, 1996. Google ScholarDigital Library
- G. Gopalakrishnan, R. M. Kirby, S. Siegel, R. Thakur, W. Gropp, E. Lusk, B. R. De Supinski, M. Schulz, and G. Bronevetsky. Formal analysis of MPI-based parallel programs. Communications of the ACM, 54(12):82--91, Dec. 2011. Google ScholarDigital Library
- C. Hathhorn, M. Becchi, W. L. Harrison, and A. M. Procter. Formal semantics of heterogeneous CUDA-C: A modular approach with applications. In Proceedings of the 7th Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28--30 November 2012, pages 115--124, 2012.Google ScholarCross Ref
- G. J. Holzmann. The Spin Model Checker. Addison-Wesley, Boston, 2004.Google Scholar
- Institute of Electrical and Electronics Engineers, Inc. IEEE Standard for Information Technology---Portable Operating System Interface (POSIX) Base Specifications, Issue 7, IEEE Std 1003.1-2008 (Revision of IEEE Std 1003.1-2004). IEEE, 3 Park Avenue, New York, NY 10016-5997, USA, Dec. 2008.Google Scholar
- International Organization for Standardization and International Electrotechnical Commission. ISO/IEC 989:2011 N1570: Programming Languages -- C. http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf, Apr. 2011.Google Scholar
- S. Khurshid, C. S. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In H. Garavel and J. Hatcliff, editors, Proceedings of TACAS, pages 553--568, 2003. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976. Google ScholarDigital Library
- Lawrence Livermore National Laboratory Message-Passing Interface (MPI) exercise. https://computing.llnl.gov/tutorials/mpi/exercise.html. Accessed Feb. 8, 2015.Google Scholar
- Lawrence Livermore National Laboratory OpenMP tutorial. https://computing.llnl.gov/tutorials/openMP/exercise.html. Accessed Feb. 8, 2015.Google Scholar
- Lawrence Livermore National Laboratory Pthreads tutorial. https://computing.llnl.gov/tutorials/pthreads/exercise.html. Accessed Feb. 8, 2015.Google Scholar
- K. R. M. Leino. This is Boogie 2. http://research.microsoft.com/apps/pubs/default.aspx?id=147643, June 2008.Google Scholar
- G. Li, P. Li, G. Sawaya, G. Gopalakrishnan, I. Ghosh, and S. P. Rajan. GKLEE: Concolic verification and test generation for GPUs. In Proceedings of PPoPP, 2012. Google ScholarDigital Library
- P. Li, G. Li, and G. Gopalakrishnan. Practical symbolic race checking of GPU programs. In Proceedings of Supercomputing, pages 179--190, Nov. 2014. Google ScholarDigital Library
- Message-Passing Interface Forum. MPI: A Message-Passing Interface standard, version 3.0. http://www.mpi-forum.org/docs/docs.html, Sept. 2012.Google Scholar
- OpenMP Architecture Review Board. OpenMP API Specification for Parallel Programming. http://openmp.org/wp/. Accessed Feb. 8, 2015.Google Scholar
- ParaSail Programming Language. http://www.parasail-lang.org. Accessed Feb. 7, 2014.Google Scholar
- C. S. Pasareanu and N. Rungta. Symbolic PathFinder: symbolic execution of Java bytecode. In Proceedings of ASE, pages 179--180, 2010. Google ScholarDigital Library
- Parallel programming course. http://users.abo.fi/mats/PP2014/examples/OpenMP/omp_critical.c. Accessed Feb. 8, 2015.Google Scholar
- W. Pugh and D. Wonnacott. Going beyond integer programming with the omega test to eliminate false data dependences. IEEE Trans. Parallel Distrib. Syst., 6(2):204--211, Feb. 1995. Google ScholarDigital Library
- Purdue University, Information Technology: Research Computing. Carter -- User Guide. https://www.rcac.purdue.edu/compute/carter/guide/#compile_gpu, 2008. Accessed Feb. 6, 2015.Google Scholar
- M. Quinn. Parallel Programming in C with MPI and OpenMP. McGraw-Hill, 2004. Google ScholarDigital Library
- Z. Rakamarić and M. Emmi. SMACK: Decoupling source language details from verifier implementations. In A. Biere and R. Bloem, editors, Proceedings of CAV, pages 106--113, 2014. Google ScholarDigital Library
- D. M. Ritchie and K. Thompson. The UNIX time-sharing system. Commun. ACM, 17(7):365--375, July 1974. Google ScholarDigital Library
- J. Sanders and E. Kandrot. CUDA by Example: An Introduction to General-Purpose GPU Programming. Addison-Wesley, 2010. Google ScholarDigital Library
- SARL: The Symbolic Algebra and Reasoning Library. http://vsl.cis.udel.edu/sarl, Accessed Feb. 6, 2015.Google Scholar
- S. F. Siegel and T. K. Zirkel. A Functional Equivalence Verification Suite. http://vsl.cis.udel.edu/fevs. Accessed Feb. 6, 2015.Google Scholar
- S. F. Siegel and T. K. Zirkel. TASS: The Toolkit for Accurate Scientific Software. Mathematics in Computer Science, 5(4):395--426, 2011.Google Scholar
- R. M. Stallman and the GCC Developer Community. Using the GNU Compiler Collection: For GCC version 4.7.2. GNU Press, a division of the Free Software Foundation, 2010. http://gcc.gnu.org/onlinedocs/gcc. Accessed Feb. 6, 2015.Google Scholar
- SV-COMP 2015: Competition on software verification. http://sv-comp.sosy-lab.org/2015, Accessed Feb. 7, 2015.Google Scholar
- VirginiaTech: Advanced Research Computing. CUDA. http://www.arc.vt.edu/resources/software/cuda. Accessed Feb. 6, 2015.Google Scholar
- Zing language specification, Microsoft Corporation. http://research.microsoft.com/en-us/projects/zing/zinglanguagespecification.pdf, 2005.Google Scholar
- T. K. Zirkel, S. F. Siegel, and T. McClory. Automated verification of Chapel programs using model checking and symbolic execution. In G. Brat, N. Rungta, and A. Venet, editors, Proceedings of NFM, pages 198--212, 2013.Google Scholar
Index Terms
- CIVL: the concurrency intermediate verification language
Recommendations
Verification of MPI programs using CIVL
EuroMPI '17: Proceedings of the 24th European MPI Users' Group MeetingCIVL is a framework for verifying concurrent programs. The framework is built around a language, CIVL-C, that extends sequential C with general-purpose primitives that can be used to model a variety of concurrency dialects, including OpenMP, Pthreads, ...
Using model checking with symbolic execution to verify parallel numerical programs
ISSTA '06: Proceedings of the 2006 international symposium on Software testing and analysisWe present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. The method requires that a sequential version of the program be provided, to ...
Combining symbolic execution with model checking to verify parallel numerical programs
We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. This method requires that a sequential version of the program be provided, to ...
Comments