TY - GEN
T1 - On the Complexity of Checking Mixed Isolation Levels for SQL Transactions
AU - Bouajjani, Ahmed
AU - Enea, Constantin
AU - Román-Calvo, Enrique
N1 - Publisher Copyright:
© The Author(s) 2025.
PY - 2025/1/1
Y1 - 2025/1/1
N2 - Concurrent accesses to databases are typically grouped in transactions which define units of work that should be isolated from other concurrent computations and resilient to failures. Modern databases provide different levels of isolation for transactions that correspond to different trade-offs between consistency and throughput. Quite often, an application can use transactions with different isolation levels at the same time. In this work, we investigate the problem of testing isolation level implementations in databases, i.e., checking whether a given execution composed of multiple transactions adheres to the prescribed isolation level semantics. We particularly focus on transactions formed of SQL queries and the use of multiple isolation levels at the same time. We show that many restrictions of this problem are NP-complete and provide an algorithm which is exponential-time in the worst-case, polynomial-time in relevant cases, and practically efficient.
AB - Concurrent accesses to databases are typically grouped in transactions which define units of work that should be isolated from other concurrent computations and resilient to failures. Modern databases provide different levels of isolation for transactions that correspond to different trade-offs between consistency and throughput. Quite often, an application can use transactions with different isolation levels at the same time. In this work, we investigate the problem of testing isolation level implementations in databases, i.e., checking whether a given execution composed of multiple transactions adheres to the prescribed isolation level semantics. We particularly focus on transactions formed of SQL queries and the use of multiple isolation levels at the same time. We show that many restrictions of this problem are NP-complete and provide an algorithm which is exponential-time in the worst-case, polynomial-time in relevant cases, and practically efficient.
UR - https://www.scopus.com/pages/publications/105017238789
U2 - 10.1007/978-3-031-98685-7_15
DO - 10.1007/978-3-031-98685-7_15
M3 - Conference contribution
AN - SCOPUS:105017238789
SN - 9783031986840
T3 - Lecture Notes in Computer Science
SP - 315
EP - 337
BT - Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings
A2 - Piskac, Ruzica
A2 - Rakamaric, Zvonimir
PB - Springer Science and Business Media Deutschland GmbH
T2 - 37th International Conference on Computer Aided Verification, CAV 2025
Y2 - 23 July 2025 through 25 July 2025
ER -