Checking Robustness Between Weak Transactional Consistency Models

Concurrent accesses to databases are typically encapsulated in transactions in order to enable isolation from other concurrent computations and resilience to failures. Modern databases provide transactions with various semantics corresponding to different trade-offs between consistency and availability. Since a weaker consistency model provides better performance, an important issue is investigating the weakest level of consistency needed by a given program (to satisfy its specification). As a way of dealing with this issue, we investigate the problem of checking whether a given program has the same set of behaviors when replacing a consistency model with a weaker one. This property known as robustness generally implies that any specification of the program is preserved when weakening the consistency. We focus on the robustness problem for consistency models which are weaker than standard serializability, namely, causal consistency, prefix consistency, and snapshot isolation. We show that checking robustness between these models is polynomial time reducible to a state reachability problem under serializability. We use this reduction to also derive a pragmatic proof technique based on Lipton’s reduction theory that allows to prove programs robust. We have applied our techniques to several challenging applications drawn from the literature of distributed systems and databases.

OpenMemDB: A Wait-Free, In-Memory Database

OpenMemDB is an in-memory database that is implemented solely using wait-free data structures. OpenMemDB is the first and only database currently developed in such a way. OpenMemDB also provides linearizable correctness guarantees for all operations executed on the database. OpenMemDB uses a form of snapshot isolation to ensure linearizability, and avoids the write-skew problem that can occur when using snapshot isolation by eliminating writes that are out of data. OpenMemDBs biggest contribution is its completely wait-free implementation. Every operation executed in OpenMemDB is guaranteed to be wait-free and linearizable. This implementation also scales competitively when compared against similar in-memory database management systems. OpenMemDB achieves its best scaling in select heavy operation loads with nearly 12 times speedup at 16 threads. This is better scaling than either VoltDB or MemSQL showed in our testing.