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

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

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.