Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning

Characterizing the set of reachable states of a distributed protocol that uses asynchronous message-passing communication is difficult due to the exponential number of possible interleavings of local executions. Any syntactic expression overapproximating the set of reachable states is an invariant formula of the system, and is a valuable tool that can aid programmers in understanding global program behavior. In this paper, we propose a method for obtaining a formula that approximates the set of reachable states; we call this formula a likely invariant, and we learn it using information only obtained from system executions. Our method doubles up as a way for identifying states that may not be known to be reachable (based on the best-known likely invariant) and hence may appear anomalous to the system designer. In some cases, they may be actually anomalous and may indicate a lurking (heisenbug). Our method has the following main steps: (1) we observe the global states of the system reached during its execution, (2) we asynchronously learn a likely invariant from the observed global states, (3) we monitor the learned likely invariant for the system states that do not satisfy it, and (4) if such states are found, we revise the likely invariant. We implement our overall methodology for a number of distributed protocols written in the Promela language and show that our technique can learn useful information about the system from just runtime executions.