arXiv subjects

Hengfeng Wei

Publications and source records attributed to Hengfeng Wei.

At least 19 recordsLinked to original sources

arXiv2026

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.

cs.DB↗

arXiv2026

Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels

Modern database systems widely support per-transaction isolation levels as a practical means of balancing consistency guarantees and performance. Yet, it remains largely unclear whether their concurrency control protocols correctly enforce the intended isolation guarantees under such mixed-isolation settings. In this paper, we address this semantic conformance question by developing \ourframework, a formal semantic framework for mixed isolation levels. We demonstrate its applicability by establishing the semantic conformance of two concurrency control protocols, one combining two isolation levels and the other three.

cs.DB↗

arXiv2026

InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs

Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop programs, but they often struggle with programs containing multiple interacting loops. This paper presents InvWeaver, a neuro-symbolic framework for synthesizing invariants for such programs. The key idea is to expose inter-loop dependencies and propagate proof obligations through a combination of loop-level abstraction, obligation-guided inference, and weakest-precondition-based refinement. We evaluate InvWeaver on a comprehensive benchmark suite, including a newly curated dataset derived from classic algorithms. Experimental results show that InvWeaver substantially outperforms existing invariant inference methods, solving 72 out of 82 multi-loop benchmark problems and maintaining strong performance on single-loop tasks.

cs.LG↗

arXiv2026

Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models

Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved by every protocol transition; yet inferring such invariants remains a major bottleneck: existing approaches either restrict the protocol models to a decidable fragment of first-order logic or demand expert-crafted templates. We present IC3Syn, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states with the assistance of Large Language Models (LLMs). At large, IC3Syn combines a symbolic IC3 controller, which decomposes invariant synthesis into focused blocking tasks and an LLM which provides protocol-level reasoning that IC3 alone lacks for TLA+ specifications. This integration enables a disciplined yet flexible search for invariants without imposing logical restrictions or requiring manual templates. We evaluate IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client-server systems, and compare it against Endive, IC3PO, SWISS and DistAI. IC3Syn discovers candidate invariants for all 29 protocols, including MongoLoglessDynamicRaft (MLDR), an industrial-scale Raft-based reconfiguration protocol for which none of the compared tools reports a solution, as well as one complex Paxos variant. In each case, the invariants synthesized on finite instances are shown in TLAPS to be inductive for the full unbounded protocol, thereby establishing safety.

cs.SE↗

arXiv2025

Fast Verification of Strong Database Isolation (Extended Version)

Strong isolation guarantees, such as serializability and snapshot isolation, are essential for maintaining data consistency and integrity in modern databases. Verifying whether a database upholds its claimed guarantees is increasingly critical, as these guarantees form a contract between the vendor and its users. However, this task is challenging, particularly in black-box settings, where only observable system behavior is available and often involves uncertain dependencies between transactions. In this paper, we present VeriStrong, a fast verifier for strong database isolation. At its core is a novel formalism called hyper-polygraphs, which compactly captures both certain and uncertain transactional dependencies in database executions. Leveraging this formalism, we develop sound and complete encodings for verifying both serializability and snapshot isolation. To achieve high efficiency, VeriStrong tailors SMT solving to the characteristics of database workloads, in contrast to prior general-purpose approaches. Our extensive evaluation across diverse benchmarks shows that VeriStrong not only significantly outperforms state-of-the-art verifiers on the workloads they support, but also scales to large, general workloads beyond their reach, while maintaining high accuracy in detecting isolation anomalies.

cs.DB↗

arXiv2025

Boosting End-to-End Database Isolation Checking via Mini-Transactions (Extended Version)

Transactional isolation guarantees are crucial for database correctness. However, recent studies have uncovered numerous isolation bugs in production databases. The common black-box approach to isolation checking stresses databases with large, concurrent, randomized transaction workloads and verifies whether the resulting execution histories satisfy specified isolation levels. For strong isolation levels such as strict serializability, serializability, and snapshot isolation, this approach often incurs significant end-to-end checking overhead during both history generation and verification. We address these inefficiencies through the novel design of Mini-Transactions (MTs). MTs are compact, short transactions that execute much faster than general workloads, reducing overhead during history generation by minimizing database blocking and transaction retries. By leveraging MTs' read-modify-write pattern, we develop highly efficient algorithms to verify strong isolation levels in linear or quadratic time. Despite their simplicity, MTs are semantically rich and effectively capture common isolation anomalies described in the literature. We implement our verification algorithms and an MT workload generator in a tool called MTC. Experimental results show that MTC outperforms state-of-the-art tools in both history generation and verification. Moreover, MTC can detect bugs across various isolation levels in production databases while maintaining the effectiveness of randomized testing with general workloads, making it a cost-effective solution for black-box isolation checking.

cs.DB↗

arXiv2025

Online Timestamp-based Transactional Isolation Checking of Database Systems (Extended Version)

Serializability (SER) and snapshot isolation (SI) are widely used transactional isolation levels in database systems. The isolation checking problem asks whether a given execution history of a database system satisfies a specified isolation level. However, existing SER and SI checkers, whether traditional black-box checkers or recent timestamp-based white-box ones, operate offline and require the entire history to be available to construct a dependency graph, making them unsuitable for continuous and ever-growing histories. This paper addresses online isolation checking by extending the timestamp-based isolation checking approach to online settings. Specifically, we design CHRONOS, an efficient timestamp-based offline SI checker. CHRONOS is incremental and avoids constructing a start-ordered serialization graph for the entire history, making it well-suited for online scenarios. We further extend CHRONOS into an online SI checker, AION, addressing several key challenges unique to online settings. Additionally, we develop AION-SER for online SER checking. Experiments highlight that CHRONOS processes offline histories with up to one million transactions in seconds, greatly outperforming existing SI checkers. Furthermore, AION and AION-SER sustain a throughput of approximately 12K transactions per second, demonstrating their practicality for online isolation checking.

cs.DB↗

arXiv2023

Efficient Black-box Checking of Snapshot Isolation in Databases

Snapshot isolation (SI) is a prevalent weak isolation level that avoids the performance penalty imposed by serializability and simultaneously prevents various undesired data anomalies. Nevertheless, SI anomalies have recently been found in production cloud databases that claim to provide the SI guarantee. Given the complex and often unavailable internals of such databases, a black-box SI checker is highly desirable. In this paper we present PolySI, a novel black-box checker that efficiently checks SI and provides understandable counterexamples upon detecting violations. PolySI builds on a novel characterization of SI using generalized polygraphs (GPs), for which we establish its soundness and completeness. PolySI employs an SMT solver and also accelerates SMT solving by utilizing the compact constraint encoding of GPs and domain-specific optimizations for pruning constraints. As demonstrated by our extensive assessment, PolySI successfully reproduces all of 2477 known SI anomalies, detects novel SI violations in three production cloud databases, identifies their causes, outperforms the state-of-the-art black-box checkers under a wide range of workloads, and can scale up to large-sized workloads.

cs.DB↗

arXiv2022

Tunable Causal Consistency: Specification and Implementation

To achieve high availability and low latency, distributed data stores often geographically replicate data at multiple sites called replicas. However, this introduces the data consistency problem. Due to the fundamental tradeoffs among consistency, availability, and latency in the presence of network partition, no a one-size-fits-all consistency model exists. To meet the needs of different applications, many popular data stores provide tunable consistency, allowing clients to specify the consistency level per individual operation. In this paper, we propose tunable causal consistency (TCC). It allows clients to choose the desired session guarantee for each operation, from the well-known four session guarantees, i.e., read your writes, monotonic reads, monotonic writes, and writes follow reads. Specifically, we first propose a formal specification of TCC in an extended (vis,ar) framework originally proposed by Burckhardt et al. Then we design a TCC protocol and develop a prototype distributed key-value store called TCCSTORE. We evaluate TCCSTORE on Aliyun. The latency is less than 38ms for all workloads and the throughput is up to about 2800 operations per second. We also show that TCC achieves better performance than causal consistency and requires a negligible overhead when compared with eventual consistency.

cs.DC↗

arXiv2022

ViSearch: Weak Consistency Measurement for Replicated Data Types

Large-scale replicated data type stores often resort to eventual consistency to guarantee low latency and high availability. It is widely accepted that programming over eventually consistent data stores is challenging, since arbitrary divergence among replicas is allowed. Moreover, pragmatic protocols actually achieve consistency guarantees stronger than eventual consistency, which can be and need to be utilized to facilitate the reasoning of and programming over replicated data types. Toward the challenges above, we propose the ViSearch framework for precise measurement of eventual consistency semantics. ViSearch employs the visibility-arbitration specification methodology in concurrent programming, which extends the linearizability-based specification methodology with a dynamic visibility relation among operations, in addition to the standard dynamic happen-before and linearization relations. The consistency measurement using ViSearch is NP-hard in general. To enable practical and efficient consistency measurement in replicated data type stores, the ViSearch framework refactors the existing brute-force checking algorithm to a generic algorithm skeleton, which further enables efficient pruning of the search space and effective parallelization. We employ the ViSearch framework for consistency measurement in two replicated data type stores Riak and CRDT-Redis. The experimental evaluation shows the usefulness and cost-effectiveness of consistency measurement based on the ViSearch framework in realistic scenarios.

cs.DC↗

arXiv2022

Remove-Win: a Design Framework for Conflict-free Replicated Data Types

Distributed storage systems employ replication to improve performance and reliability. To provide low latency data access, replicas are often required to accept updates without coordination with each other, and the updates are then propagated asynchronously. This brings the critical challenge of conflict resolution among concurrent updates. Conflict-free Replicated Data Type (CRDT) is a principled approach to addressing this challenge. However, existing CRDT designs are tricky, and hard to be generalized to other data types. A design framework is in great need to guide the systematic design of new CRDTs. To address this challenge, we propose RWF -- the Remove-Win design Framework for CRDTs. RWF leverages the simple but powerful remove-win strategy to resolve conflicting updates, and provides generic design for a variety of data container types. Two exemplar implementations following RWF are given over the Redis data type store, which demonstrate the effectiveness of RWF. Performance measurements of our implementations further show the efficiency of CRDT designs following RWF.

cs.DC↗

arXiv2022

Verifying Transactional Consistency of MongoDB

MongoDB is a popular general-purpose, document-oriented, distributed NoSQL database. It supports transactions in three different deployments: single-document transactions utilizing the WiredTiger storage engine in a standalone node, multi-document transactions in a replica set which consists of a primary node and several secondary nodes, and distributed transactions in a sharded cluster which is a group of multiple replica sets, among which data is sharded. A natural and fundamental question about MongoDB transactions is: What transactional consistency guarantee do MongoDB Transactions in each deployment provide? However, it lacks both concise pseudocode of MongoDB transactions in each deployment and formal specification of the consistency guarantees which MongoDB claimed to provide. In this work, we formally specify and verify the transactional consistency protocols of MongoDB. Specifically, we provide a concise pseudocode for the transactional consistency protocols in each MongoDB deployment, namely WIREDTIGER, REPLICASET, and SHARDEDCLUSTER, based on the official documents and source code. We then prove that WIREDTIGER, REPLICASET, and SHARDEDCLUSTER satisfy different variants of snapshot isolation, namely Strong-SI, Realtime-SI, and Session-SI, respectively. We also propose and evaluate efficient white-box checking algorithms for MongoDB transaction protocols against their consistency guarantees, effectively circumventing the NP-hard obstacle in theory.

cs.DC↗

arXiv2022

MET: Model Checking-Driven Explorative Testing of CRDT Designs and Implementations

Internet-scale distributed systems often replicate data at multiple geographic locations to provide low latency and high availability. The Conflict-free Replicated Data Type (CRDT) is a framework that provides a principled approach to maintaining eventual consistency among data replicas. CRDTs have been notoriously difficult to design and implement correctly. Subtle deep bugs lie in the complex and tedious handling of all possible cases of conflicting data updates. We argue that the CRDT design should be formally specified and model-checked to uncover deep bugs. The implementation further needs to be systematically tested. On the one hand, the testing needs to inherit the exhaustive nature of the model checking and ensures the coverage of testing. On the other hand, the testing is expected to find coding errors which cannot be detected by design level verification. Towards the challenges above, we propose the Model Checking-driven Explorative Testing (MET) framework. At the design level, MET uses TLA+ to specify and model check CRDT designs. At the implementation level, MET conducts model checking-driven explorative testing, in the sense that the test cases are automatically generated from the model checking traces. The system execution is controlled to proceed deterministically, following the model checking trace. The explorative testing systematically controls and permutes all nondeterministic message reorderings. We apply MET in our practical development of CRDTs. The bugs in both designs and implementations of CRDTs are found. As for bugs which can be found by traditional testing techniques, MET greatly reduces the cost of fixing the bugs. Moreover, MET can find subtle deep bugs which cannot be found by existing techniques at a reasonable cost. We further discuss how MET provides us with sufficient confidence in the correctness of our CRDT designs and implementations.

cs.DC↗

arXiv2021

Byz-GentleRain: An Efficient Byzantine-tolerant Causal Consistency Protocol

Causal consistency is a widely used weak consistency model that allows high availability despite network partitions. There are plenty of research prototypes and industrial deployments of causally consistent distributed systems. However, as far as we know, none of them consider Byzantine faults, except Byz-RCM proposed by Tseng et al. Byz-RCM achieves causal consistency in the client-server model with $3f + 1$ servers where up to $f$ servers may suffer Byzantine faults, but assumes that clients are non-Byzantine. In this work, we present Byz-Gentlerain, the first causal consistency protocol which tolerates up to $f$ Byzantine servers among $3f + 1$ servers in each partition and any number of Byzantine clients. Byz-GentleRain is inspired by the stabilization mechanism of GentleRain for causal consistency. To prevent causal violations due to Byzantine faults, Byz-GentleRain relies on PBFT to reach agreement on a sequence of global stable times and updates among servers, and only updates with timestamps less than or equal to such common global stable times are visible to clients. We prove that Byz-GentleRain achieves Byz-CC, the causal consistency variant in the presence of Byzantine faults. We evaluate Byz-GentleRain on Aliyun. The preliminary results show that Byz-GentleRain is efficient on typical workloads.

cs.DC↗

arXiv2021

UniStore: A fault-tolerant marriage of causal and strong consistency (extended version)

Modern online services rely on data stores that replicate their data across geographically distributed data centers. Providing strong consistency in such data stores results in high latencies and makes the system vulnerable to network partitions. The alternative of relaxing consistency violates crucial correctness properties. A compromise is to allow multiple consistency levels to coexist in the data store. In this paper we present UniStore, the first fault-tolerant and scalable data store that combines causal and strong consistency. The key challenge we address in UniStore is to maintain liveness despite data center failures: this could be compromised if a strong transaction takes a dependency on a causal transaction that is later lost because of a failure. UniStore ensures that such situations do not arise while paying the cost of durability for causal transactions only when necessary. We evaluate UniStore on Amazon EC2 using both microbenchmarks and a sample application. Our results show that UniStore effectively and scalably combines causal and strong consistency.

cs.DC↗

arXiv2020

Fine-grained Analysis on Fast Implementations of Distributed Multi-writer Atomic Registers

Distributed multi-writer atomic registers are at the heart of a large number of distributed algorithms. While enjoying the benefits of atomicity, researchers further explore fast implementations of atomic reigsters which are optimal in terms of data access latency. Though it is proved that multi-writer atomic register implementations are impossible when both read and write are required to be fast, it is still open whether implementations are impossible when only write or read is required to be fast. This work proves the impossibility of fast write implementations based on a series of chain arguments among indistiguishable executions. We also show the necessary and sufficient condition for fast read implementations by extending the results in the single-writer case. This work concludes a series of studies on fast implementations of distributed atomic registers.

cs.DC↗

arXiv2019

Inversion-based Measurement of Data Consistency for Read/Write Registers

Both providers and consumers of distributed storage services benefit from the quantification of the severity of consistency violations. However, existing methods fail to capture a typical pattern of violation - the disorder among operations with reference to the ideally strong atomic execution. Such disorder are often seen in Internet applications based on distributed storage services, such as instant messaging. To this end, we use inversions in a permutation with reference to the totally-ordered permutation to measure the consistency of data. The $i$-atomicity model is proposed and a (pseudo-)polynomial verification algorithm for a restricted type of histories is proposed. The basic idea of the verification algorithm is brute-force search of the permutation with less than $i$ inversions, which requires exponential cost. Reasonable assumptions abstracted from applications scenarios can be leveraged to prune the search space, which yields an efficient polynomial verification algorithm.

cs.DC↗

arXiv2018

Specification and Implementation of Replicated List: The Jupiter Protocol Revisited

The replicated list object is frequently used to model the core functionality of replicated collaborative text editing systems. Since 1989, the convergence property has been a common specification of a replicated list object. Recently, Attiya et al. proposed the strong/weak list specification and conjectured that the well-known Jupiter protocol satisfies the weak list specification. The major obstacle to proving this conjecture is the mismatch between the global property on all replica states prescribed by the specification and the local view each replica maintains in Jupiter using data structures like 1D buffer or 2D state space. To address this issue, we propose CJupiter (Compact Jupiter) based on a novel data structure called $n$-ary ordered state space for a replicated client/server system with $n$ clients. At a high level, CJupiter maintains only a single $n$-ary ordered state space which encompasses exactly all states of each replica. We prove that CJupiter and Jupiter are equivalent and that CJupiter satisfies the weak list specification, thus solving the conjecture above.

cs.DC↗