@techreport{oai:ipsj.ixsq.nii.ac.jp:00234365,
 author = {Tung, Nguyen and Hideyuki, Kawashima and Tung, Nguyen and Hideyuki, Kawashima},
 issue = {10},
 month = {May},
 note = {Wound-wait, a preemptive deadlock prevention scheme, has been widely used in locking-based concurrency control protocols among transaction processing systems. This scheme provides a commit priority order based on the timestamp of each transaction, which is commonly generated using a single centralized atomic counter. Due to the inefficiency of this timestamp generation mechanism, recent researches attempted to decentralize this mechanism to accelerate performance. While the new decentralized approaches make transaction processing highly performant, the inherent liveness property is often overlooked. Identifying such property violations is notoriously difficult in concurrent systems such as databases. This paper formally specifies a decentralized wound-wait scheme in TLA+ and verifies it using explicit-state model checker TLC. A vital liveness property violation has been detected and we were also able to offer a fundamental solution to this violation., Wound-wait, a preemptive deadlock prevention scheme, has been widely used in locking-based concurrency control protocols among transaction processing systems. This scheme provides a commit priority order based on the timestamp of each transaction, which is commonly generated using a single centralized atomic counter. Due to the inefficiency of this timestamp generation mechanism, recent researches attempted to decentralize this mechanism to accelerate performance. While the new decentralized approaches make transaction processing highly performant, the inherent liveness property is often overlooked. Identifying such property violations is notoriously difficult in concurrent systems such as databases. This paper formally specifies a decentralized wound-wait scheme in TLA+ and verifies it using explicit-state model checker TLC. A vital liveness property violation has been detected and we were also able to offer a fundamental solution to this violation.},
 title = {Understanding Liveness Property in Decentralized Wound-Wait Scheme with TLA+},
 year = {2024}
}