- Main
CDSSPEC: Testing Concurrent Data Structures Under the C/C++11 Memory Model
- Ou, Peizhao
- Advisor(s): Demsky, Brian
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
Enter the password to open this PDF file:
-
-
-
-
-
-
-
-
-
-
-
-
-
-