JAIST Logic@JAIST

CDSChecker: Checking Concurrent Data Structures Written with C/C++ Atomics

  • Brian Demsky, University of California Irvine
  • Brian Demsky is an Associate Professor in the Electrical Engineering and Computer Science Department at the University of California, Irvine. His current research interests include software reliability, security, software engineering, compilation, parallel software, program analysis, and program understanding. He received his B.S. degrees in Physics and Electrical Engineering from the University of Texas, Austin in 1998, his M.S. degree in Computer Science from MIT in 2001, and his Ph.D. degree in Computer Science from MIT in 2006.
Date: 2015/01/09 (Fri) 15:00 to 17:00
Place: JAIST IS school seminar room 6 (6F)
Group: Research Center for Software Verification
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. Developing correct low-level concurrent code is well-known to be especially difficult under a weak memory model, where code behavior can be surprising. Building reliable concurrent software using C/C++ low-level atomic operations will likely require tools that help developers discover unexpected program behaviors. In this paper we present CDSChecker, a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We develop several novel techniques for modeling the relaxed behaviors allowed by the memory model and for minimizing the number of execution behaviors that CDSChecker must explore. We have used CDSChecker to exhaustively unit test several concurrent data structure implementations on specific inputs and have discovered errors in both a recently published C11 implementation of a work-stealing queue and a single producer, single consumer queue implementation.
Contact nao-aoki