{"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":1773895293239,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2127309"],"award-info":[{"award-number":["2127309"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n            Clients rely on database systems to be correct, which requires the system not only to implement transactions\u2019 semantics correctly but also to provide isolation guarantees for the transactions. This paper presents a client-centric technique for checking\n            <jats:italic toggle=\"yes\">both<\/jats:italic>\n            semantic correctness and isolation-level guarantees for black-box database systems based on observations collected from running transactions on these systems. Our technique verifies\n            <jats:italic toggle=\"yes\">observational correctness<\/jats:italic>\n            with respect to a given set of transactions and observations for them, which holds iff there exists a possible correct execution of the transactions under a given isolation level that could result in these observations. Our technique relies on novel symbolic encodings of (1) the semantic correctness of database transactions in the presence of weak isolation and (2) isolation-level guarantees. These are used by the checker to query a Satisfiability Modulo Theories solver. We applied our tool Troubadour to verify observational correctness of several database systems, including PostgreSQL and an industrial system under development, in which the tool helped detect two new bugs. We also demonstrate that Troubadour is able to find known semantic correctness bugs and detect isolation-related anomalies.\n          <\/jats:p>","DOI":"10.1145\/3720504","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1661-1688","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Checking Observational Correctness of Database Systems"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1605-5383","authenticated-orcid":false,"given":"Lauren","family":"Pick","sequence":"first","affiliation":[{"name":"The Chinese University of Hong Kong, Hong Kong, Hong Kong"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2279-5816","authenticated-orcid":false,"given":"Amanda","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9006-0100","authenticated-orcid":false,"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Cupertino, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4577-175X","authenticated-orcid":false,"given":"Aws","family":"Albarghouthi","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2011. Big data in real time at Twitter. https:\/\/www.infoq.com\/presentations\/Big-Data-in-Real-Time-at-Twitter"},{"key":"e_1_2_1_2_1","unstructured":"2017. RUBiS. https:\/\/projects.ow2.org\/view\/rubis\/"},{"key":"e_1_2_1_3_1","unstructured":"2022. SQLsmith: a random sql query generator. https:\/\/github.com\/anse1\/sqlsmith Accessed: 2023-11-15."},{"key":"e_1_2_1_4_1","unstructured":"2024. Jepsen. https:\/\/jepsen.io\/ Accessed: 2024-04-05."},{"key":"e_1_2_1_5_1","unstructured":"Atul Adya. 1999. Weak consistency: a generalized theory and optimistic implementations for distributed transactions."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/3430915.3442427"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485546"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3626768"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3560431"},{"key":"e_1_2_1_16_1","unstructured":"Google Cloud. 2024. BigQuery: Multi-statement transactions. https:\/\/cloud.google.com\/bigquery\/docs\/transactions Accessed: 2024-04-02."},{"key":"e_1_2_1_17_1","volume-title":"Transaction Processing: Concepts and Techniques. Morgan Kaufmann.","author":"Gray Jim","year":"1993","unstructured":"Jim Gray and Andreas Reuter. 1993. Transaction Processing: Concepts and Techniques. Morgan Kaufmann."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563292"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649849"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.14778\/3583140.3583145"},{"key":"e_1_2_1_22_1","volume-title":"17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023","author":"Jiang Zu-Ming","year":"2023","unstructured":"Zu-Ming Jiang, Si Liu, Manuel Rigger, and Zhendong Su. 2023. Detecting Transactional Bugs in Database Engines via Graph-Based Oracle Construction. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023, Roxana Geambasu and Ed Nightingale (Eds.). USENIX Association, 397\u2013417. https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/jiang"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859063"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2011.21"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE55515.2023.00061"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_21"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2018.41"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Lauren Pick Amanda Xu Ankush Desai Sanjit Seshia and Aws Albarghouthi. 2024. Checking Observational Correctness of Database Systems Artifact (Troubadour). https:\/\/doi.org\/10.5281\/zenodo.14918621 10.5281\/zenodo.14918621","DOI":"10.5281\/zenodo.14918621"},{"key":"e_1_2_1_29_1","unstructured":"PostgreSQL Global Development Group. 2023. PostgreSQL. http:\/\/www.postgresql.org"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1225053"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428279"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2010.5470389"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563321"},{"key":"e_1_2_1_34_1","volume-title":"Cobra: Making Transactional Key-Value Stores Verifiably Serializable. In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020","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 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4-6, 2020. USENIX Association, 63\u201380. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/tan"},{"key":"e_1_2_1_35_1","unstructured":"Transaction Processing Performance Council. 2010. TPC-C Benchmark Revision 5.11.0. https:\/\/www.tpc.org\/tpcc\/"},{"key":"e_1_2_1_36_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Wang Yuepeng","year":"2018","unstructured":"Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018. Verifying equivalence of database-driven applications. Proc. ACM Program. Lang., 2, POPL (2018), 56:1\u201356:29."},{"key":"e_1_2_1_37_1","unstructured":"ANSI X3.135-1992. November 1992. American National Standard for Information Systems \u2013 Database Language \u2013 SQL."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514221.3517851"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00607-021-00911-3"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3552326.3567492"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1986037"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417260"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720504","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720504","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:15:21Z","timestamp":1760030121000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720504"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":42,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720504"],"URL":"https:\/\/doi.org\/10.1145\/3720504","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}