Extending Elle for Transaction Workloads with Duplicate Values

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.