Title : CIVL : The Concurrency Intermediate Verification Language

Recent years have witnessed an explosion in the number of programming languages and language extensions dealing with concurrency. Examples include message-passing libraries (MPI-3), multithreading and GPU language extensions such as OpenMP, Pthreads, OpenCL, and CUDA, and entirely new languages such as Chapel. This multitude creates a serious challenge for developers of software verification tools: it takes enormous e↵ort to develop such tools, but each development e↵ort typically targets one small part of the concurrency landscape, with little sharing of techniques and code between e↵orts. To address this problem, we present CIVL: a Concurrency Intermediate Verification Language. CIVL provides a concurrency model su ciently flexible to represent programs in a wide variety of parallel languages, including those listed above. We have realized CIVL as a dialect of C with new primitives for concurrency and others to facilitate specification and verification. We have also developed a tool that combines model checking and symbolic execution to verify or refute a number of properties of CIVL programs, such as absence of deadlock and assertion violations, and functional equivalence. 1 The CIVL Framework The CIVL framework encompasses (1) the programming language CIVL-C, a dialect of C with additional primitives supporting concurrency, specification, and modeling; (2) verification and analysis tools, including a symbolic executionbased model checker for checking various properties of, or finding defects in, CIVL-C programs; and (3) tools that translate from many commonly used languages/APIs to CIVL-C. Our goal is for CIVL-C to be an e↵ective intermediate representation for verification. A C program using MPI [16], CUDA [11], OpenMP [7], OpenCL [21], or another API (or even some combination of APIs), will be automatically translated into CIVL-C and then verified. The advantages of such a framework are