A Practical Approach for Model Checking C/C++11 Code

Abstract

Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak memory model, enabling developers to write portable and efficient multithreaded code. In this article, we present CDSC hecker , a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We have used CDSC hecker to exhaustively unit test concurrent data structure implementations and have discovered errors in a published implementation of a work-stealing queue and a single producer, single consumer queue.