Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
For database system designers, this work provides a formal method to verify correctness of concurrency control protocols under mixed isolation levels, addressing a previously unclear issue.
The paper addresses the problem of verifying whether concurrency control protocols correctly enforce intended isolation guarantees under mixed-isolation settings. It develops a formal semantic framework and demonstrates its applicability by establishing semantic conformance for two protocols combining two and three isolation levels.
Modern database systems widely support per-transaction isolation levels as a practical means of balancing consistency guarantees and performance. Yet, it remains largely unclear whether their concurrency control protocols correctly enforce the intended isolation guarantees under such mixed-isolation settings. In this paper, we address this semantic conformance question by developing \ourframework, a formal semantic framework for mixed isolation levels. We demonstrate its applicability by establishing the semantic conformance of two concurrency control protocols, one combining two isolation levels and the other three.