Runtime Model Checking of Multithreaded C/C++ Programs
The authors present inspect, a tool for model checking safety properties of multithreaded C/C++ programs where threads interact through shared variables and synchronization primitives. The given program is mechanically transformed into an instrumented version that yields control to a centralized scheduler around each such interaction. The scheduler first enables an arbitrary execution. It then explores alternative interleavings of the program. It avoids redundancy exploration through Dynamic Partial Order Reduction (DPOR). The authors' initial experience shows that inspect is effective in testing and debugging multithreaded C/C++ programs. They are not aware of DPOR having been implemented in such a setting. With inspect, they have been able to find many bugs in real applications.