作者:
Y Yang，X Chen，G Gopalakrishnan
关键词:
摘要:
We present Inspect, a runtime model checker for revealing concurrency bugs in mul- tithreaded C programs. Inspect instruments a given program at all global interaction points, and with the help of a new scheduler, examines all relevant thread interleavings under dynamic partial order reduction (DPOR). While the ideas behindInspect are well known, there hasn't been a previously reported effort in which these ideas are applied to multithreaded C programs. We report on our engineering efforts to endow Inspect with (i) automatic source program instrumentation, (ii) practical DPOR implementation, and (iii) optimizations such as using locksets to compute more precise co-enabled relation. Our initial experience shows that such a tool can, indeed, be very effective for obtaining a han- dle on the notorious complexity of thread programming.
在线下载