SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresRemote
Concolic testing combines concrete execution with symbolic execution to automatically generate test inputs that exercise different program paths and deliver high code coverage. This approach has been extended to multithreaded programs for exposing data races. Multithreaded programs frequently rely upon concurrent dynamic data structures whose implementations may contain data races that manifest only when certain dynamic data structure shapes, program paths, and thread interleavings are exercised. The lack of support for exploring different data structure shapes compromises the detection of races. This paper presents a summarization-guided approach for concolic testing capable of efficiently exploring different dynamic data structure shapes to expose data races. Via unit testing of key functions, function summaries are generated that capture data structure shapes that cause various function paths to be exercised. The shapes are captured in the form of pointer-pointee relations among symbolic pointers. By reusing function summaries during concolic testing, much of the overhead of handling symbolic pointers and dynamic objects in summarized functions is avoided. The summary also contains symbolic memory accesses and synchronization events that guide application-level concolic testing first to identify and then confirm potential data races. We demonstrate the efficiency and efficacy of our approach via experiments with multithreaded programs performing concurrent operations on four widely used dynamic data structures - Skip List, Unrolled Linked List, Priority Queue, and AVL Tree. It increases the number of races detected from 34 to 74 in total in comparison to Cloud9, and reduces both constraints solving time and number of constraints needed to be solved via summarization.
Tue 25 JunDisplayed time zone: Windhoek change
16:00 - 17:00 | ISMM: Session 4 - PotpourriISMM 2024 at Iceland Chair(s): Tony Hosking Australian National University | ||
16:00 20mTalk | SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresRemote ISMM 2024 Xiaofan Sun University of California at Riverside, Rajiv Gupta University of California at Riverside DOI | ||
16:20 20mTalk | A Heuristic for Periodic Memory Allocation with Little Fragmentation to Train Neural Networks ISMM 2024 DOI | ||
16:40 20mTalk | ESPN: Memory-Efficient Multi-vector Information Retrieval ISMM 2024 DOI |