Serializability (SER) and snapshot isolation (SI) are widely used transactional isolation levels in database systems. The isolation checking problem asks whether a given execution history of a database system satisfies a specified isolation level. However, existing SER and SI checkers, whether traditional black-box checkers or recent timestamp-based white-box ones, operate offline and require the entire history to be available to construct a dependency graph, making them unsuitable for continuous and ever-growing histories. This paper addresses online isolation checking by extending the timestamp-based isolation checking approach to online settings. Specifically, we design Chronos, an efficient timestamp-based offline SI checker. Chronos is incremental and avoids constructing a start-ordered serialization graph for the entire history, making it well-suited for online scenarios. We further extend Chronos into an online SI checker, Aion, addressing several key challenges unique to online settings. Additionally, we develop Aion-SER for online SER checking. Experiments highlight that Chronos processes offline histories with up to one million transactions in seconds, greatly outperforming existing SI checkers. Furthermore, Aion and Aion-ser sustain a throughput of approximately 12K transactions per second, demonstrating their practicality for online isolation checking.

Transactional isolation guarantees are crucial for database correctness. However, recent studies have uncovered numerous isolation bugs in production databases. The common black-box approach to isolation checking stresses databases with large, concurrent, randomized transaction workloads and verifies whether the resulting execution histories satisfy specified isolation levels. For strong isolation levels such as strict serializability, serializability, and snapshot isolation, this approach often incurs significant end-to-end checking overhead during both history generation and verification. We address these inefficiencies through the novel design of Mini-Transactions (MTs). MTs are compact, short transactions that execute much faster than general workloads, reducing overhead during history generation by minimizing database blocking and transaction retries. By leveraging MTs' read-modify-write pattern, we develop highly efficient algorithms to verify strong isolation levels in linear or quadratic time. Despite their simplicity, MTs are semantically rich and effectively capture common isolation anomalies described in the literature. We implement our verification algorithms and an MT workload generator in a tool called MTC. Experimental results show that MTC outperforms state-of-the-art tools in both history generation and verification. Moreover, MTC can detect bugs across various isolation levels in production databases while maintaining the effectiveness of randomized testing with general workloads, making it a cost-effective solution for black-box isolation checking.

Substantial research efforts have been devoted to studying the performance optimality problem for distributed database transactions. However, they focus just on optimizing transactional reads, and thus overlook crucial factors, such as the efficiency of writes, which also impact the overall system performance. Motivated by a recent study on Twitter's workloads showing the prominence of write-heavy workloads in practice, we make a substantial step towards performance-optimal distributed transactions by also aiming to optimize writes, a fundamentally new dimension to this problem. We propose a new design objective and establish impossibility results with respect to the achievable isolation levels. Guided by these results, we present two new transaction algorithms with different isolation guarantees that fulfill this design objective. Our evaluation demonstrates that these algorithms outperform the state of the art.

Transactional isolation is critical to the functional correctness of database management systems (DBMSs). Much effort has recently been devoted to finding isolation bugs and validating isolation fulfilment in production DBMSs. However, there are still challenges that existing isolation checkers have not yet fully addressed. For instance, they may overlook bugs, incur high checking overhead, and return hard-to-understand counterexamples. We present IsoVista, the first black-box isolation checking system that encompasses all the following features. It builds on faithful characterizations of a range of isolation levels, ensuring the absence of both false positives and missed bugs in collected DBMS execution histories. IsoVista exhibits superior checking efficiency, compared to the state-of-the-art, and visualizes violation scenarios, facilitating the understanding of bugs found. It also supports profiling and benchmarking the performance of isolation checkers under various workloads, assisting developers of both DBMSs and checkers. We showcase all these features through user-friendly interfaces.

Snapshot isolation (SI) is a prevalent weak isolation level that avoids the performance penalty imposed by serializability and simultaneously prevents various undesired data anomalies. Nevertheless, SI anomalies have recently been found in production cloud databases that claim to provide the SI guarantee. Given the complex and often unavailable internals of such databases, a black-box SI checker is highly desirable. In this paper we present PolySI, a black-box checker that efficiently checks SI and provides understandable counterexamples upon detecting violations. PolySI builds on a characterization of SI using generalized polygraphs (GPs), for which we establish its soundness and completeness. PolySI employs an SMT solver and also accelerates SMT solving by utilizing a compact constraint encoding of GPs and domain-specific optimizations for pruning constraints. As our extensive assessment demonstrates, PolySI successfully reproduces all of 2477 known SI anomalies, detects novel SI violations in three production cloud databases, identifies their causes, outperforms the state-of-the-art black-box checkers under a wide range of workloads, and can scale up to large workloads.