Extending Elle for Transaction Workloads with Duplicate Values∗ Zhiheng Cai
Si Liu
Hengfeng Wei
Tsinghua University [email protected]
Texas A&M University [email protected]
Hunan University [email protected]
Abstract
2 in the database. In contrast, most existing isolation validators are built on the traditional read-write register setting, where they must “guess” all possible WW dependencies, a key source of the problem’s computational complexity. Crucially, Elle relies on the unique-value assumption: each value read can be deterministically matched to a single write. Otherwise, in the presence of duplicate values, a read returning a list such as [1,2,1] no longer allows Elle to reliably determine which append of 1 produced each observed value (i.e., the WR dependency), thereby preventing accurate inference of the WW dependency between the two appends. Yet, transaction workloads with duplicate values are highly relevant in practice. Recent findings [13, 15] reveal that many isolation bugs arise only in the presence of duplicate values. Moreover, duplicate-value workloads can naturally occur in real systems, e.g., due to retry mechanisms, and may expose subtle isolation bugs [9]. Thus, checkers relying solely on unique-value workloads may fail to detect these bugs. Due to the randomized nature of black-box testing, rediscovering even a single missed bug may require substantial effort. In this paper, we extend Elle to support database workloads with duplicate values while preserving soundness, completeness, and much of its practical efficiency. One may wonder whether handling duplicate values merely requires reasoning over additional uncertain WR dependencies, as in the recent solution for the read-write register setting [4]. For example, one may attempt possible matchings between the appends of 1 and the corresponding values read in the list, and then check whether any resulting Adya dependency graph is acyclic, which is equivalent to satisfying serializability. Yet, this may yield a spurious serial interpretation of the underlying execution, which in turn may cause genuine bugs to be missed (see Section 3 for details). We address this challenge by introducing a fine-grained dependency model that enables reasoning about dependencies at the operation level rather than the transaction level. Our approach unfolds each returned list into its prefixes, thereby recovering operation-level WR dependencies between append and read operations. These dependencies, in turn, enable precise inference of WW dependencies despite duplicate values. We formally establish the soundness and completeness of our approach. We develop an SMT-based prototype, Elle+ , that uses hyper-polygraphs [4] to encode dependency constraints. Our current implementation focuses on checking serializability.
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.
1
Introduction
Ensuring that database systems uphold their promised isolation guarantees, e.g., serializability, has long been a central concern in both research and practice. Violating these guarantees can lead to undesirable data anomalies, e.g., lost updates, as well as severe security and reliability issues [6, 17]. Black-box validation [3, 4, 7, 9–11, 14, 16, 18, 19] offers an effective practical approach to addressing this concern, as modern database systems often have large codebases that are inaccessible or too difficult to verify directly. In this approach, a validator collects execution histories of database transactions as an external observer and verifies whether these histories satisfy the isolation level in question, i.e., without producing false positives or missing bugs. Elle [9] stands out as one of the most widely adopted blackbox isolation validators. The reasons are mainly twofold. First, although the history verification problem is NP-complete in general [3], Elle achieves near-linear validation time in practice, allowing it to scale to real-world workloads. Second, as part of the Jepsen framework [8], Elle can leverage techniques such as fault injection to stress-test database systems and explore a much broader space of system behaviors. Key to Elle’s effectiveness and efficiency is the co-design of a list-append workload generator and a transactional dependency inference mechanism based on Adya’s theory [1]. For example, a read returning the list [1,2] allows Elle to infer the version order (or the WW dependency) between writes: the append that wrote 1 must precede the append that wrote ∗ This work was accepted by and will be presented at the 1st Symposium on
Consistency Checking Principles (SCCP 2026). 1
Zhiheng Cai, Si Liu, and Hengfeng Wei
Using Elle+ , we successfully reproduced two known serializability bugs in MySQL and MariaDB, both of which can only be triggered in the presence of duplicate values and are thus beyond the scope of Elle. We further show that Elle+ achieves promising performance, suggesting its practical viability.
2
Figure 1b illustrates this idea. As both 𝑇1 and 𝑇2 write to WW(𝑥 )
WR(𝑥 )
WR(𝑥 )
either transaction, we introduce {𝑇1 −−−−−→ 𝑇3,𝑇2 −−−−−→ 𝑇3 }. Under this transaction-level modeling, a history is deemed serializable if one edge can be selected from each choice set such that the resulting dependency graph is acyclic. However, this transaction-level modeling is insufficient.
How Elle Infers Dependencies
Elle [9] considers a distributed key-value store over a set of keys (denoted by 𝑥, 𝑦, 𝑧, . . . ), where each key identifies a list. A list-append history consists of two kinds of operations: an append operation A(𝑥, 𝑣) appending value 𝑣 to the list stored at key 𝑥 and a read operation R(𝑥, ℓ) reading 𝑥 and returning a list ℓ of values. The unique-value assumption requires that, for each key 𝑥, each value 𝑣 is appended at most once. A transaction is a finite set of operations totally ordered by the program order po. A history H is a pair (T , SO), where T is the set of transactions and SO is the session order. A list-append history satisfies serializability iff its transactions can be totally ordered in a way that respects the session order, such that each read operation observes exactly the list produced by all preceding appends to the same key. Elle checks a unique-value list-append history by first constructing an Adya dependency graph [1]. The graph contains three kinds of transaction-level dependencies: WR relates a writer to a reader of its value, WW orders transactions that write the same key, and RW relates a reader of a version to a later writer of that key. The history then satisfies serializability iff SO ∪ WR ∪ WW ∪ RW is acyclic. Figure 1a shows an example unique-value list-append history. Consider the list [1,2,3] read by 𝑇3 . The last value, 3,
WW(𝑥 )
WR(𝑥 )
Figure 1c shows an acyclic resolution 𝑇2 −−−−−−→ 𝑇1 −−−−−→ 𝑇3 . Despite being acyclic, it cannot account for the observed read list [1,2,1]. In particular, the resolution overlooks an append by 𝑇2 that must occur between the append of 2 by 𝑇2 and the append of 1 by 𝑇1 . Consequently, it implies a different evolution of the list than the one actually observed. Even worse, such unfaithful resolutions can mask isolation bugs. Figure 1d shows a non-serializable history, in which both 𝑇1 and 𝑇2 append 1 twice, while 𝑇3 reads [1,1,1]. No serial execution can produce this observation: by atomicity, 𝑇3 can observe either zero, two, or four occurrences of 1, but never three. Yet, this approach admits an acyclic resolution. 3.2 Our Solution: List Unfolding The limitations of the strawman approach point to the need for a faithful characterization of dependencies that: (i) identifies the source append responsible for each successive list extension, rather than only the transaction producing the final value; and (ii) ensures that consecutive values in a list correspond to consecutive appends in the WW order, with no intervening append on the same key. To this end, we shift from transaction-level to operationlevel reasoning. The key idea is to unfold each read list into its successive prefixes, thereby identifying the append responsible for each successive extension of the observed list. Specifically, for each read 𝑟 ≜ R(𝑥, [𝑣 1, 𝑣 2, · · · , 𝑣𝑛 ]), we ′ , where 𝑟 ′ reads introduce 𝑛 auxiliary reads 𝑟 0′ , 𝑟 1′ , · · · , 𝑟𝑛−1 𝑖 the length-𝑖 prefix [𝑣 1, . . . , 𝑣𝑖 ] of the original list (𝑟 0′ reads the empty list, while 𝑟 itself reads the full list). To capture these successive list extensions, we introduce a new order ao, called the append order. For every read and its unfolded
WR(𝑥 )
uniquely identifies the WR dependency 𝑇2 −−−−−→ 𝑇3 , while the relative positions of 1 and 2 imply the WW dependency WW(𝑥 )
𝑇1 −−−−−−→ 𝑇2 . Therefore, in the unique-value setting, the list itself contains sufficient information to recover these dependencies. The resulting dependency graph is acyclic and admits the serial order 𝑇1 → 𝑇2 → 𝑇3 .
3
WW(𝑥 )
key 𝑥, we introduce the choice set {𝑇1 −−−−−−→ 𝑇2,𝑇2 −−−−−−→ 𝑇1 }. Likewise, as the final value read by 𝑇3 may originate from
Extending Elle for Duplicate Values
ao(𝑥 )
reads, we then add the chain of ao(𝑥)-labeled edges: 𝑟 0′ −−−−→
In the presence of duplicate values, Elle can no longer directly recover WR and WW dependencies from read lists. Figure 1b shows an example, where both 𝑇1 and 𝑇2 append value 1 to key 𝑥. As a result, when 𝑇3 reads [1,2,1], the two occurrences of 1 cannot be uniquely mapped to their source appends, and different assignments may induce different WR dependencies. Such uncertainties also extend to WW dependencies, as the same read list may imply different, or even conflicting, orderings of appends.
ao(𝑥 )
ao(𝑥 )
ao(𝑥 )
′ 𝑟 1′ −−−−→ · · · −−−−→ 𝑟𝑛−1 −−−−→ 𝑟 . Figure 2a depicts how our approach handles the duplicatevalue history in Figure 1b. By unfolding the read list of 𝑇3 , uncertain WR dependencies are captured by the following operation-level choice sets:1 wr(𝑥 )
{𝑇⊥ : A(𝑥, empty) −−−−→ R(𝑥, [])}, wr(𝑥 )
wr(𝑥 )
{𝑇1 : A(𝑥, 1) −−−−→ R(𝑥, [1]),𝑇2 : A(𝑥, 1) −−−−→ R(𝑥, [1])}, wr(𝑥 )
3.1
{𝑇2 : A(𝑥, 2) −−−−→ R(𝑥, [1, 2])},
A Strawman Using Transactional Dependencies
wr(𝑥 )
wr(𝑥 )
{𝑇1 : A(𝑥, 1) −−−−→ R(𝑥, [1, 2, 1]),𝑇2 : A(𝑥, 1) −−−−→ R(𝑥, [1, 2, 1])}.
A natural attempt to address this issue is to represent each WR or WW uncertainty as a choice set and ask whether some resolution yields an acyclic dependency graph.
1 Following prior work [3, 4, 7, 11], we additionally introduce a synthetic
initial transaction 𝑇⊥ , which initializes each list to empty. 2
Extending Elle for Transaction Workloads with Duplicate Values T1 A(x, 1)
T2
WW(x)
A(x, 2)
po
T1
A(x, 3)
A(x, 1)
WR(x)
T2
WW(x) WW(x)
A(x, 2)
po
T1 A(x, 1)
A(x, 1)
WR(x)
WR(x)
WW(x)
T2 A(x, 2)
po
T1
A(x, 1)
A(x, 1)
po
A(x, 1)
WW(x)
T2 A(x, 1)
po
A(x, 1)
WR(x)
WR(x)
R(x, [1, 2, 3])
R(x, [1, 2, 1])
R(x, [1, 2, 1])
R(x, [1, 1, 1])
T3
T3
T3
T3
(a) A unique-value list-append history.
(b) A duplicate-value history with constraints.
(c) An unfaithful acyclic resolution.
(d) A false negative caused by transaction-level modeling.
Figure 1. Example histories showing that transaction-level dependency modeling is sufficient for unique-value list-append histories but insufficient when duplicate values are present. T⊥
T1
A(x, empty)
A(x, 1)
wr(x)
T2 A(x, 2)
wr(x)
po
This operation-level dependency model enables us to identify the source append operation responsible for each successive extension of a list. Once the operation-level wr dependencies have been selected, we further constrain the operation-level ww order. Specifically, for every pair of (unfolded) reads 𝑟 and 𝑟 ′
A(x, 1)
wr(x)
wr(x)
R(x, [])
R(x, [1]) R(x, [1, 2]) R(x, [1, 2, 1]) ao(x) ao(x) ao(x) T3 unfolded read operations
ao(𝑥 )
(a) Unfolded reads and operation-level constraints for the history in Figure 1b. The ww constraints are omitted for readability. T⊥ A(x, empty)
ww(x)
wr(x)
T1 A(x, 1)
ww(x)
rw(x) wr(x)
A(x, 2)
such that 𝑟 −−−−→ 𝑟 ′ , if the selected wr dependencies are wr(𝑥 )
wr(𝑥 )
𝑤 −−−−→ 𝑟 and 𝑤 ′ −−−−→ 𝑟 ′ , then the resolution must also
T2 ww(x)
ww(𝑥 )
select 𝑤 −−−−−→ 𝑤 ′ . Furthermore, 𝑤 and 𝑤 ′ must be adjacent in the ww(𝑥) order: there must be no append operation 𝑤 ′′
A(x, 1) po rw(x) wr(x) rw(x) wr(x)
ww(𝑥 )
R(x, [1]) R(x, [1, 2]) R(x, [1, 2, 1]) ao(x) ao(x) ao(x) T3 unfolded read operations
(b) A valid resolution witnessing serializability at the operation level. The so edges from 𝑇⊥ to all other transactions are omitted for readability. T⊥ A(x, empty)
WW(x)
T1 A(x, 1)
WW(x)
T2 A(x, 2)
po
A(x, 1) WR(x)
R(x, [1, 2, 1]) T3
(c) The corresponding transaction-level dependency graph for the valid resolution.
Figure 2. Illustrating list unfolding and the resulting operation- and transaction-level dependency graphs for the duplicate-value history in Figure 1b.
Theorem 3.1. A list-append history satisfies serializability iff there exists a resolution of the operation-level choice sets
Here, 𝑇 : A(_, _) denotes an append operation in transaction 𝑇 , and (lower-case) wr relations denote read-from dependencies between individual operations. Similarly, for WW dependencies, we construct a choice set for each pair of append operations on the same key: ww(𝑥 )
ww(𝑥 )
ww(𝑥 )
ww(𝑥 )
ww(𝑥 )
ww(𝑥 )
ww(𝑥 )
on key 𝑥 such that 𝑤 −−−−−→ 𝑤 ′′ ∧ 𝑤 ′′ −−−−−→ 𝑤 ′ . This condition, which we call the append-order condition, enforces the list semantics that adjacent prefixes of a read list correspond to adjacent append operations. In addition, a valid resolution witnessing serializability must be acyclic at both the operation and transaction levels. First, the selected operation-level dependencies, together with so, ao, and the derived rw edges, must form an acyclic operation graph. This rules out resolutions that assign source appends to read prefixes in a manner inconsistent with the ordering of operations. Second, after lifting the selected dependencies to transactions, the resulting transaction-level dependency graph must also be acyclic. This graph is obtained by collapsing the operation-level dependency graph onto original transactions: auxiliary unfolded reads are ignored, and a transaction-level dependency 𝑇 → 𝑇 ′ is introduced whenever the resolution contains a dependency from an original operation in 𝑇 to an original operation in 𝑇 ′ .
R(x, [])
(i) satisfying the append-order condition; and (ii) yielding acyclic dependency graphs at both the operation and transaction levels.2 Figure 2b shows a valid resolution of the history in Figure 1b. The selected wr edges identify the source append for each successive list extension: the initial append A(𝑥, empty) accounts for [], A(𝑥, 1) in 𝑇1 accounts for [1], A(𝑥, 2) in 𝑇2 accounts for [1,2], and the later append A(𝑥, 1) in 𝑇2 accounts for [1,2,1]. The selected ww edges order these
{𝑇1 : A(𝑥, 1) −−−−−→ 𝑇2 : A(𝑥, 2),𝑇2 : A(𝑥, 2) −−−−−→ 𝑇1 : A(𝑥, 1)}, {𝑇1 : A(𝑥, 1) −−−−−→ 𝑇2 : A(𝑥, 1),𝑇2 : A(𝑥, 1) −−−−−→ 𝑇1 : A(𝑥, 1)}, {𝑇2 : A(𝑥, 2) −−−−−→ 𝑇2 : A(𝑥, 1),𝑇2 : A(𝑥, 1) −−−−−→ 𝑇2 : A(𝑥, 2)}.
We omit the WW choices involving the initial append operation, since it is known to precede all other appends.
2 A proof is provided in Appendix A.
3
Time (s)
Algorithm 1 Verifying duplicate-value list-append histories 1: function Verify(H ) 2: (O, so, po, ao) ← Unfold(H ) 3: (C ww, C wr ) ← ConstructChoices(O) 4: for each resolution (ww, wr) of (C ww, C wr ) 5: rw ← DeriveRW(ww, wr) 6: if CheckAOCond(ww, wr, ao) ∧ 7: 8:
ww(𝑥 )
wr(𝑥 )
WR(𝑥 )
R(𝑥, [1, 2, 1]) induces 𝑇2 −−−−−→ 𝑇3 .
The Algorithm
Algorithm 1 summarizes our procedure Verify for verifying list-append histories with duplicate values. Given a history H , it first invokes Unfold to obtain the operation set O, the operation-level session order so, the program order po, and the append order ao (Line 2). It then constructs the operation-level choice sets C ww and C wr for possible ww and wr dependencies (Line 3). Next, the algorithm enumerates all resolutions (ww, wr) of these choice sets (Line 4). For each resolution, it derives the corresponding operation-level rw edges (Line 5) and checks the two conditions in Theorem 3.1 (Line 6): (i) the selected wr and ww edges satisfy the append-order condition, as checked by CheckAOCond; and (ii) the resulting dependency graphs are acyclic at both the operation and transaction levels, as checked by CheckDepAcyc. If a resolution satisfies both conditions, the history is accepted as serializable (Line 7); otherwise, it is rejected (Line 8). 2 The worst-case complexity of the algorithm is 𝑛𝑂 (𝑛 ) , with 𝑛 the number of operations in H (see Appendix B). Yet, this bound is reached only in the extreme case where all transactions append the same value to the same key. Such workloads are unlikely to arise under the randomized workload generation commonly used in practice (e.g., Jepsen). As we will see next, our tool remains practical even under highly skewed workloads with a high proportion of duplicate values.
5
Elle+ Elle
50 0
0 25 50 75 100 duplicate-key proportion (%)
utilizes hyper-polygraphs [4] to encode both operation-level and transaction-level dependency constraints, which are then solved using an SMT solver [4] optimized for checking strong isolation levels like serializability. We conduct a preliminary evaluation of Elle+ along two dimensions: its effectiveness in detecting isolation bugs and its checking performance. Rediscovering Duplicate-Value Bugs. Using duplicatevalue list-append workloads, Elle+ successfully rediscovers two serializability violations in MySQL (v8.0) and MariaDB (v11.5) that were originally reported through SQL test cases [13, 15]. Both violations require duplicate values to manifest and therefore lie beyond the scope of most existing isolation validators, including Elle. These findings also highlight the potential of duplicate-value list-append workloads to expose subtle isolation bugs in real database systems. Performance Evaluation. To obtain duplicate-value histories, we extend the workload generator of [3], integrate it with Jepsen, and run the generated workloads against a PostgreSQL (v15) instance under serializability. The extended generator allows us to control the fraction of keys receiving duplicate-value appends and uses a Zipfian key-access distribution to emulate high-contention workloads.3 Our experiments run on a local machine equipped with an Intel 13th Gen i5 CPU and 32GB of RAM. Figure 3 (left) shows that the checking time of Elle+ grows steadily with workload size, reaching approximately 50s for histories containing 5K transactions (and 100K operations). Figure 3 (right) shows the runtime as the fraction of keys receiving duplicate-value appends increases. As expected, Elle outperforms Elle+ in the unique-value setting, i.e., when the proportion is zero. The performance gap stems mainly from the need to solve additional constraints introduced at the operation level. Yet, Elle+ manages to verify histories containing 10K transactions and 80K operations in under 100s, even when all 5K keys receive duplicate-value appends.
𝑇⊥ −−−−−−→ 𝑇1 −−−−−−→ 𝑇2 ; the edge 𝑇2 : A(𝑥, 1) −−−−→ 𝑇3 :
4
1k 2k 3k 4k 5k number of transactions
100
Figure 3. Runtime under varying number of transactions (left) and duplicate-key proportions (right).
A(𝑥, empty) −−−−−→ 𝑇1 : A(𝑥, 1) −−−−−→ 𝑇2 : A(𝑥, 2) induces WW(𝑥 )
Elle+ 0
appends as required by the ao edges, and each consecutive pair is adjacent in the ww(𝑥) order. Thus, the resolution explains the observed list at the operation level. Figure 2c shows the corresponding Adya dependency graph, which is also acyclic. This transaction-level graph is obtained by excluding the auxiliary unfolded reads and lifting the dependencies between the remaining operations to their enclosing transactions. For example, the chain 𝑇⊥ : WW(𝑥 )
25 0
CheckDepAcyc(so, po, ao, ww, wr, rw) return true return false
ww(𝑥 )
50
Time (s)
Zhiheng Cai, Si Liu, and Hengfeng Wei
6
Future Work
Building on the promising preliminary results of Elle+ , future work includes (i) leveraging Jepsen’s fault injection for largescale testing of distributed database systems, (ii) exploring additional optimizations to improve the scalability of Elle+ , and (iii) extending it to support other isolation levels [2, 12].
Experiments
We have implemented our algorithm in a prototype checker, called Elle+ , with approximately 3K lines of C++ code. It
3 All parameters and their values are summarized in Appendix C.
4
Extending Elle for Transaction Workloads with Duplicate Values
References
and Aoying Zhou. 2023. Leopard: A Black-Box Approach for Efficiently Verifying Various Isolation Levels. In ICDE 2023. IEEE, 722–735. [11] Si Liu, Long Gu, Hengfeng Wei, and David Basin. 2024. Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels. Proc. ACM Program. Lang. 8, OOPSLA2, Article 302 (Oct. 2024), 29 pages. doi:10.1145/3689742 [12] Si Liu, Luca Multazzu, Hengfeng Wei, and David A. Basin. 2024. NOCNOC: Towards Performance-optimal Distributed Transactions. Proc. ACM Manag. Data 2, 1, Article 9 (March 2024), 25 pages. [13] MariaDB-#26642. Accessed in May, 2026. Weird SELECT view when a record is modified to the same value by two transactions. https: //jira.mariadb.org/browse/MDEV-26642. [14] Lasse Møldrup and Andreas Pavlogiannis. 2025. AWDIT: An Optimal Weak Database Isolation Tester. Proc. ACM Program. Lang. 9, PLDI, Article 209 (June 2025), 25 pages. [15] MySQL-#100328. Accessed in May, 2026. Inconsistent behavior with isolation levels when binlog enabled. https://bugs.mysql.com/bug. php?id=100328. [16] Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. 2020. Cobra: Making Transactional Key-Value Stores Verifiably Serializable. In OSDI 2020. USENIX Association, 63–80. [17] Todd Warszawski and Peter Bailis. 2017. ACIDRain: ConcurrencyRelated Attacks on Database-Backed Web Applications. In SIGMOD 2017. ACM, 5–20. [18] Hengfeng Wei, Jiang Xiao, Na Yang, Si Liu, Zijing Yin, Yuxing Chen, and Anqun Pan. 2025. Boosting End-to-End Database Isolation Checking via Mini-Transactions. In ICDE 2025. IEEE Computer Society, 3998– 4010. [19] Jian Zhang, Ye Ji, Shuai Mu, and Cheng Tan. 2023. Viper: A Fast Snapshot Isolation Checker. In EuroSys 2023. ACM, 654–671.
[1] Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph. D. Dissertation. USA. [2] Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O’Neil, and Patrick O’Neil. 1995. A critique of ANSI SQL isolation levels. ACM SIGMOD Record 24, 2 (1995), 1–10. [3] Ranadeep Biswas and Constantin Enea. 2019. On the Complexity of Checking Transactional Consistency. Proc. ACM Program. Lang. 3, OOPSLA, Article 165 (2019). [4] Zhiheng Cai, Si Liu, Hengfeng Wei, Yuxing Chen, and Anqun Pan. 2025. Fast Verification of Strong Database Isolation. Proc. VLDB Endow. 19, 4 (Dec. 2025), 563–575. [5] Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A Framework for Transactional Consistency Models with Atomic Visibility. In CONCUR 2015 (LIPIcs, Vol. 42). Schloss Dagstuhl - LeibnizZentrum für Informatik, 58–71. [6] Ziyu Cui, Wensheng Dou, Yu Gao, Dong Wang, Jiansen Song, Yingying Zheng, Tao Wang, Rui Yang, Kang Xu, Yixin Hu, Jun Wei, and Tao Huang. 2024. Understanding Transaction Bugs in Database Systems. In ICSE ’24. ACM, Article 163, 13 pages. [7] Kaile Huang, Si Liu, Zhenge Chen, Hengfeng Wei, David A. Basin, Haixiang Li, and Anqun Pan. 2023. Efficient Black-box Checking of Snapshot Isolation in Databases. Proc. VLDB Endow. 16, 6 (2023), 1264–1276. [8] Jepsen. Accessed in June, 2026. https://jepsen.io. [9] Kyle Kingsbury and Peter Alvaro. 2020. Elle: Inferring Isolation Anomalies from Experimental Observations. Proc. VLDB Endow. 14, 3 (2020), 268–280. [10] Keqiang Li, Siyang Weng, Peiyuan Liu, Lyu Ni, Chengcheng Yang, Rong Zhang, Xuan Zhou, Jianghang Lou, Gui Huang, Weining Qian,
5
Zhiheng Cai, Si Liu, and Hengfeng Wei
A
Proof of Theorem 3.1 𝑅
maximal visible append on the same key under gar. The list semantics of IntExt guarantees that this source has the required value, so the selected wr edges are among the alternatives generated by the constraint construction. The rw edges are then derived from the selected ww and wr edges. This resolution satisfies the append-order condition. Indeed, two adjacent unfolded reads correspond to two consecutive prefixes of the same observed list. By IntExt, these prefixes must be produced by consecutive visible append operations on the same key. Therefore, if their selected sources
𝑅
For a total order 𝑅, we write 𝑎 −−−→ 𝑏 if 𝑎 − → 𝑏 and there is imm 𝑅
𝑅
no element 𝑐 such that 𝑎 − →𝑐 − → 𝑏. We use the vis, ar characterization of Serializability [5] in terms of an abstract execution A = (T , SO, vis, ar) satisfying Session, IntExt, and TotalVis. Since TotalVis requires vis = ar, the arbitration order induces a total operation-level order, denoted by gar, by extending ar with program order inside transactions. Similarly, vis induces an operation-level visibility relation gvis. The only list-specific semantic condition used below is the following. For a read operation 𝑟 ≜ R(𝑥, [𝑣 1, . . . , 𝑣𝑛 ]), the visible append operations on key 𝑥 must be exactly 𝑤 0, 𝑤 1, . . . , 𝑤𝑛 in gar order, where 𝑤 0 = A(𝑥, empty) and 𝑤𝑖 = A(𝑥, 𝑣𝑖 ) for every 1 ≤ 𝑖 ≤ 𝑛.
ww(𝑥 )
are 𝑤 and 𝑤 ′ , then 𝑤 −−−−−→ 𝑤 ′ , and there is no append 𝑤 ′′ ww(𝑥 )
rw(𝑥 )
consistent with gar by construction. A derived edge 𝑟 −−−−→
Proof Sketch. We prove Theorem 3.1 in both directions. (“⇐”) Suppose there exists a valid resolution, and let G ′ and GT′ be the resulting operation-level and transaction-level dependency graphs. By validity, both graphs are acyclic. We take ar to be a topological order of GT′ and set vis = ar. Then Session and TotalVis hold immediately, since SO is included in GT′ and vis = ar is total. It remains to check the list semantics required by IntExt. Consider an arbitrary read 𝑟 ≜ R(𝑥, [𝑣 1, . . . , 𝑣𝑛 ]) and its unfolded reads ao(𝑥 )
ao(𝑥 )
ao(𝑥 )
wr(𝑥 )
ao(𝑥 )
Let 𝑤 0, 𝑤 1, . . . , 𝑤𝑛 be the append operations selected by the wr(𝑥) edges for these reads. By construction of wr constraints, these operations append exactly empty, 𝑣 1, . . . , 𝑣𝑛 , respectively. Moreover, the append-order condition ensures ww(𝑥 )
ww(𝑥 )
imm
imm
imm
ww(𝑥 )
𝑤 ′ can only arise from 𝑤 −−−−→ 𝑟 and 𝑤 −−−−−→ 𝑤 ′ . If 𝑤 ′ preceded 𝑟 in gar, then 𝑤 ′ would be visible to 𝑟 , contradicting the maximality of 𝑤 as the visible append source of 𝑟 . Hence rw edges are also consistent with gar, and G1′ is acyclic. The lifted transaction-level graph is acyclic for the same reason, since all lifted edges are consistent with ar. Finally, add the unfolded reads and the ao edges to obtain the full operation-level graph G2′ . Suppose, for contradiction, that G2′ contains a cycle. If the cycle contains no unfolded read, it is already a cycle in G1′ , impossible. It remains to show that the unfolded reads do not introduce new cycles. We prove that any cycle in G2′ would imply a cycle in G1′ : cycles passing through unfolded reads can be eliminated using the append-order condition. Since G1′ is acyclic, G2′ is acyclic as well. Hence the constructed resolution satisfies the appendorder condition and both acyclicity requirements, so it is a valid resolution. This completes the proof sketch. □
′ 𝑟 0′ −−−−→ 𝑟 1′ −−−−→ · · · −−−−→ 𝑟𝑛−1 −−−−→ 𝑟 .
ww(𝑥 )
ww(𝑥 )
such that 𝑤 −−−−−→ 𝑤 ′′ −−−−−→ 𝑤 ′ . It remains to argue acyclicity. First ignore the auxiliary unfolded read operations and consider the graph G1′ over the original operations. The po, so, ww, and wr edges are
𝑤 0 −−−−−→ 𝑤 1 −−−−−→ · · · −−−−−→ 𝑤𝑛 . Thus these append operations explain the successive extensions of the list read by 𝑟 . There cannot be any additional visible append operation on key 𝑥 before 𝑟 . Indeed, because 𝑤 0, . . . , 𝑤𝑛 are adjacent in the ww(𝑥) order, any such extra append 𝑤 ′ would have
B
Complexity Analysis
Let 𝑛 be the number of operations in the input history. The running time of Algorithm 1 is dominated by enumerating possible resolutions of the uncertain ww and wr dependenww(𝑥 ) wr(𝑥 ) to satisfy 𝑤𝑛 −−−−−→ 𝑤 ′ . Together with 𝑤𝑛 −−−−→ 𝑟 , the cies. After read unfolding, there can be 𝑂 (𝑛 2 ) ww choice sets rw(𝑥 ) ′ with two alternatives each, and 𝑂 (𝑛 2 ) wr choice sets with at rw derivation rule gives 𝑟 −−−−→ 𝑤 , forcing 𝑟 to precede ′ most 𝑂 (𝑛) alternatives each. Thus, the number of resolutions 𝑤 in the dependency graph, contradicting the assumption 2 2 that 𝑤 ′ is visible to 𝑟 under the topological order. Hence the is bounded by 2𝑂 (𝑛 ) 𝑛𝑂 (𝑛 ) . For each resolution, the validity visible appends of 𝑟 are exactly 𝑤 0, . . . , 𝑤𝑛 , so IntExt holds. checks, including deriving rw, checking append-order condiTherefore the history satisfies Serializability. tion, and checking acyclicity at both levels, take polynomial (“⇒”) Conversely, suppose the history satisfies Serializtime, say 𝑂 (𝑛 4 ) under a straightforward implementation. ability, witnessed by an abstract execution A = (T , SO, vis, ar). Hence the overall worst-case complexity is 𝑛𝑂 (𝑛2 ) . Yet, this Since TotalVis holds, we have vis = ar. We construct a resupper bound is reached only in the extreme case where all olution from this abstract execution. transactions append the same value to the same key. RealFirst, order append operations on each key according to world workloads are unlikely to exhibit such a worst-case gar and use this order to select the ww edges. For each read pattern, and thus typically induce a much smaller search prefix introduced by unfolding, select as its wr source the space. 6
Extending Elle for Transaction Workloads with Duplicate Values
C
Workload Generator Parameters
In Figure 3 (right), we vary the proportion of keys that allow duplicate append values. Each generated history contains 100 sessions, each with 100 transactions, and each transaction contains 8 operations. The key space again contains 5,000 keys, and the workload consists of 50% reads and 50% appends. Append values are sampled from a Zipfian distribution with skew parameter 𝜃 = 1.5 over a domain of size 𝑁 = 100.
In Figure 3 (left), we vary the total number of transactions. Each generated history contains 20 sessions, and each transaction contains 20 operations. The key space contains 5,000 keys, and the workload consists of 50% reads and 50% appends. Half of the keys allow duplicate append values, while the other half use unique append values. For each key, append values are sampled from a Zipfian distribution with skew parameter 𝜃 = 0.5 over a domain of size 𝑁 = 100.
7