Online Timestamp-based Transactional Isolation Checking of Database Systems (Extended Version)
Hexu Li, Hengfeng Wei, Hongrong Ouyang, Yuxing Chen, Na Yang, Ruohao Zhang, Anqun Pan
TL;DR
The paper tackles online transactional isolation checking for Serializability and Snapshot Isolation by extending a timestamp-based verification approach. It introduces Chronos, an efficient offline SI checker that runs in timestamp order, and extends it online as AION to support online SI checks, with AION-SER for online SER checks. Chronos achieves $O\left(N\log N + M\right)$ time, processes histories with up to one million transactions rapidly, and uses garbage collection to bound memory. AION delivers sustained throughput around $12{,}000$ transactions per second with minimal database overhead, and AION-SER demonstrates similar performance for online SER checks, significantly outperforming prior online checkers like Cobra. The results demonstrate practical feasibility for continuous, online isolation checking in real-world systems and point to future work extending the approach to more data types and SQL-style queries.
Abstract
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.