arXiv subjects

Sho Nakazono

Publications and source records attributed to Sho Nakazono.

4 recordsLinked to original sources

arXiv2026

CV-Rules: Serializability Verification of Concurrency Control Protocols via Explicit Transaction Ordering

We present CV-rules, an alternative characterization of serializability in which a transaction order constructed by a protocol satisfies two per-read conditions, C-rule (Causality) and V-rule (View Consistency), that constrain the reads-from relation and competing writers. While classical Multi-Version Serialization Graph (MVSG) reasoning characterizes serializability via its acyclicity, our approach requires explicit order construction, enabling direct proofs that build on the protocol's own mechanisms. We prove that CV-rules, serializability, and MVSG acyclicity are all equivalent. Moreover, the C/V separation reveals that serializability is polynomial-time decidable for any fixed bound on the width of the order forced by C-rule. We verify five protocols: Two-Phase Locking, Multi-Version Timestamp Ordering, Serial Safety Net (SSN), Aria, and SnapChain. For SSN and Aria, whose original papers defined only certification conditions, we identify explicit transaction orders arising from their mechanisms; we also prove that Aria's unique-write constraint is unnecessary for serializability. SnapChain, in contrast, is designed directly from CV-rules, enforcing V-rule by construction. All results except the complexity bounds are mechanized in Lean with no additional axioms and no admitted goals.

cs.LO↗

arXiv2024

Griffin: Fast Transactional Database Index with Hash and B+-Tree

Index access is one of the dominant performance factors in transactional database systems. Many systems use a B+-tree or one of its variants to handle point and range operations. This access pattern has room for performance improvement. Firstly, point operations can potentially be processed in $O(1)$ with a hash table. Secondly, to ensure serializability of transactions, range operations incur overhead from phantom avoidance techniques that involve additional processing or synchronization, such as an extra traversal of the B+-tree. To address these issues, we propose a hybrid index architecture, Griffin. For point operations, Griffin has a hash table that provides access paths in $O(1)$ time, along with a B+-tree. For phantom avoidance, Griffin employs a precision locking method, which does not involve additional traversal of the B+-tree. Despite its hybrid architecture, Griffin transparently provides linearizable operations and an interface of a single database index. We built a Griffin index combining a hash table and BwTree. Compared to a baseline index that is composed of a BwTree only, it achieves up to 3.1x higher throughput in a point operation dominant workload, and up to 5.4x higher throughput in a range operation dominant workload.

cs.DB↗

arXiv2023

Scheduling Space Expander: An Extension of Concurrency Control for Data Ingestion Queries

With the continuing advances of sensing devices and IoT/Telecom applications, database systems need to process data ingestion queries that update the sensor data frequently. However, as the rate of data ingestion queries increases, existing protocols have exhibited degraded performance since concurrent updates need to acquire lock to update the latest versions. To reduce the load on system on data ingestion queries, we focus on the theory of version order; we can test that a write is an old and unnecessary version by using version order of data items. In this paper, we propose a novel protocol extension method, scheduling space expander (SSE). SSE adds another control flow to conventional protocols to omit updates on data ingestion queries. It generates an erasing version order, which assumes that a transaction processes outdated unnecessary versions. SSE also tests the correctness of this version order efficiently and independently from conventional protocols. In addition, we present an optimization of SSE called epoch-based SSE (ESSE), which tests and maintains an erasing version order more efficiently than SSE. We extend two state-of-the-art 1VCC and MVCC protocols, Silo and MVTO with ESSE. Experimental results demonstrate that extensions of Silo and MVTO improve 2.7x and 2.5x performance on the TATP benchmark on a 144-core machine, and the extensions achieved performance comparable to that of the original protocol for the TPC-C benchmark.

cs.DB↗

arXiv2020

NWR: Rethinking Thomas Write Rule for Omittable Write Operations

Concurrency control protocols are the key to scaling current DBMS performances. They efficiently interleave read and write operations in transactions, but occasionally they restrict concurrency by using coordination such as exclusive lockings. Although exclusive lockings ensure the correctness of DBMS, it incurs serious performance penalties on multi-core environments. In particular, existing protocols generally suffer from emerging highly write contended workloads, since they use innumerable lockings for write operations. In this paper, we rethink the Thomas write rule (TWR), which allows the timestamp ordering (T/O) protocol to omit write operations without any lockings. We formalize the notion of omitting and decouple it from the T/O protocol implementation, in order to define a new rule named non-visible write rule (NWR). When the rules of NWR are satisfied, any protocol can in theory generate omittable write operations with preserving the correctness without any lockings. In the experiments, we implement three NWR-extended protocols: Silo+NWR, TicToc+NWR, and MVTO+NWR. Experimental results demonstrate the efficiency and the low-overhead property of the extended protocols. We confirm that NWR-extended protocols achieve more than 11x faster than the originals in the best case of highly write contended YCSB-A and comparable performance with the originals in the other workloads.

cs.DB↗