A core feature of many database systems is the ability to group operations into transactions. An isolation level defines the extent to which operations within a transaction interact with operations from other concurrent transactions. The serializable isolation level provides correctness guarantees that many programmers implicitly assume, since it provides the illusion of transactions running in some sequential order. However, implementing serializable transactions, particularly in a distributed setting, has proven to be a challenging task, with many systems failing to live up to their guarantees.

Unfortunately, verifying that an execution history is serializable is NP-complete. However, with access to a database system’s internal version order, serializability can be efficiently checked. Existing tools for checking the serializability of histories either have exponential running time or require specially crafted operations to be able to recover version order information, which significantly limits the amount of functionality that can be tested. Furthermore, existing tools cannot handle predicate operations which are a key feature of most database systems.

This talk demonstrates that it is possible to recover the version order directly from real database systems and that it can be used to efficiently verify execution histories. Additionally, we show that recovering additional object visibility information enables verification of histories that contain predicate operations, a condition which distinguishes the serializable isolation level from weaker levels. Building on these foundations, we discuss how we can move towards verifying histories generated by real-world workloads, something not achievable with existing tools and techniques.

Please email for a Zoom link

Jack Clark joined the Multicore Programming Group at Imperial College London as a Research Associate in October 2021. He obtained a master’s degree in computer science from ETH Zurich that included a thesis proposing a novel method of verifying concurrency control protocol executions in database systems. His interests include database systems, the automatic testing and verification of distributed systems, and fuzz testing of wider software systems.