Name
Abstract | ||
|---|---|---|
To cope with large data sets, distributed data stores partition their data across servers. However, real-world systems usually do not provide useful transactional semantics for operations accessing multiple partitions due to the delays involved in achieving multi-partition consistency. Read Atomic Multi-Partition (RAMP) transactions have recently been proposed as efficient light-weight multi-partition transactions that guarantee read atomicity: either all updates or no updates of a transaction are visible to other transactions. In this paper we formalize RAMP transactions in rewriting logic and perform model checking verification of key properties using the Maude tool. In particular, we develop detailed formal models---and formally analyze---a number of extensions and optimizations of RAMP that are only briefly mentioned by the RAMP developers. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2851613.2851838 | SAC |
Field | DocType | Citations |
Atomicity,Data set,Programming language,Model checking,Computer science,Server,Rewriting,Database transaction,Distributed transaction,Semantics | Conference | 5 |
PageRank | References | Authors |
0.45 | 11 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Si Liu | 1 | 42 | 4.43 |
| Peter Csaba Ölveczky | 2 | 864 | 57.59 |
| Muntasir Raihan Rahman | 3 | 455 | 21.21 |
| Jatin Ganhotra | 4 | 6 | 0.80 |
| Indranil Gupta | 5 | 1837 | 143.92 |
| José Meseguer | 6 | 9533 | 805.39 |