Name
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2535838.2535877 | POPL |
Keywords | Field | DocType |
large scale network,message-passing program,optimistic replication system,model checking problem,formal definition,data structure,verification problem,verification tool,eventual consistency,finite-state program,static program analysis,model checking | Optimistic replication,Static program analysis,Eventual consistency,Sequential consistency,Model checking,Computer science,Theoretical computer science,Implementation,Reachability,Consistency model,Distributed computing | Conference |
Volume | Issue | ISSN |
49 | 1 | 0362-1340 |
Citations | PageRank | References |
19 | 0.83 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ahmed Bouajjani | 1 | 2663 | 184.84 |
| Constantin Enea | 2 | 249 | 26.95 |
| Jad Hamza | 3 | 71 | 6.44 |