A High-Performance Black-Box Bug-Finding Tool for Database Isolation Levels

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 hard 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 tool Leopard. 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 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; From experimental results, Leopard outperforms existing methods Cobra and Elle. In practice, Leopard has a superpower to verify various ILs on any workload running on all commercial DBMSs. Moreover, it has discovered 49 bugs undetected by other existing methods.