Scalable, Precise, and Effective Analyses for Detecting Race Conditions

用于检测竞争条件的可扩展、精确且有效的分析

• 批准号: 0541036
• 负责人: Michael Hicks
• 金额: $ 36万
• 依托单位: University of Maryland, College Park
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-09-01 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541036&HistoricalAwards=false
• 关键词: Scalable; Precise; Effective; Analyses; Detecting

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.

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