# Checking Robustness Against Snapshot Isolation

## TL;DR

This paper presents a method to verify if programs maintain correctness under snapshot isolation by reducing the problem to a state reachability analysis, enabling reuse of existing verification techniques.

## Contribution

It introduces a polynomial-time reduction from robustness verification against snapshot isolation to state reachability, facilitating the application of classic verification methods.

## Key findings

- Verification problem is polynomial-time reducible to state reachability.
- Reduction enables reuse of classic verification techniques.
- Proof technique based on Lipton's reduction theory for robustness.

## Abstract

Transactional access to databases is an important abstraction allowing programmers to consider blocks of actions (transactions) as executing in isolation. The strongest consistency model is {\em serializability}, which ensures the atomicity abstraction of transactions executing over a sequentially consistent memory. Since ensuring serializability carries a significant penalty on availability, modern databases provide weaker consistency models, one of the most prominent being \emph{snapshot isolation}. In general, the correctness of a program relying on serializable transactions may be broken when using weaker models. However, certain programs may also be insensitive to consistency relaxations, i.e., all their properties holding under serializability are preserved even when they are executed over a weak consistent database and without additional synchronization. In this paper, we address the issue of verifying if a given program is {\em robust against snapshot isolation}, i.e., all its behaviors are serializable even if it is executed over a database ensuring snapshot isolation. We show that this verification problem is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. This reduction opens the door to the reuse of the classic verification technology for reasoning about weakly-consistent programs. In particular, we show that it can be used to derive a proof technique based on Lipton's reduction theory that allows to prove programs robust.