# 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.