Verifying Serializability Protocols With Version Order Recovery
Clark, Jack · Repository for Publications and Research Data (ETH Zurich) · 2021
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 sequentially.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.One method of providing assurance of the correctness of concurrency control protocols purporting to offer serializability is by verifying that the execution histories they produce are serializable.However, existing verifiers either have no guarantees on their worst-case execution time or require constraints on the type of operations they support, for example no verifier currently supports verifying histories containing predicate operations except in very special cases.We introduce the concept of version order recovery, which recovers the version order from database systems while imposing fewer constraints than existing verifiers, that provides the means for efficient verification of serializable concurrency control protocols.We implement version order recovery for both PostgreSQL and TiDB, and show that it has minimal overhead on execution performance.We also implement a serializability verifier Emme and show that its performance is competitive with or better than existing verifiers.Additionally, when object visibility information can be recovered on a per-operation basis, we show that Emme supports the verification of moderate size histories containing predicate operations.Due to the significant improvements in efficiency, broader testing applicability, and moderate implementation effort, we expect version order recovery to be widely adopted in practice.i