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.

Cloud computing is on the rise, which promotes new breeds of database systems to accommodate the cloud environment. The development of cloud-native databases reveals three trends. One is the adoption of multi-datacenter (DC) deployment to survive the downtime of any single site. Another is the separation of computation and storage resources to achieve higher elasticity and scalability. The last is the support of HTAP to eliminate data redundancy and system complexity from heterogeneous databases. To cater to these trends, we design a distributed relational database called PolarDB-X, which is built on top of the cloud-native database PolarDB. It hence inherits many cloud-native features, such as multi-datacenter deployment and elasticity. To achieve cross-DC capability, it leverages Paxos and hybrid logical clock to achieve durability and snapshot-isolation consistency with low coordination costs. For resource elasticity, since the underlying PolarDB supports rapid migration of tenants between nodes, PolarDB-X can quickly scale the cluster to cope with a sudden traffic increase. For HTAP support, with the help of read replicas and a HTAP executor, PolarDB-X can improve the latency and parallelism of analytical queries without impacting concurrently-running TP workloads. Using its MPP engine and an in-memory column index, the efficiency of analytical queries can be further enhanced. PolarDB-X is now a cloud database service at Alibaba Cloud. We have learned many useful lessons from its development and operation, and have incorporated those into our design and analysis.