Skip to main content
eScholarship
Open Access Publications from the University of California

CDSSPEC: Testing Concurrent Data Structures Under the C/C++11 Memory Model

  • Author(s): Ou, Peizhao
  • Advisor(s): Demsky, Brian
  • et al.
Abstract

Concurrent data structures often provide better performance on multi-core platforms, but are significantly more difficult to design and verify than their sequential counterparts. The C/C++11 standard introduced a weak language memory model supporting low-level atomic operations such as compare and swap (CAS). While these atomic operations can significantly improve the performance of concurrent data structures, programming at this level introduces non-intuitive behaviors that significantly increase the difficulty of developing code.

In this paper, we present CDSSPEC, a specification language checker that allows developers to write simple specifications for low-level concurrent data structures that make use of C/C++11 atomics and check the correctness of concurrent data structures against these specifications. We have evaluated CDSSPEC by annotating and checking several concurrent data structures.

Main Content
Current View