Fair stateless model checking - Musuvathi, Madanlal; Qadeer, Shaz; Musuvathi, Madan (PLDI 08: Programming Language Design and Implementation, 2008)
Stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. Existing stateless model checkers are limited to the veriﬁcation of safety properties on terminating programs. However, realistic concurrent programs are nonterminating, a property that signiﬁcantly reduces the efﬁcacy of stateless model checking in testing them. Moreover, existing stateless model checkers are unable to verify that a nonterminating program satisﬁes the important liveness property of livelock-freedom, a property that requires the program to make continuous progress for any input. To address these short comings, this paper argues for incorporating a fair scheduler in stateless exploration. The key contribution of this paper is an explicit scheduler that is (strongly) fair and at the same time sufﬁciently nondeterministic to guarantee full coverage of safety properties. We have implemented the fair scheduler in the CHESS modelchecker. We show through theoretical arguments and empirical evaluation that our algorithm satisﬁes two important properties: 1) it visits all states of a ﬁnite-state program achieving state coverage at a faster rate than existing techniques, and 2) it ﬁnds all livelocks in a ﬁnite-state program. Before this work, nonterminating programs had to be manually modiﬁed in order to apply CHESS to them. The addition of fairness has allowed CHESS to be effectively applied to real-world nonterminating programs without any modiﬁcation. For example, we have successfully booted the Singularity operating system under the control of CHESS.