Generating data race witnesses by an SMT-based analysis

摘要: Data race is one of the most dangerous errors in multithreaded programming, and despite intensive studies, it remains a notorious cause failures concurrent systems. Detecting data races already hard problem, yet even harder for programmer to decide whether or how reported can appear actual program execution. In this paper we propose an algorithm generating debugging aid information called witnesses, which are concrete thread schedules that deterministically trigger races. More specifically, given execution trace, e.g. non-erroneous may have triggered warning Eraser-style detectors, use symbolic analysis based on SMT solvers search witness among alternative interleavings events trace. Our precisely encodes sequential consistency semantics using scalable predictive model ensure always feasible.