ViewChecker: A Sound and Complete Checker for View-Serializability in Quadratic Time Complexity

Abstract

Atomicity is a crucial correctness criterion for concurrent programs. In multi-threaded programs, executions of procedures are regarded as transactions. These transactions may fail to behave atomically, resulting in transactional atomicity violations. To dynamically check for atomicity, existing atomicity checkers focus on the well-studied notions of conflict-serializability and view-serializability to ensure that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. However, all the current methods for checking view-serializability are inefficient. In this paper, we present ViewChecker, a novel violation detection method for checking view-serializability in an online (dynamic) setting. ViewChecker is the first trace-based checker, using vector clocks to guarantee soundness and completeness. We also provethat ViewChecker is more efficient than any existing solution with quadratic time complexity

Date
Jun 18, 2024 2:00 PM — 3:00 PM
Event
Weekly Talk
Location
Zoom