Invisible Invariants in the Spotlight

We study the problem of automatically proving parameterized mutual exclusion algorithms mutually exclusive. In our first contribution we show that the problem remains undecidable even for a very weak model of computation. In this model agents have no identities but can iterate over all agents. This iteration, however, is executed in an arbitrary sequence which is only guaranteed to contain every agent at least once. Further, we show that checking if a set of configurations describable in first-order logic is an invariant is also undecidable. In our second contribution we present an automatic procedure, based on first-order theorem proving, that constructs small and readable inductive invariants of a given algorithm. This procedure leverages invariants that can be used to prove finite instances of the parametric algorithms correct. Formulating generalizations of these invariants in first-order logic allows us to use the mature tooling of automated theorem proving to discharge required proof obligations. Moreover, we can give externally verifiable certificates of positive results as a sequence of first-order problems which collectively prove the desired property of the parameterized system. We show that this technique is able to automatically produce modular proofs of mutual exclusion for basic algorithms from the literature.