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

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 por...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 2016-05, Vol.38 (3), p.1-51, Article 10
Main Authors: Norris, Brian, Demsky, Brian
Format: Article
Language:English
Subjects:
Assembly
C++ (programming language)
Computer programs
Consumption
Queues
Software
Software and its engineering
Software creation and management
Software defect analysis
Software testing and debugging
Software verification and validation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 CDSChecker, a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We have used CDSChecker 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.
ISSN:0164-0925
1558-4593
DOI:10.1145/2806886