Checking Observational Correctness of Database Systems

Lauren Pick, Amanda Xu, Ankush Desai, S. Seshia, Aws Albarghouthi. 2025. Proc. ACM Program. Lang..

Read the paper · doi:10.1145/3720504

What this paper does with SQLancer

SQLancer supplies the evaluation's yardstick: Troubadour is shown to verify that a trace exhibits none of the classes of bug SQLancer detects for the SQL fragment it supports, and was run on the queries and incorrect responses SQLancer had observed, reporting errors for all of them. The paper is careful that testing tools like SQLancer detect bugs but cannot verify observational correctness. This paper checks database systems as a client would, verifying both transaction semantics and isolation guarantees from observations of running transactions against a black-box system. Observational correctness holds if some correct execution under the given isolation level could have produced the observations. The technique rests on symbolic encodings discharged with an SMT solver. The tool, Troubadour, was applied to PostgreSQL and an industrial system under development, finding two new bugs. Written by claude-opus-5 from the 6 places this paper refers to SQLancer. The quotations below are the paper's own words, stored verbatim when the text was extracted.

How it was classified

uses infrastructure — no

SQLancer is cited, not used; nothing in the mentions describes reusing its code.

extends technique — no

No technique is extended; the citation is background.

compares with — yes

M1 and M2 report running Troubadour on the bug classes and on the actual incorrect responses SQLancer found, and comparing what each detects. That is an empirical comparison of coverage of bug classes rather than a bug-count race, but it is a comparison.

Troubadour can verify that a trace does not demonstrate any of the classes of bugs detected by DBMS fuzzer SQLancer for the fragment of SQL that Troubadour supports as well as detect the presence of such bugs. M1 · 8.2 RQ2: Classes of Bugs Considered · page 20

We also ran the tool on the query and the original incorrect response observed by SQLancer, and Troubadour reported errors for all the examples in under a second total as well, demonstrating its ability to detect semantic bugs. M2 · 8.2 RQ2: Classes of Bugs Considered · page 20

describes as state of the art — no

The citation does not characterise SQLancer as the state of the art.

SQLancer publications it cites (2)

Bibliography entries that resolved to a SQLancer publication, or to a paper by one of the project's authors. A sentence citing one of these numbers is a reference to SQLancer even when it never writes the name.

#	Entry	Matched as
22	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 Implementatio...	project authored
31	Manuel Rigger and Zhendong Su. 2020. Finding bugs in database systems via query partitioning. Proc. ACM Program. Lang. 4, OOPSLA (2020), 211:1–211:30. https://doi.org/10.1145/3428279	sqlancer publication · TLP

Every place it refers to SQLancer (6)

6 sentences, each stored verbatim from the extracted text with where it was found and how. “Citation marker” means the sentence names no tool at all and was reached through a reference number that resolved to a SQLancer publication.

Id	Sentence	Found by	Where
M1	Troubadour can verify that a trace does not demonstrate any of the classes of bugs detected by DBMS fuzzer SQLancer for the fragment of SQL that Troubadour supports as well as detect the presence of such bugs.	name result comparison	8.2 RQ2: Classes of Bugs Considered page 20
M2	We also ran the tool on the query and the original incorrect response observed by SQLancer, and Troubadour reported errors for all the examples in under a second total as well, demonstrating its ability to detect semantic bugs.	name result comparison	8.2 RQ2: Classes of Bugs Considered page 20
M3	Testing tools like SQLancer and TxCheck can detect certain semantic bugs but clearly cannot perform verification of observational correctness [ 22, 31].	name background	8.2 RQ2: Classes of Bugs Considered page 20
M4	There has been much work on DBMS fuzzing for SQL using a variety of techniques [ 3,15,31,42], such as ternary logic partitioning and mutation-based fuzzing.	technique definition	8.5 Industrial Case Study page 24
M5	The TxCheck fuzzer employs some limited reasoning about isolation levels [ 22].	citation marker project authored background	8.5 Industrial Case Study page 24
M6	While these values may be gotten by instrumenting transactions [ 22], instrumentation implicitly relies on the semantic correctness of the DBMS and may not be possible for certain DBMSs [16].	citation marker project authored background	8.5 Industrial Case Study page 25

This page is rendered from _data/papers/paper_doi_10_1145_3720504.json, extracted from supplied pdf. 28 pages, 42 references parsed.