Back to Search
Start Over
A Practical Approach for Model Checking C/C++11 Code
- Source :
- ACM Transactions on Programming Languages and Systems. 38:1-51
- Publication Year :
- 2016
- Publisher :
- Association for Computing Machinery (ACM), 2016.
-
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.
- Subjects :
- Model checking
Unit testing
Programming language
business.industry
Computer science
Concurrent data structure
020207 software engineering
02 engineering and technology
Parallel computing
computer.software_genre
Toolchain
Allocator
Software
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Memory model
business
computer
Queue
Subjects
Details
- ISSN :
- 15584593 and 01640925
- Volume :
- 38
- Database :
- OpenAIRE
- Journal :
- ACM Transactions on Programming Languages and Systems
- Accession number :
- edsair.doi...........5ea19f3520cc0e84f64301e4c1f7a0ad