PolySI & Tesseract: New Black‑Box Tools for Snapshot Isolation & Schema Evolution

Just now, the Tencent Cloud database team received a big surprise!

At the recently concluded 49th VLDB conference, a joint paper by Tencent Cloud, Nanjing University, ETH Zurich, and Simon Fraser University was accepted, highlighting innovative technologies recognized by this top‑tier database venue.

About VLDB

VLDB, one of the three premier conferences in the database field, showcases cutting‑edge research and industrial applications each year, attracting leading tech companies and research institutions worldwide. With strict criteria for system innovation, completeness, and experimental design, its acceptance rate is around 18%.

Novel Black‑Box Checker for Snapshot Isolation

Snapshot isolation (SI) is a widely used weak isolation level that avoids the performance loss of serializability while preventing many common data anomalies. However, some production cloud databases claiming SI guarantees still exhibit SI anomalies, especially in financial applications, causing significant impact. Existing tools either do not support SI testing or are inefficient.

To address this, the collaborative solution "Efficient Black‑box Checking of Snapshot Isolation in Databases" introduces PolySI, a novel black‑box checker that efficiently verifies SI and provides understandable counterexamples when violations are detected.

PolySI is based on the Generalized Polygraphs (GPs) SI characterization theorem, guaranteeing correctness and completeness. It leverages the MonoSAT SMT solver, compact GPs constraint encoding, and domain‑specific optimizations to accelerate solving.

Extensive evaluation shows PolySI reproduces known SI anomalies, discovers new SI bugs in three production cloud databases, and outperforms state‑of‑the‑art SI black‑box checkers across diverse workloads, scaling to large workloads.

Online and Transactional Schema Evolution (Tesseract)

Modern database applications often need to evolve their schema without downtime. Online schema changes allow structural modifications without stopping the service or interrupting ongoing transactions, enabling continuous operation while adapting to dynamic requirements.

Challenges include maintaining data consistency during modifications, handling long‑running schema changes that can affect performance, and avoiding the need for scheduled downtime.

The paper "Online Schema Evolution is (Almost) Free for Snapshot Databases" presents Tesseract, a novel method that models schema evolution as Data‑Definition‑as‑Modification (DDaM) in multi‑version databases, allowing near‑free online, transactional schema changes by exploiting concurrency control protocols.

In tests on a 40‑core server, Tesseract provides online, transactional schema evolution without service interruption while maintaining high application performance.

Through participation in VLDB, Tencent Cloud shares these breakthroughs with the global developer community, offering valuable references for the advancement of database technology and industry.

Paper links:

https://www.vldb.org/pvldb/vol16/p1264-wei.pdf

https://www.vldb.org/pvldb/vol16/p140-hu.pdf