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

点击翻译按钮获取中文摘要

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.