Sciweavers

Share
NFM
2011

Generating Data Race Witnesses by an SMT-Based Analysis

8 years 1 months ago
Generating Data Race Witnesses by an SMT-Based Analysis
Abstract. Data race is one of the most dangerous errors in multithreaded programming, and despite intensive studies, it remains a notorious cause of failures in concurrent systems. Detecting data races is already a hard problem, and yet it is even harder for a programmer to decide whether or how a reported data race can appear in the actual program execution. In this paper we propose an algorithm for generating debugging aid information called witnesses, which are concrete thread schedules that can deterministically trigger the data races. More specifically, given a concrete execution trace, e.g. non-erroneous one which may have triggered a warning in Eraser-style data race detectors, we use a symbolic analysis based on SMT solvers to search for a data race witness among alternative interleavings of events of that trace. Our symbolic analysis precisely encodes the sequential consistency semantics using a scalable predictive model to ensure that the reported witness is always feasible....
Mahmoud Said, Chao Wang, Zijiang Yang, Karem Sakal
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where NFM
Authors Mahmoud Said, Chao Wang, Zijiang Yang, Karem Sakallah
Comments (0)
books