Society has long relied on increasing computing power to drive technological development. Continuing this trend in the multi-core era will require a large scale migration to parallel software. As an acknowledgment of the new importance of parallelism in software development, the 2011 C and C++ standards extended C and C++ with language support for low-level atomic operations to allow developers to write portable efficient concurrent data structures. Unfortunately, implementing concurrent data structures is extremely difficult to do correctly. Despite the difficulties, we expect that the potential performance benefits will lure many developers, both experts and others, to attempt to develop customized concurrent data structures. Without tool support, this will inevitably lead to potentially costly failures in deployed software.
This project will explore techniques for efficiently model checking concurrent data structures under the C/C++ memory model and support for developers to effectively use a model checker for testing and debugging code. These techniques will be implemented in the form of a concurrent data structure checking tool, CDSChecker, that will be developed by the this project. The project will develop efficient model-checking techniques for the C/C++ memory model, explore how to specify the correct behavior of concurrent data structures, explore how to support testing and debugging of concurrent code, and explore how to effectively communicate information about concurrency bugs to developers.
