Search for a command to run...
Transactions are a key feature of database systems and isolation levels specify the behavior of concurrently executing transactions. Ensuring the correctness of isolation levels is crucial. Recently, many isolation anomalies have been found in production database systems. Checkers can be used to validate that a particular execution history conforms to a desired isolation level. However, state-of-the-art checkers cannot handle predicate operations, which are both common in real-world workloads and essential for distinguishing between the repeatable read and serializable isolation levels. In this work, we address this issue by proposing two techniques for efficient white-box checking. Our key idea is to use information that is easily provided by database systems to efficiently check the isolation level of a given execution history. We present the version certificate recovery technique and its associated checker Emme . Version certificate recovery is a method of recovering the version order and each operation’s version set from the database system under test. To minimise execution time, we also propose the expected serialization order technique, along with its associated checker Enne , which obviates the need to define and recover a version certificate for many serializable concurrency control protocols. We have implemented version certificate recovery for three widely used database systems—PostgreSQL, CockroachDB, and TiDB. We demonstrate that Emme is 1.2–3.6 × faster than Elle, a state-of-the-art checker. When paired with the expected serialization order technique, Enne obtains a further speedup of 34–430 × when checking execution histories containing predicate operations. We show that our approaches can identify invalid execution histories that cannot be detected by Elle and also show that they can find realistic bugs purposely introduced by an engineer. Finally, we create a new checker, King Cobra , by modifying Cobra, an existing black-box checker, in order to conduct an ablation study to evaluate how the performance of a black-box checker changes when provided with varying degrees of ordering information. By doing so, we highlight the fundamental role that ordering information plays in the execution time of an isolation level checker and explore the limits that this places on a truly black-box checker.