research-article

Public Access

CIVL: the concurrency intermediate verification language

Authors:

Stephen F. Siegel,

Timothy K. Zirkel,

Andre V. Marianiello,

John G. Edenhofner,

Matthew B. Dwyer,

Michael S. RogersAuthors Info & Claims

SC '15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis

Article No.: 61, Pages 1 - 12

https://doi.org/10.1145/2807591.2807635

Published: 15 November 2015 Publication History

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.

References

[1]

ABC: ANTLR-Based C front-end. http://vsl.cis.udel.edu/abc. Accessed Jul. 28, 2015.

[2]

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.

[3]

J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang. Prentice Hall Europe, Herfordshire, UK, second edition, 1996.

Digital Library

[4]

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.

[5]

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.

[6]

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.

Digital Library

[7]

C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, Proceedings of CAV, pages 298--302, 2007.

Digital Library

[8]

C OpenMP examples. http://people.sc.fsu.edu/~jburkardt/c_src/openmp/openmp.html. Accessed Feb. 8, 2015.

[9]

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.

[10]

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.

[11]

The Chapel parallel programming language. http://chapel.cray.com/. Accessed Feb. 8, 2015.

[12]

B. Chapman, G. Jost, and R. van der Pas. Using OpenMP: Portable Shared Memory Parallel Programming. MIT Press, Cambridge, Massachusetts, 2008. (examples).

Digital Library

[13]

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.

Digital Library

[14]

CUDA Samples. http://docs.nvidia.com/cuda/cuda-samples/. Accessed Apr. 15, 2015.

[15]

CUDA Programming Guide Version 5.0. http://docs.nvidia.com/cuda/cuda-c-programming-guide/. Accessed Feb. 8, 2015.

[16]

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.

Digital Library

[17]

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.

Digital Library

[18]

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.

Digital Library

[19]

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.

Digital Library

[20]

M. Flatt and PLT. The Racket reference, version 5.3.1. http://docs.racket-lang.org/reference/. Accessed Feb. 6, 2015.

[21]

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.

Digital Library

[22]

M. Garland, M. Kudlur, and Y. Zheng. Designing a unified programming model for heterogeneous machines. In Proceedings of Supercomputing, Nov. 2012.

Digital Library

[23]

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.

Digital Library

[24]

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.

Digital Library

[25]

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.

[26]

G. J. Holzmann. The Spin Model Checker. Addison-Wesley, Boston, 2004.

[27]

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.

[28]

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.

[29]

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.

Digital Library

[30]

J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.

Digital Library

[31]

Lawrence Livermore National Laboratory Message-Passing Interface (MPI) exercise. https://computing.llnl.gov/tutorials/mpi/exercise.html. Accessed Feb. 8, 2015.

[32]

Lawrence Livermore National Laboratory OpenMP tutorial. https://computing.llnl.gov/tutorials/openMP/exercise.html. Accessed Feb. 8, 2015.

[33]

Lawrence Livermore National Laboratory Pthreads tutorial. https://computing.llnl.gov/tutorials/pthreads/exercise.html. Accessed Feb. 8, 2015.

[34]

K. R. M. Leino. This is Boogie 2. http://research.microsoft.com/apps/pubs/default.aspx?id=147643, June 2008.

[35]

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.

Digital Library

[36]

P. Li, G. Li, and G. Gopalakrishnan. Practical symbolic race checking of GPU programs. In Proceedings of Supercomputing, pages 179--190, Nov. 2014.

Digital Library

[37]

Message-Passing Interface Forum. MPI: A Message-Passing Interface standard, version 3.0. http://www.mpi-forum.org/docs/docs.html, Sept. 2012.

[38]

OpenMP Architecture Review Board. OpenMP API Specification for Parallel Programming. http://openmp.org/wp/. Accessed Feb. 8, 2015.

[39]

ParaSail Programming Language. http://www.parasail-lang.org. Accessed Feb. 7, 2014.

[40]

C. S. Pasareanu and N. Rungta. Symbolic PathFinder: symbolic execution of Java bytecode. In Proceedings of ASE, pages 179--180, 2010.

Digital Library

[41]

Parallel programming course. http://users.abo.fi/mats/PP2014/examples/OpenMP/omp_critical.c. Accessed Feb. 8, 2015.

[42]

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.

Digital Library

[43]

Purdue University, Information Technology: Research Computing. Carter -- User Guide. https://www.rcac.purdue.edu/compute/carter/guide/#compile_gpu, 2008. Accessed Feb. 6, 2015.

[44]

M. Quinn. Parallel Programming in C with MPI and OpenMP. McGraw-Hill, 2004.

Digital Library

[45]

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.

Digital Library

[46]

D. M. Ritchie and K. Thompson. The UNIX time-sharing system. Commun. ACM, 17(7):365--375, July 1974.

Digital Library

[47]

J. Sanders and E. Kandrot. CUDA by Example: An Introduction to General-Purpose GPU Programming. Addison-Wesley, 2010.

Digital Library

[48]

SARL: The Symbolic Algebra and Reasoning Library. http://vsl.cis.udel.edu/sarl, Accessed Feb. 6, 2015.

[49]

S. F. Siegel and T. K. Zirkel. A Functional Equivalence Verification Suite. http://vsl.cis.udel.edu/fevs. Accessed Feb. 6, 2015.

[50]

S. F. Siegel and T. K. Zirkel. TASS: The Toolkit for Accurate Scientific Software. Mathematics in Computer Science, 5(4):395--426, 2011.

[51]

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.

[52]

SV-COMP 2015: Competition on software verification. http://sv-comp.sosy-lab.org/2015, Accessed Feb. 7, 2015.

[53]

VirginiaTech: Advanced Research Computing. CUDA. http://www.arc.vt.edu/resources/software/cuda. Accessed Feb. 6, 2015.

[54]

Zing language specification, Microsoft Corporation. http://research.microsoft.com/en-us/projects/zing/zinglanguagespecification.pdf, 2005.

[55]

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.

Cited By

Hao JWang MZhang H(2024)Efficient Deadlock Detection in MPI Programs with Path Compression and Focus MatchingProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3674822(467-476)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3674822
El Karchi JChen HTehraniJamsaz AJannesari APopov MSaillard E(2024)MPI Errors Detection using GNN Embedding and Vector Embedding over LLVM IR2024 IEEE International Parallel and Distributed Processing Symposium (IPDPS)10.1109/IPDPS57955.2024.00059(595-607)Online publication date: 27-May-2024
https://doi.org/10.1109/IPDPS57955.2024.00059
Burak SIvanov IDomke JMüller M(2024)SPMD IR: Unifying SPMD and Multi-value IR Showcased for Static Verification of CollectivesRecent Advances in the Message Passing Interface10.1007/978-3-031-73370-3_1(3-20)Online publication date: 25-Sep-2024
https://doi.org/10.1007/978-3-031-73370-3_1
Show More Cited By

Index Terms

Recommendations

Verification of MPI programs using CIVL
EuroMPI '17: Proceedings of the 24th European MPI Users' Group Meeting

CIVL 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 analysis

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SC '15: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis

November 2015

985 pages

ISBN:9781450337236

DOI:10.1145/2807591

General Chair:
Jackie Kern
University of Illinois at Urbana-Champaign, Urbana, Illinois
,
Program Chair:
Jeffrey S. Vetter
Oak Ridge National Laboratory and Georgia Institute of Technology, Oak Ridge, Tennessee

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 November 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

SC15

Sponsor:

SIGHPC
SIGARCH
IEEE-CS

SC15: The International Conference for High Performance Computing, Networking, Storage and Analysis

November 15 - 20, 2015

Texas, Austin

Acceptance Rates

SC '15 Paper Acceptance Rate 79 of 358 submissions, 22%;

Overall Acceptance Rate 1,516 of 6,373 submissions, 24%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
1,099
Total Downloads

Downloads (Last 12 months)177
Downloads (Last 6 weeks)29

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hao JWang MZhang H(2024)Efficient Deadlock Detection in MPI Programs with Path Compression and Focus MatchingProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3674822(467-476)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3674822
El Karchi JChen HTehraniJamsaz AJannesari APopov MSaillard E(2024)MPI Errors Detection using GNN Embedding and Vector Embedding over LLVM IR2024 IEEE International Parallel and Distributed Processing Symposium (IPDPS)10.1109/IPDPS57955.2024.00059(595-607)Online publication date: 27-May-2024
https://doi.org/10.1109/IPDPS57955.2024.00059
Burak SIvanov IDomke JMüller M(2024)SPMD IR: Unifying SPMD and Multi-value IR Showcased for Static Verification of CollectivesRecent Advances in the Message Passing Interface10.1007/978-3-031-73370-3_1(3-20)Online publication date: 25-Sep-2024
https://doi.org/10.1007/978-3-031-73370-3_1
Denis XSiegel S(2024)VerifyThis 2023: An International Program Verification CompetitionTOOLympics Challenge 202310.1007/978-3-031-67695-6_5(147-159)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_5
Luo ZSiegel S(2024)Collective Contracts for Message-Passing Parallel ProgramsComputer Aided Verification10.1007/978-3-031-65630-9_3(44-68)Online publication date: 25-Jul-2024
https://doi.org/10.1007/978-3-031-65630-9_3
Wu WHückelheim JHovland PLuo ZSiegel S(2023)Model Checking Race-Freedom When “Sequential Consistency for Data-Race-Free Programs” is GuaranteedComputer Aided Verification10.1007/978-3-031-37703-7_13(265-287)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37703-7_13
Sugawara STakahashi KShimomura YEgawa RTakizawa H(2023)Equivalence Checking of Code Transformation by Numerical and Symbolic ApproachesParallel and Distributed Computing, Applications and Technologies10.1007/978-3-031-29927-8_29(373-386)Online publication date: 8-Apr-2023
https://doi.org/10.1007/978-3-031-29927-8_29
Vasconcelos VMartins FLópez HYoshida N(2022)A Type Discipline for Message Passing Parallel ProgramsACM Transactions on Programming Languages and Systems10.1145/355251944:4(1-55)Online publication date: 21-Dec-2022
https://dl.acm.org/doi/10.1145/3552519
Nguyen TNguyen KDuong HDwyer M(2022)SymInferProceedings of the ACM/IEEE 44th International Conference on Software Engineering: Companion Proceedings10.1145/3510454.3516833(197-201)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510454.3516833
Nguyen TNguyen KDwyer M(2022)Using Symbolic States to Infer Numerical InvariantsIEEE Transactions on Software Engineering10.1109/TSE.2021.310696448:10(3877-3899)Online publication date: 1-Oct-2022
https://doi.org/10.1109/TSE.2021.3106964
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents