Verifying eventual consistency of optimistic replication systems

Speaker

Ahmed Bouajjani, University of Paris Diderot, France

Date and Time

Wednesday, June 11th, 2014 at 10:15.

Location

Polacksbacken, room 4308

Abstract

We address the verification problem of eventual consistency of optimistic replication systems. Such systems are typically used to implement distributed data structures over large scale networks. We introduce a formal definition of eventual consistency that applies to a wide class of existing implementations, including the ones using speculative executions. Then, we reduce the problem of checking eventual consistency to reachability and model checking problems. This reduction enables the use of existing verification tools for message-passing programs in the context of verifying optimistic replication systems. Furthermore, we derive from these reductions decision procedures for checking eventual consistency of systems implemented as finite-state programs communicating through unbounded unordered channels.