Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code
Charles Edwin Killian, James W. Anderson, Ranjit Jhala, Amin M. Vahdat · 2015
Modern software model checkers find safety violations: breaches where the system has entered some bad state. For many environments however, particularly complex con-current and distributed systems, we argue that liveness properties are both more natural to specify and more im-portant to check. Liveness conditions specify desirable system conditions in the limit, with the expectation that they will be temporarily violated, perhaps as a result of failure or during system initialization. Existing software model checkers cannot verify live-ness because doing so requires finding an infinite exe-cution that never satisfies one or more liveness proper-ties. We present algorithms to find liveness violations with high probability and the critical transition that moves the system from an indeterminate state, where liveness can still be achieved despite a temporary violation, to a dead state, where it becomes impossible to ever achieve live-ness. We present MACEMC, a software model checker that implements our algorithms and finds complex live-ness errors in implementations of PASTRY, a reliable transport protocol, and an overlay tree. 1