{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T04:41:33Z","timestamp":1773895293793,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"6","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2023,2]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.14778\/3583140.3583145","type":"journal-article","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T16:45:59Z","timestamp":1682009159000},"page":"1264-1276","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Efficient Black-Box Checking of Snapshot Isolation in Databases"],"prefix":"10.14778","volume":"16","author":[{"given":"Kaile","family":"Huang","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Si","family":"Liu","sequence":"additional","affiliation":[{"name":"ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenge","family":"Chen","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hengfeng","family":"Wei","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haixiang","family":"Li","sequence":"additional","affiliation":[{"name":"Tencent Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anqun","family":"Pan","sequence":"additional","affiliation":[{"name":"Tencent Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. USA.  Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. USA."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732232.2732237"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI'15)","author":"Bayless Sam","unstructured":"Sam Bayless , Noah Bayless , Holger H. Hoos , and Alan J. Hu . 2015. SAT modulo Monotonic Theories . In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI'15) . AAAI Press, 3702--3709. Sam Bayless, Noah Bayless, Holger H. Hoos, and Alan J. Hu. 2015. SAT modulo Monotonic Theories. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI'15). AAAI Press, 3702--3709."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/223784.223785"},{"key":"e_1_2_1_5_1","volume-title":"Concurrency Control and Recovery in Database Systems","author":"Bernstein Philip A","unstructured":"Philip A Bernstein , Vassos Hadzilacos , and Nathan Goodman . 1986. Concurrency Control and Recovery in Database Systems . Addison-Wesley Longman Publishing Co., Inc. , USA. Philip A Bernstein, Vassos Hadzilacos, and Nathan Goodman. 1986. Concurrency Control and Recovery in Database Systems. Addison-Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485546"},{"key":"e_1_2_1_8_1","volume-title":"POPL'17","author":"Bouajjani Ahmed","year":"2017","unstructured":"Ahmed Bouajjani , Constantin Enea , Rachid Guerraoui , and Jad Hamza . 2017 . On verifying causal consistency . In POPL'17 . ACM, 626--638. Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017. On verifying causal consistency. In POPL'17. ACM, 626--638."},{"key":"e_1_2_1_9_1","volume-title":"CONCUR'15 (LIPIcs)","volume":"42","author":"Cerone Andrea","year":"2015","unstructured":"Andrea Cerone , Giovanni Bernardi , and Alexey Gotsman . 2015 . A Framework for Transactional Consistency Models with Atomic Visibility . In CONCUR'15 (LIPIcs) , Vol. 42 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 58--71. Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A Framework for Transactional Consistency Models with Atomic Visibility. In CONCUR'15 (LIPIcs), Vol. 42. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 58--71."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152396"},{"key":"e_1_2_1_11_1","volume-title":"All about Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","author":"Clavel Manuel","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , and Carolyn Talcott . 2007. All about Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic . Springer-Verlag , Berlin, Heidelberg . Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn Talcott. 2007. All about Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_2_1_12_1","unstructured":"MariaDB Galera Cluster. Accessed February 14 2023. https:\/\/mariadb.com\/kb\/en\/what-is-mariadb-galera-cluster\/.  MariaDB Galera Cluster. Accessed February 14 2023. https:\/\/mariadb.com\/kb\/en\/what-is-mariadb-galera-cluster\/."},{"key":"e_1_2_1_13_1","unstructured":"CockroachDB. Accessed February 14 2023. https:\/\/www.cockroachlabs.com\/.  CockroachDB. Accessed February 14 2023. https:\/\/www.cockroachlabs.com\/."},{"key":"e_1_2_1_14_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . 2009. Introduction to Algorithms , Third Edition (3 rd ed.). The MIT Press . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, Third Edition (3rd ed.). The MIT Press.","edition":"3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_2_1_16_1","unstructured":"Ben Darnell. Accessed February 14 2023. Lessons Learned from 2+ Years of Nightly Jepsen Tests. https:\/\/www.cockroachlabs.com\/blog\/jepsen-tests-lessons\/.  Ben Darnell. Accessed February 14 2023. Lessons Learned from 2+ Years of Nightly Jepsen Tests. https:\/\/www.cockroachlabs.com\/blog\/jepsen-tests-lessons\/."},{"key":"e_1_2_1_17_1","unstructured":"Oracle Database. Accessed February 14 2023. https:\/\/www.oracle.com\/database\/.  Oracle Database. Accessed February 14 2023. https:\/\/www.oracle.com\/database\/."},{"key":"e_1_2_1_18_1","volume-title":"Lazy Database Replication with Snapshot Isolation. In VLDB'06","author":"Daudjee Khuzaima","year":"2006","unstructured":"Khuzaima Daudjee and Kenneth Salem . 2006 . Lazy Database Replication with Snapshot Isolation. In VLDB'06 . VLDB Endowment, 715--726. Khuzaima Daudjee and Kenneth Salem. 2006. Lazy Database Replication with Snapshot Isolation. In VLDB'06. VLDB Endowment, 715--726."},{"key":"e_1_2_1_19_1","unstructured":"Dgraph. Accessed February 14 2023. https:\/\/dgraph.io\/.  Dgraph. Accessed February 14 2023. https:\/\/dgraph.io\/."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407860"},{"key":"e_1_2_1_21_1","unstructured":"Graphviz. Accessed February 14 2023. Open source graph visualization software. https:\/\/graphviz.org\/.  Graphviz. Accessed February 14 2023. Open source graph visualization software. https:\/\/graphviz.org\/."},{"key":"e_1_2_1_23_1","unstructured":"Kaile Huang Si Liu Zhenge Chen Hengfeng Wei David Basin Haixiang Li and Anqun Pan. Accessed February 14 2023. Issue #17. https:\/\/github.com\/jepsen-io\/elle\/issues\/17.  Kaile Huang Si Liu Zhenge Chen Hengfeng Wei David Basin Haixiang Li and Anqun Pan. Accessed February 14 2023. Issue #17. https:\/\/github.com\/jepsen-io\/elle\/issues\/17."},{"key":"e_1_2_1_24_1","unstructured":"Jepsen. Accessed February 14 2023. https:\/\/jepsen.io.  Jepsen. Accessed February 14 2023. https:\/\/jepsen.io."},{"key":"e_1_2_1_25_1","unstructured":"Jepsen. Accessed February 14 2023. Issue #824. https:\/\/github.com\/YugaByte\/yugabyte-db\/issues\/824.  Jepsen. Accessed February 14 2023. Issue #824. https:\/\/github.com\/YugaByte\/yugabyte-db\/issues\/824."},{"key":"e_1_2_1_26_1","unstructured":"Nick Kallen. Accessed February 14 2023. Big Data in Real Time at Twitter. https:\/\/www.infoq.com\/presentations\/Big-Data-in-Real-Time-at-Twitter\/.  Nick Kallen. Accessed February 14 2023. Big Data in Real Time at Twitter. https:\/\/www.infoq.com\/presentations\/Big-Data-in-Real-Time-at-Twitter\/."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_2_1_28_1","volume-title":"Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In TACAS 2019 (LNCS)","volume":"11428","author":"Liu Si","year":"2019","unstructured":"Si Liu , Peter Csaba \u00d6lveczky , Min Zhang , Qi Wang , and Jos\u00e9 Meseguer . 2019 . Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In TACAS 2019 (LNCS) , Vol. 11428 . Springer, 40--57. Si Liu, Peter Csaba \u00d6lveczky, Min Zhang, Qi Wang, and Jos\u00e9 Meseguer. 2019. Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In TACAS 2019 (LNCS), Vol. 11428. Springer, 40--57."},{"key":"e_1_2_1_29_1","volume-title":"Andersen","author":"Lloyd Wyatt","year":"2013","unstructured":"Wyatt Lloyd , Michael J. Freedman , Michael Kaminsky , and David G . Andersen . 2013 . Stronger semantics for low-latency geo-replicated storage. In NSDI' 13. USENIX Association , 313--328. Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2013. Stronger semantics for low-latency geo-replicated storage. In NSDI' 13. USENIX Association, 313--328."},{"key":"e_1_2_1_30_1","volume-title":"Performance-Optimal Read-Only Transactions. In OSDI","author":"Lu Haonan","year":"2020","unstructured":"Haonan Lu , Siddhartha Sen , and Wyatt Lloyd . 2020 . Performance-Optimal Read-Only Transactions. In OSDI 2020. USENIX Association, 333--349. Haonan Lu, Siddhartha Sen, and Wyatt Lloyd. 2020. Performance-Optimal Read-Only Transactions. In OSDI 2020. USENIX Association, 333--349."},{"key":"e_1_2_1_31_1","unstructured":"MongoDB. Accessed February 14 2023. https:\/\/www.mongodb.com\/.  MongoDB. Accessed February 14 2023. https:\/\/www.mongodb.com\/."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_33_1","volume-title":"Large-Scale Incremental Processing Using Distributed Transactions and Notifications. In OSDI'10","author":"Peng Daniel","year":"2010","unstructured":"Daniel Peng and Frank Dabek . 2010 . Large-Scale Incremental Processing Using Distributed Transactions and Notifications. In OSDI'10 . USENIX Association, USA, 251--264. Daniel Peng and Frank Dabek. 2010. Large-Scale Incremental Processing Using Distributed Transactions and Notifications. In OSDI'10. USENIX Association, USA, 251--264."},{"key":"e_1_2_1_34_1","unstructured":"PostgreSQL. Accessed February 14 2023. Transaction Isolation. https:\/\/www.postgresql.org\/docs\/current\/transaction-iso.html.  PostgreSQL. Accessed February 14 2023. Transaction Isolation. https:\/\/www.postgresql.org\/docs\/current\/transaction-iso.html."},{"key":"e_1_2_1_35_1","unstructured":"RUBiS. Accessed February 14 2023. Auction Site for e-Commerce Technologies Benchmarking. https:\/\/projects.ow2.org\/view\/rubis\/.  RUBiS. Accessed February 14 2023. Auction Site for e-Commerce Technologies Benchmarking. https:\/\/projects.ow2.org\/view\/rubis\/."},{"key":"e_1_2_1_36_1","unstructured":"Microsoft SQL Server. Accessed February 14 2023. https:\/\/www.microsoft.com\/en-us\/sql-server\/.  Microsoft SQL Server. Accessed February 14 2023. https:\/\/www.microsoft.com\/en-us\/sql-server\/."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_2_1_38_1","volume-title":"COBRA: Making Transactional Key-Value Stores Verifiably Serializable. In OSDI'20","author":"Tan Cheng","year":"2020","unstructured":"Cheng Tan , Changgeng Zhao , Shuai Mu , and Michael Walfish . 2020 . COBRA: Making Transactional Key-Value Stores Verifiably Serializable. In OSDI'20 . Article 4, 18 pages. Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. 2020. COBRA: Making Transactional Key-Value Stores Verifiably Serializable. In OSDI'20. Article 4, 18 pages."},{"key":"e_1_2_1_39_1","volume-title":"Welch","author":"Terry Douglas B.","year":"1994","unstructured":"Douglas B. Terry , Alan J. Demers , Karin Petersen , Mike Spreitzer , Marvin Theimer , and Brent B . Welch . 1994 . Session Guarantees for Weakly Consistent Replicated Data. In PDIS. IEEE Computer Society , 140--149. Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent B. Welch. 1994. Session Guarantees for Weakly Consistent Replicated Data. In PDIS. IEEE Computer Society, 140--149."},{"key":"e_1_2_1_40_1","unstructured":"Jepsen testing of MongoDB 4.2.6. Accessed February 14 2023. http:\/\/jepsen.io\/analyses\/mongodb-4.2.6.  Jepsen testing of MongoDB 4.2.6. Accessed February 14 2023. http:\/\/jepsen.io\/analyses\/mongodb-4.2.6."},{"key":"e_1_2_1_41_1","unstructured":"Jepsen testing of TiDB 2.1.7. Accessed February 14 2023. https:\/\/jepsen.io\/analyses\/tidb-2.1.7.  Jepsen testing of TiDB 2.1.7. Accessed February 14 2023. https:\/\/jepsen.io\/analyses\/tidb-2.1.7."},{"key":"e_1_2_1_42_1","unstructured":"TiDB. Accessed February 14 2023. https:\/\/en.pingcap.com\/tidb\/.  TiDB. Accessed February 14 2023. https:\/\/en.pingcap.com\/tidb\/."},{"key":"e_1_2_1_43_1","unstructured":"TPC. Accessed February 14 2023. TPC-C: On-Line Transaction Processing Benchmark. https:\/\/www.tpc.org\/tpcc\/.  TPC. Accessed February 14 2023. TPC-C: On-Line Transaction Processing Benchmark. https:\/\/www.tpc.org\/tpcc\/."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3064037"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.21"},{"key":"e_1_2_1_46_1","unstructured":"YugabyteDB. Accessed February 14 2023. https:\/\/www.yugabyte.com\/.  YugabyteDB. Accessed February 14 2023. https:\/\/www.yugabyte.com\/."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-013-0318-x"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31277-0_3"}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3583140.3583145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T16:59:56Z","timestamp":1682009996000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3583140.3583145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2]]},"references-count":47,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["10.14778\/3583140.3583145"],"URL":"https:\/\/doi.org\/10.14778\/3583140.3583145","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2023,2]]},"assertion":[{"value":"2023-04-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}