The Concurrency Intermediate Verification Language Reference Manual v0. 17

The CIVL-C language is primarily intended to be an intermediate representation for verification. AC program using MPI [2], CUDA [3], OpenMP [4], OpenCL [1], 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 clear: the developer of a new verification technique could implement it for CIVL-C and then immediately see its impact across a broad range of concurrent programs. Likewise, when a new concurrency API is introduced, one only needs to implement a translator from it to CIVL-C in order to reap the benefits of all the verification tools in the platform. Programmers would have a valuable verification and debugging tool, while API designers could use CIVL as a “sandbox” to investigate possible API modifications, additions, and interactions. This manual covers all aspects of the CIVL framework, and is organized in parts as follows:1. this introduction, including “quick start” instructions for downloading and installing CIVL and several examples; 2. a complete description of the CIVL-C language; 3. a formal semantics for the language; and4. a description of the tools in the framework.