Boosting End-to-End Database Isolation Checking via Mini-Transactions (Extended Version)
Hengfeng Wei, Jiang Xiao, Na Yang, Si Liu, Zijing Yin, Yuxing Chen, Anqun Pan
TL;DR
This work tackles the inefficiencies of black-box isolation checking in databases by introducing Mini-Transactions (MTs), compact read/write patterns that enable faster history generation and verification for strong isolation levels such as SSER, SER, and SI. By leveraging the read-modify-write structure and unique write values, MT histories admit highly efficient, linear- or quadratic-time verification algorithms, and MTs capture the 14 well-known isolation anomalies with at most four operations per transaction. The authors implement these algorithms and a MT workload generator in MTC, achieving substantial performance gains over state-of-the-art checkers in end-to-end testing and in detecting real-world bugs across production DBMSs. The approach reduces overhead, preserves bug-detection effectiveness, and offers a cost-efficient path for black-box isolation checking, with practical implications for deploying robust database systems. Overall, MTC demonstrates that MT-based testing can maintain strong coverage while dramatically improving efficiency in both history generation and verification.
Abstract
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.