Path-sensitive race detection with partial order reduced symbolic execution

Abstract

This paper presents a combination of symbolic execution and partial order reduction to achieve path-sensitive race detection. The presented approach limits the complexity of symbolic execution of multithreaded code by applying it with a fixed scheduling algorithm only. Alternative thread interleavings are generated from fixed-scheduling ones with ample set partial order reduction on an abstraction level of thread interactions. Races are detected on the abstraction level. The proposed algorithm is implemented as plug-in extension of Eclipse CDT and evaluated by running it on the race condition test cases from the Juliet suite.