Isolation Levels (IL) act as correct contracts between applications and database management systems (DBMSs). The complex code logic and concurrent interactions among transactions make it a hard problem to expose violations of various ILs stated by DBMSs. With the recent proliferation of new DBMSs, especially the cloud ones, there is an urgent demand for a general way to detect bugs violating various ILs. The core challenges come from the requirements of: (a) lightweight (verifying without modifying the application logic in workloads and the source code of DBMSs), (b) generality (verifying various ILs), and (c) efficiency (performing efficient verification on a long running workload). To this end, we propose a powerful and practical bug-finding toolLeopard. For lightweight, we propose to infer transaction dependencies based on the time intervals of operations collected from the client-side, without modifying the source code of DBMSs. For generality, based on a thorough analysis of existing concurrency control protocols, we summarize and abstract four mechanisms which can implement ILs in all commercial DBMSs we have investigated. For efficiency, we design atwo-level pipelineto organize and sort massive time intervals in a time and memory conservative way; we propose amechanism-mirrored verificationto simulate the concurrency control protocols implemented in DBMSs for high throughputs; From experimental results,Leopardoutperforms existing methodsCobraandElle. In practice,Leopardhas a superpower to verify various ILs on any workload running on all commercial DBMSs. Moreover, it has successfully discovered 49 bugs that cannot be found by other existing methods.

Isolation level (IL) acts as a correctness contract between applications and DBMSs. Problematic IL implementations would cause incorrect transaction execution results and erroneous database states. However, existing studies could not efficiently generate various effective workloads for IL test. The core challenges come from the requirements of (a) black-box testing (trigger the IL code of a closed source DBMS), (b) effective testing (evade redundant and ineffective testing), and (c) anomaly-sensitive testing (test various ILs in a distinguishable way). For black-box testing, we investigate the IL implementations of 15 popular DBMSs and discover that they follow a generic framework that utilizes conflict graphs to manage all conflicts of a workload, and performs a verification policy to prevent non-serializable anomalies. For effective testing, we propose a lightweight data state mirroring method, which helps generate SQL operations that precisely access its expected records and participate the formation of specific conflict graphs. We also propose an efficient history-independent approach to generate dissimilar conflict graphs. It guarantees the graph generation overhead is irrelevant to the scale of historical graphs. For anomaly-sensitive testing, we propose an implantation-based approach to orchestrate conflict record accesses and inject them into different transactions according to the anomaly definition. Our approach outperforms existing approaches in testing effectiveness, efficiency, and coverage. Practically, we have successfully found 33 bugs in popular DBMSs.

Isolation Levels (IL) act as correct contracts between applications and database management systems (DBMSs). The complex code logic and concurrent interactions among transactions make it a hard problem to expose violations of various ILs stated by DBMSs. With the recent proliferation of new DBMSs, especially the cloud ones, there is an urgent demand for a general way to verify various ILs. The core challenges come from the requirements of: (a) lightweight (verifying without modifying the application logic in workloads and the source code of DBMSs), (b) generality (verifying various ILs), and (c) efficiency (performing efficient verification on a long running workload). For lightweight, we propose to deduce transaction dependencies based on time intervals of operations collected from client-sides without touching the source code of DBMSs. For generality, based on a thorough analysis of existing concurrency control protocols, we summarize and abstract four mechanisms which can implement ILs in all commercial DBMSs we have investigated. For efficiency, we design a two-level pipeline to organize and sort massive time intervals in a time and memory conservative way; we propose a mechanism-mirrored verification to simulate the concurrency control protocols implemented in DBMSs for high throughputs. Leopard outperforms existing methods by up to 114× in verification time with a relative small memory usage. In practice, Leopard has a superpower to verify various ILs on any workload running on all commercial DBMSs. Moreover, it has successfully discovered 23 bugs that cannot be found by other existing methods.