Recurrent Sets for Non-Termination and Safety of Programs

Termination and non-termination are a pair of fundamental program properties. Arguably, the majority of code is required to terminate, e.g., dispatch routines of drivers or other event-driven code, GPU programs, etc – and the existence of non-terminating executions is a serious bug. Such a bug may manifest by freezing a device or an entire system, or by causing a multi-region cloud service disruption. Thus, proving termination is an interesting problem in the process of establishing correctness, and proving non-termination is a complementary problem that is interesting for debugging. This work considers a sub-problem of proving non-termination – the problem of finding recurrent sets. A recurrent set is a way to compactly represent the set of nonterminating executions of a program and is a set of states from which an execution of the program cannot or may not escape (there exist multiple definitions that differ in modalities). A recurrent set acts as a part of a non-termination proof. If we find a nonempty recurrent set and are able to show its reachability from an initial state – then we prove the existence of a non-terminating execution. Most part of this work is devoted to automated static analyses that find recurrent sets in imperative programs. We follow the general framework of abstract interpretation and go all the way from trace semantics of programs to practical analyses that compute abstract representations of recurrent sets. In particular, we present two novel analyses. The first one is based on abstract pre-condition computation (backward analysis) and trace partitioning and focuses on numeric programs (but with some modifications it may be applicable to non-numeric ones). In popular benchmarks, it performs comparably to state-of-the-art tools. The second analysis is based on abstract post-condition computation (forward analysis) and is readily applicable to non-numeric (e.g., heap-manipulating) programs, which we demonstrate by tackling examples from the domain of shape analysis with 3-valued logic. As it turns out, recurrent sets can be used in establishing other properties as well. For example, recurrent sets are used in CTL model checking of programs. And as part of this work, we were able to apply recurrent sets in the process of establishing sufficient pre-conditions for safety