Forcing small models of conditions on program interleaving for detection of concurrent bugs.

ABSTRACTIs it possible to efficiently reveal concurrency bugs by forcing a well selected set of conditions on program interleaving? To study this general question, we defined two simple models of conditions on program interleaving targeted at the insufficient-synchronization-scope bug pattern. We analyzed these models with respect to several buggy programs. We also implemented an algorithm that tries to force one of these models. The analysis of these models shows that relatively small models can detect insufficient-synchronization-scope bugs. The experiments with the forcing algorithm demonstrated the ability of finding the bug with high efficiency: the average testing time till the bug is detected was improved by factors of 7 and 73 compared with the average time required by a dynamic exploration that did not incorporate the forcing algorithm.