SSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures
summary
SSRD implements summarization-guided concolic testing that generates function summaries from unit testing (capturing pointer-pointee relations and symbolic memory accesses), then reuses those summaries during whole-program concolic runs to avoid recreating symbolic heap and reduce constraint solving. Experiments on Skip List, Unrolled Linked List, Priority Queue and AVL Tree compare against Cloud9: SSRD raises detected races from 34→74 races, cuts constraint-solving work and shows per-benchmark runtime reductions (example: ~47% less execution time excluding summary build).
AI-written summary · about
chapters (10)
- 0:00SSRD and concurrent data structures
- 1:07Concolic testing for multi-threaded
- 2:33Data shapes in race detection
- 3:58Performance challenges in shape
- 5:23Function summaries for efficiency
- 8:18Summaries in testing
- 10:31Two-stage race detection
- 12:19Experimental evaluation of SSRD
- 14:09Summarization impact on performance
- 16:25Conclusion and future
related talks
24mRacerD - Compositional Static Race Detection
01h 04mDebugging data races
22mData race detection
18mSound Static Data Race Verification for C: Is the Race Lost?
15mSound and partially-complete static analysis of data-races in GPU programs
07mRace Conditions in Details
32mEventRacer: Finding Concurrency Errors in Event-Driven Applications
20mRRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures