Scaling model checking of dataraces using dynamic information

Dataraces in multithreaded programs often indicate severe bugs and can cause unexpected behaviors when different thread interleavings are executed. Because dataraces are a cause for concern, many works have dealt with the prob-lem of detecting them. Works based on dynamic techniques either report errors only for dataraces that occur in the cur-rent interleaving, which limits their usefulness, or produce many spurious dataraces. Works based on model checking search exhaustively for dataraces and thus can reveal even those that occur in rarely executed paths. However, the ap-plicability of model checking is limited because the large number of thread interleavings in realistic multithreaded programs causes state space explosion. In this work, we combine the two techniques in a hybrid scheme which over-comes these difficulties and enjoys the advantages of both worlds. Our hybrid technique succeeds in providing thread interleavings that prove the existence of dataraces in realistic programs. The programs we experimented with cannot be checked using either an ordinary industrial strength model checker or bounded model checking