Validating Database Execution: Revisiting Concurrency Correctness in Modern Systems
Host
Samuel Madden
CSAIL
Abstract:
Database correctness is crucial, but checking it remains a significant challenge. Modern transactional databases---leveraging distributed architectures, outsourced components, geo-replication, and advanced optimizations---further complicate this validation process. In this talk, we present our efforts to tackle this problem, resulting in several key advancements. These include the development of systems for validating serializability and snapshot isolation of black-box databases, a simpler snapshot isolation definition, a specialized SMT solver, and a unified framework---both theoretical and implemented---for validating concurrent systems.
More broadly, databases represent just one example within a wide range of modern concurrent systems, including serverless platforms, deep learning training frameworks, and cloud infrastructure. We believe that now is the right time to revisit the classic problem of checking concurrency correctness for this new generation of systems.
Bio:
Cheng Tan is an assistant professor at Khoury College of Computer Sciences at Northeastern University. His research interests are in computer systems, verifiable systems, and neural networks for systems. He is a recipient of the SOSP’17 Best Paper Award, ASPLOS'23 Distinguished Artifact Award, MSRA StarTrack Scholar, and NSF CAREER Award.
Database correctness is crucial, but checking it remains a significant challenge. Modern transactional databases---leveraging distributed architectures, outsourced components, geo-replication, and advanced optimizations---further complicate this validation process. In this talk, we present our efforts to tackle this problem, resulting in several key advancements. These include the development of systems for validating serializability and snapshot isolation of black-box databases, a simpler snapshot isolation definition, a specialized SMT solver, and a unified framework---both theoretical and implemented---for validating concurrent systems.
More broadly, databases represent just one example within a wide range of modern concurrent systems, including serverless platforms, deep learning training frameworks, and cloud infrastructure. We believe that now is the right time to revisit the classic problem of checking concurrency correctness for this new generation of systems.
Bio:
Cheng Tan is an assistant professor at Khoury College of Computer Sciences at Northeastern University. His research interests are in computer systems, verifiable systems, and neural networks for systems. He is a recipient of the SOSP’17 Best Paper Award, ASPLOS'23 Distinguished Artifact Award, MSRA StarTrack Scholar, and NSF CAREER Award.