CIVL: A Concurrency Intermediate Verification Language

点击翻译按钮获取中文摘要

Parallel programming has become increasingly common with the advent of"multi-core" computer chips that pack many processors into a singlechip. Most standard laptop and desktop computers now come with anywherefrom two to thirty-two such cores. Such chips offer unprecedented computing power, but at a price: toextract their full potential, programmers writing software for the newchips must use special programming language "libraries" in order tospecify how the program is to do two (or more) things at once. Onepopular such library is called OpenMP. These so-called parallelprograms are notoriously difficult to get right, and many containundetected defects ("bugs") that can cause the program to crash orproduce incorrect results.The CIVL project has the potential to dramatically reduce the effortrequired to develop new static analysis tools. The key idea is aunified language for describing parallel programs, whether these useMPI, OpenMP, or both. One tool translates the original program intothe new language, also called CIVL. Other tools perform staticanalysis on the CIVL program. Eventually, many other parallellibraries will be added to the new system. The advantage of thisapproach is that the designer of a new static analysis tool need onlydesign the tool for a single language---CIVL---but then gets a toolthat works on all the source libraries "for free". Similarly, when anew parallel library comes along, by developing a translator from itto CIVL, one can immeidately reap the benefits of all the staticanalysis tools. The researchers expect that the resulting platformwill make it much easier to develop correct parallel programs, nomatter how that parallelism is expressed.