Thu 11 Jan 2018 10:55 - 11:20 at Bunker Hill - Consistency Chair(s): Xinyu Feng

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 \emph{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), and thus guaranteeing that checking inductiveness 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.

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
ConsistencyResearch Papers at Bunker Hill
Chair(s): Xinyu Feng University of Science and Technology of China
10:30
25m
Talk
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Research Papers
Michael Emmi Nokia Bell Labs, Constantin Enea Université Paris Diderot
10:55
25m
Talk
Reducing Liveness to Safety in First-Order Logic
Research Papers
Oded Padon Tel Aviv University, Jochen Hoenicke Universität Freiburg, Giuliano Losa University of California at Los Angeles, USA, Andreas Podelski University of Freiburg, Germany, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
11:20
25m
Talk
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Research Papers
Gowtham Kaki Purdue University, Kartik Nagar Purdue University, Mahsa Najafzadeh Purdue University, Suresh Jagannathan Purdue University
11:45
25m
Talk
Programming and Proving with Distributed Protocols
Research Papers
Ilya Sergey University College London, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle
DOI Pre-print