Scalable, Precise, and Effective Analyses for Detecting Race Conditions

奖abstract0541036马里兰大学帕克分校的Michael HicksU可扩展的，精确的，有效的分析检测竞争条件Michael W. Hicks Jeffrey S. foster多线程编程是关键软件，如操作系统和网络服务器的重要组成部分。随着硬件制造商正在构建和交付多cpu核心机器，多线程编程可能会变得更加普遍。多线程程序中一个常见的错误来源是数据争用，当两个线程同时访问相同的数据时，就会发生数据争用。众所周知，竞争条件是难以发现的错误，可能导致不正确的行为、数据损坏、程序失败、拒绝服务攻击和/或安全漏洞。由于竞态条件可能非常有害，因此人们对开发检测和预防竞态条件的工具产生了广泛的兴趣。然而，这些工具仍然不切实际。该研究将开发使用静态（整个程序）分析来证明C程序中不存在竞争条件的工具。这些工具将基于一种通用的注释和规范语言，这种语言可以描述用于防止数据争用的常用习惯用法。最终的目标是开发可扩展到大型软件系统的技术，并且这些技术是基于可靠的基础之上的。

AWARD ABSTRACT0541036Michael HicksU of Maryland College ParkScalable, Precise, and Effective Analyses for Detecting Race Conditions Michael W. Hicks Jeffrey S. FosterMulti-threaded programming is an essential part of critical software such as operating systems and network servers. Multi-threaded programming is likely to become far more prevalent as hardware manufacturers are now building and shipping multi-CPU core machines. One common source of errors in multi-threaded programs is data races, which occur when two threads each concurrently access the same data.Race conditions are notoriously hard-to-find errors that can lead to incorrect behavior, data corruption, program failure, denial-of-service attacks, and/or security breaches. Because race conditions can be so pernicious, there has been widespread interest in developing tools for detecting and preventing them. However, these tools are still impractical. The research will develop tools that use static (whole-program) analysis to prove the absence of race conditions in C programs. The tools will be based on a common annotation and specification language that can describe commonly-used idioms for preventing data races. The goal is ultimately to develop techniques that scale to large software systems, and that are based on a sound foundation.