CIVL: A Concurrency Intermediate Verification Language

随着“多核”计算机芯片的出现，并行编程变得越来越普遍，这种芯片可以将多个处理器整合到一个单片机上。大多数标准的笔记本电脑和台式电脑现在都配备了2到32个这样的核心。这种芯片提供了前所未有的计算能力，但也是有代价的：为了充分挖掘它们的潜力，为新芯片编写软件的程序员必须使用特殊的编程语言“库”，以指定程序如何同时做两件(或更多)事情。一个流行的这样的库被称为OpenMP。众所周知，这些所谓的并行程序很难正确运行，许多程序包含未被检测到的缺陷(“错误”)，这些缺陷可能会导致程序崩溃或产生错误的结果。Cipl项目有可能极大地减少开发新的静态分析工具所需的工作量。其核心思想是使用一种统一的语言来描述并行程序，无论这些程序使用MPI、OpenMP还是两者都使用。有一种工具可以将原始程序翻译成新的语言，也称为CIVL。其他工具对CIVIL程序执行静态分析。最终，许多其他并行库将被添加到新系统中。这种方法的优点是，一个新的静态分析工具的设计者只需要为一种语言设计工具-Ciffl-然后就可以“免费”获得一个可以在所有源代码库上工作的工具。同样，当一个新的并行库出现时，通过开发一个从ITT到CIVL的翻译器，人们可以立即获得所有静态分析工具的好处。研究人员预计，由此产生的平台将使开发正确的并行程序变得更加容易，无论这种并行性是如何表达的。

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.