Reducing Liveness to Safety in First-Order Logic

Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham.

POPL 2018.

(paper) (examples source files) (artifact virtual machine)

Abstract

We develop a new technique for verifying temporal properties of infinite-state (distributed) systems. The main idea is to reduce the temporal verification problem to the problem of verifying the safety of infinite-state systems expressed in first-order logic. This allows to leverage existing techniques for safety verification to verify temporal properties of interesting distributed protocols, including some that have not been mechanically verified before.

We model infinite-state systems using first-order logic, and use first-order temporal logic (FO-LTL) to specify temporal properties. This general formalism allows to naturally model distributed systems, while supporting both unbounded-parallelism (where the system is allowed to dynamically create processes), and infinite-state per process.

The traditional approach for verifying temporal properties of infinite-state systems employs well-founded relations (e.g. using linear arithmetic ranking functions). In contrast, our approach is based the idea of fair cycle detection. In finite-state systems, temporal verification can always be reduced to fair cycle detection (a system contains a fair cycle if it revisits a state after satisfying all fairness constraints). However, with both infinitely many states and infinitely many fairness constraints, a straightforward reduction to fair cycle detection is unsound. To regain soundness, we augment the infinite-state transition system by a dynamically computed finite set, that exploits the locality of transitions. This set lets us define a form of fair cycle detection that is sound in the presence of both infinitely many states, and infinitely many fairness constraints. Our approach allows a new style of temporal verification that does not explicitly involve ranking functions. This fits well with pure first-order verification which does not explicitly reason about numerical values. In particular, it can be used with effectively propositional first-order logic (EPR), in which case checking verification conditions is decidable.

We applied our technique to verify temporal properties of several interesting protocols. To the best of our knowledge, we have obtained the first mechanized liveness proof for both TLB Shootdown, and Stoppable Paxos.

Artifact

(artifact virtual machine) SHA-256 checksum: f566a53f4064ae7a9fac5819c4596aa1f79e1e0193905c736cec7f8dbf306426

The artifact is provided by a VirtualBox virtual machine that contains Ivy and Z3 installed, and contains Ivy files for the benchmarks described in the paper. This allows to examine the Ivy source files and also check them with Ivy (which internally uses Z3). The Ivy source files contain transition systems after applying the liveness to safety reduction, and a suitable inductive invariant (denoted by the Ivy keyword conjecture). To check the safety using Ivy, open a terminal and run:

ivyuser@ivyvm:~$ cd reducing-liveness-to-safety-in-first-order-logic
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ ivy_check ticket_protocol.ivy
...
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ ivy_check alternating_bit_protocol.ivy
...
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ ivy_check tlb-termination.ivy  # this example takes a few minutes
...
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ ivy_check paxos_liveness/paxos_liveness.ivy
...
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ ivy_check paxos_liveness/multi_paxos_liveness.ivy
...
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ ivy_check paxos_liveness/stoppable_paxos_liveness.ivy
...

For each example, after printing some text, Ivy should print OK, which means the safety of the transition system is verified, thus proving the liveness property of the original transition system. The Ivy files contain comments that explain the system and property formalized in each file. If you wish to modify the Ivy source files, for example by commenting out some of the conjectures, you can use ivy_check diagnose=true <filename> to examine counterexamples to induction.

Alternatively, you can run all benchmarks using a python script:

ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ python run_experiment.py
...
ivyuser@ivyvm:~/reducing-liveness-to-safety-in-first-order-logic$ python analyze_results.py
...

The virtual machine's user name is ivyuser and the password is ivy.

Note that run times reported in the paper are not measured in a virtual machine, so you could expect to get different performance.