  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.
