A New Distributed Transaction Protocol and Its Formal Analysis in Maude

Designers of distributed database systems face the choice between performance and consistency guarantees: with stronger consistency guarantees comes higher transactional latency and lower throughput. Certain collaborative editing application scenarios only require read atomicity (either all or none of a transaction's updates are visible to another transaction) and no lost updates (all updates are incrementally performed). Many existing distributed database systems meet these requirements. However, they all provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets application scenarios where only read atomicity and no lost updates are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA's satisfaction of read atomicity and prevention of lost updates. Our results show that ROLA satisfies the correctness properties with a bounded number of parameters. To analyze performance we: (a) perform statistical model checking to analyze key performance properties such as throughput, averange latency, and commit rate; and (b) compare these performance results with those obtained by also modeling and analyzing in Maude the same performance properties for Walter, a well-known high-performance protocol meeting the requirements of read atomicity and preservation of lost updates. Our statistical model checking results show that ROLA outperforms Walter.Ope