SHF: Small: CDSChecker: Model-Checking Concurrent Data Structures under the C11/C++11 Memory Model

SHF：小：CDSChecker：C11/C 11 内存模型下的模型检查并发数据结构

• 批准号: 1319786
• 负责人: Brian Demsky
• 金额: $ 40万
• 依托单位: University of California-Irvine
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-10-01 至 2018-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319786&HistoricalAwards=false
• 关键词: SHF; Small; CDSChecker; Model; Checking

Society has long relied on increasing computing power to drivetechnological development. Continuing this trend in the multi-core erawill require a large scale migration to parallel software. As anacknowledgment of the new importance of parallelism in softwaredevelopment, the 2011 C and C++ standards extended C and C++ withlanguage support for low-level atomic operations to allow developersto write portable efficient concurrent data structures.Unfortunately, implementing concurrent data structures is extremelydifficult to do correctly. Despite the difficulties, we expect thatthe potential performance benefits will lure many developers, bothexperts and others, to attempt to develop customized concurrent datastructures. Without tool support, this will inevitably lead topotentially costly failures in deployed software.This project will explore techniques for efficiently model checkingconcurrent data structures under the C/C++ memory model and supportfor developers to effectively use a model checker for testing anddebugging code. These techniques will be implemented in the form of aconcurrent data structure checking tool, CDSChecker, that will bedeveloped by the this project. The project will develop efficientmodel-checking techniques for the C/C++ memory model, explore how tospecify the correct behavior of concurrent data structures, explorehow to support testing and debugging of concurrent code, and explorehow to effectively communicate information about concurrency bugs todevelopers.

长期以来，社会一直依赖于不断增长的计算能力来推动技术发展。在多核时代继续这一趋势将需要大规模迁移到并行软件。 作为对并行性在软件开发中新的重要性的认可，2011年的C和C++标准扩展了C和C++对低级原子操作的语言支持，以允许开发人员编写可移植的高效并发数据结构。不幸的是，实现并发数据结构是非常困难的。尽管困难重重，但我们预计潜在的性能优势将吸引许多开发人员，包括专家和其他人，尝试开发定制的并发数据结构。 如果没有工具的支持，这将不可避免地导致潜在的昂贵的失败部署的软件。这个项目将探讨技术，有效地模型检查并发数据结构下的C/C++内存模型和支持开发人员有效地使用模型检查器进行测试和调试代码。这些技术将以本项目开发的并行数据结构检查工具CDSocket.com的形式实现。 该项目将为C/C++内存模型开发有效的模型检查技术，探索如何指定并发数据结构的正确行为，探索如何支持并发代码的测试和调试，以及探索如何有效地向开发人员传达有关并发错误的信息。