Department of Information Technology

Verifying eventual consistency of optimistic replication systems


Ahmed Bouajjani, University of Paris Diderot, France

Date and Time

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


Polacksbacken, room 4308


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.

Updated  2014-06-10 13:55:14 by Mohamed Faouzi Atig.