SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

Enforcing the correctness of isolation levels in modern database management systems (DBMSs) is essential but notoriously challenging. Although formal frameworks like Adya’s model capture concurrency anomalies precisely, they are difficult to apply in practice when DBMS internals remain opaque. Conventional black-box verification tools, while accessible, often fail to observe nuanced read/write dependencies that underlie subtle isolation violations. In this paper, we introduce IsoFuzz, a greybox fuzz-testing framework that bridges these extremes by instrumenting key transactional operations in the DBMS source. By logging version-aware reads, writes, and transaction boundaries, IsoFuzz generates concurrency traces that reflect true internal dependencies without requiring extensive modifications. A guided fuzzer then manipulates interleavings to systematically explore corner-case schedules. Evaluations on MySQL reveal that IsoFuzz reproduces known isolation-level anomalies efficiently and also surfaces previously unseen violations. Our results highlight the promise of combining formal concurrency theory with targeted instrumentation to achieve more comprehensive DBMS isolation-level verification.