{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:07Z","timestamp":1767928507167,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986840","type":"print"},{"value":"9783031986857","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.\n<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_15","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:31:35Z","timestamp":1753155095000},"page":"315-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the\u00a0Complexity of\u00a0Checking Mixed Isolation Levels for\u00a0SQL Transactions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2060-3592","authenticated-orcid":false,"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7539-2330","authenticated-orcid":false,"given":"Enrique","family":"Rom\u00e1n-Calvo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2(OOPSLA), 135:1\u2013135:29 (2018). https:\/\/doi.org\/10.1145\/3276505","DOI":"10.1145\/3276505"},{"key":"15_CR2","volume-title":"Weak consistency: A generalized theory and optimistic implementations for distributed transactions","author":"A Adya","year":"1999","unstructured":"Adya, A.: Weak consistency: A generalized theory and optimistic implementations for distributed transactions. Technical report, USA (1999)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-030-81685-8_16","volume-title":"Computer Aided Verification","author":"P Agarwal","year":"2021","unstructured":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., Toman, V.: Stateless model checking under a reads-value-from equivalence. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021, Part I. LNCS, vol. 12759, pp. 341\u2013366. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Alvaro, P., Kingsbury, K.: Elle: inferring isolation anomalies from experimental observations. Proc. VLDB Endow. 14(3), 268\u2013280 (2020). http:\/\/www.vldb.org\/pvldb\/vol14\/p268-alvaro.pdf. https:\/\/doi.org\/10.5555\/3430915.3442427","DOI":"10.5555\/3430915.3442427"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Rom\u00e1n-Calvo, E.: Artifact for \u201cOn the complexity of checking mixed isolation levels for SQL transactions\u201d (2024). https:\/\/github.com\/Galieve\/benchbase-histories","DOI":"10.1007\/978-3-031-98685-7_15"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Berenson, H., Bernstein, P.A., Gray, J., Melton, J., O\u2019Neil, E.J., O\u2019Neil, P.E.: A critique of ANSI SQL isolation levels. In: Carey, M.J., Schneider, D.A. (eds.) Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, San Jose, California, USA, 22\u201325 May 1995, pp. 1\u201310. ACM Press (1995). https:\/\/doi.org\/10.1145\/223784.223785","DOI":"10.1145\/223784.223785"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Biswas, R., Enea, C.: On the complexity of checking transactional consistency. Proc. ACM Program. Lang. 3(OOPSLA), 165:1\u2013165:28 (2019). https:\/\/doi.org\/10.1145\/3360591","DOI":"10.1145\/3360591"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Biswas, R., Kakwani, D., Vedurada, J., Enea, C., Lal, A.: MonkeyDB: effectively testing correctness under weak isolation levels. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201327 (2021). https:\/\/doi.org\/10.1145\/3485546","DOI":"10.1145\/3485546"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 626\u2013638. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009888","DOI":"10.1145\/3009837.3009888"},{"issue":"7","key":"15_CR10","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1109\/TPDS.2005.86","volume":"16","author":"JF Cantin","year":"2005","unstructured":"Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence and consistency. IEEE Trans. Parallel Distributed Syst. 16(7), 663\u2013671 (2005). https:\/\/doi.org\/10.1109\/TPDS.2005.86","journal-title":"IEEE Trans. Parallel Distributed Syst."},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Cerone, A., Bernardi, G., Gotsman, A.: A framework for transactional consistency models with atomic visibility. In: Aceto, L., de\u00a0Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, 1\u20134 September 2015, vol.\u00a042 of LIPIcs, pp. 58\u201371. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.58. https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2015.58","DOI":"10.4230\/LIPICS.CONCUR.2015.58"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Difallah, D.E., Pavlo, A., Curino, C., Cudr\u00e9-Mauroux, P.: OLTP-bench: an extensible testbed for benchmarking relational databases. Proc. VLDB Endow. 7(4), 277\u2013288 (2013). http:\/\/www.vldb.org\/pvldb\/vol7\/p277-difallah.pdf. https:\/\/doi.org\/10.14778\/2732240.2732246","DOI":"10.14778\/2732240.2732246"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Emmi, M., Enea, C.: Sound, complete, and tractable linearizability monitoring for concurrent collections. Proc. ACM Program. Lang. 2(POPL), 25:1\u201325:27 (2018). https:\/\/doi.org\/10.1145\/3158113","DOI":"10.1145\/3158113"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Furbach, F., Meyer, R., Schneider, K., Senftleben, M.: Memory-model-aware testing: a unified complexity analysis. ACM Trans. Embed. Comput. Syst. 14(4), 63:1\u201363:25 (2015). https:\/\/doi.org\/10.1145\/2753761","DOI":"10.1145\/2753761"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Gibbons, P.B., Korach, E.: On testing cache-coherent shared memories. In: Snyder, L., Leiserson, C.E. (eds.) Proceedings of the 6th Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1994, Cape May, New Jersey, USA, 27\u201329 June 1994, pp. 177\u2013188. ACM (1994). https:\/\/doi.org\/10.1145\/181014.181328","DOI":"10.1145\/181014.181328"},{"issue":"4","key":"15_CR16","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997). https:\/\/doi.org\/10.1137\/S0097539794279614","journal-title":"SIAM J. Comput."},{"issue":"4","key":"15_CR17","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1142\/S0129626403001628","volume":"13","author":"A Gontmakher","year":"2003","unstructured":"Gontmakher, A., Polyakov, S.V., Schuster, A.: Complexity of verifying java shared memory execution. Parallel Process. Lett. 13(4), 721\u2013733 (2003). https:\/\/doi.org\/10.1142\/S0129626403001628","journal-title":"Parallel Process. Lett."},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Huang, K., et al.: Efficient black-box checking of snapshot isolation in databases. Proc. VLDB Endow. 16(6), 1264\u20131276 (2023). https:\/\/www.vldb.org\/pvldb\/vol16\/p1264-wei.pdf. https:\/\/doi.org\/10.14778\/3583140.3583145","DOI":"10.14778\/3583140.3583145"},{"key":"15_CR19","unstructured":"Jepsen: Distributed systems testing (2020). https:\/\/jepsen.io\/"},{"issue":"OOPSLA2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"876","DOI":"10.1145\/3689742","volume":"8","author":"S Liu","year":"2024","unstructured":"Liu, S., Long, G., Wei, H., Basin, D.A.: Plume: efficient and complete black-box checking of weak isolation levels. Proc. ACM Program. Lang. 8(OOPSLA2), 876\u2013904 (2024). https:\/\/doi.org\/10.1145\/3689742","journal-title":"Proc. ACM Program. Lang."},{"issue":"4","key":"15_CR21","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979). https:\/\/doi.org\/10.1145\/322154.322158","journal-title":"J. ACM"},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Pavlo, A.: What are we doing with our lives?: Nobody cares about our concurrency control research. In: Salihoglu, S., Zhou, W., Chirkova, R., Yang, J., Suciu, D. (eds.) Proceedings of the 2017 ACM International Conference on Management of Data, SIGMOD Conference 2017, Chicago, IL, USA, 14\u201319 May 2017, p.\u00a03. ACM (2017). https:\/\/doi.org\/10.1145\/3035918.3056096","DOI":"10.1145\/3035918.3056096"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Terry, D.B., Demers, A.J., Petersen, K., Spreitzer, M., Theimer, M., Welch, B.B.: Session guarantees for weakly consistent replicated data. In: Proceedings of the Third International Conference on Parallel and Distributed Information Systems (PDIS 1994), Austin, Texas, USA, 28\u201330 September 1994, pp. 140\u2013149. IEEE Computer Society (1994). https:\/\/doi.org\/10.1109\/PDIS.1994.331722","DOI":"10.1109\/PDIS.1994.331722"},{"key":"15_CR24","unstructured":"TPC: Technical report, Transaction Processing Performance Council, February 2010. http:\/\/www.tpc.org\/tpc_documents_current_versions\/pdf\/tpc-c_v5.11.0.pdf"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:54:45Z","timestamp":1760086485000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}