CIVL: A Concurrency Intermediate Verification Language

University Of Delaware, Newark DE

Investigators

Abstract

Parallel programming has become increasingly common with the advent of "multi-core" computer chips that pack many processors into a single chip. Most standard laptop and desktop computers now come with anywhere from two to thirty-two such cores. Such chips offer unprecedented computing power, but at a price: to extract their full potential, programmers writing software for the new chips must use special programming language "libraries" in order to specify how the program is to do two (or more) things at once. One popular such library is called OpenMP. These so-called parallel programs are notoriously difficult to get right, and many contain undetected defects ("bugs") that can cause the program to crash or produce incorrect results. The CIVL project has the potential to dramatically reduce the effort required to develop new static analysis tools. The key idea is a unified language for describing parallel programs, whether these use MPI, OpenMP, or both. One tool translates the original program into the new language, also called CIVL. Other tools perform static analysis on the CIVL program. Eventually, many other parallel libraries will be added to the new system. The advantage of this approach is that the designer of a new static analysis tool need only design the tool for a single language---CIVL---but then gets a tool that works on all the source libraries "for free". Similarly, when a new parallel library comes along, by developing a translator from it to CIVL, one can immeidately reap the benefits of all the static analysis tools. The researchers expect that the resulting platform will make it much easier to develop correct parallel programs, no matter how that parallelism is expressed.