Extending Elle for Transaction Workloads with Duplicate Values
2026-07-20 • Databases
Databases
AI summaryⓘ
The authors looked at Elle, a tool that checks if database transactions run without problems under certain assumptions. They noticed Elle struggles when transactions have repeated values, which happens often in real databases and can cause hidden bugs. To fix this, they improved Elle by creating a detailed way to track how individual operations depend on each other. They proved their method works correctly, built a prototype, and showed it can find isolation bugs effectively while performing well.
database transactionsisolation validationblack-box testingdependency modelunique-value assumptionisolation bugstransaction workloadssoundnesscompletenessprototype implementation
Authors
Zhiheng Cai, Si Liu, Hengfeng Wei
Abstract
Elle is one of the most widely adopted black-box isolation validators. It crucially relies on the unique-value assumption for sound and efficient isolation validation. Yet, transaction workloads with duplicate values are highly relevant in practice: they naturally arise in real database systems, and many isolation bugs manifest only in their presence. In this paper, we extend Elle to handle such workloads by introducing a fine-grained dependency model that enables reasoning about dependencies between individual operations. We establish the soundness and completeness of our approach and implement it in a prototype. We also demonstrate its effectiveness in detecting isolation bugs and its promising performance.