Generalize Synchronization Mechanism: Specification, Properties, Limits
Chih-Wei Chien, Chi-Yeh Chen
TL;DR
This work addresses the lack of a universal model for synchronization across shared and distributed memory by introducing a general framework that treats synchronization as multi-writer to single-writer convergence. It analyzes five core properties—consistency, writing freedom, latency, loading, and fault tolerance—within a horizontal (pass-based) and vertical (quorum/arbitration) structure, and derives formal limits including dynamic- and static-arbiter bounds akin to the ROLL theorem. By applying the framework to Paxos, Raft, Viewstamp Replication, EPaxos, CRDTs, and atomic operations, it elucidates how each mechanism trades one property off against others and showcases how different quorums and arbitration strategies affect progress and fault tolerance. The work provides a principled basis for designing new synchronization mechanisms and for choosing among existing ones based on system requirements and fault models, potentially guiding practitioners toward optimal trade-offs in real deployments.
Abstract
Shared resources synchronization is a well studied problem, in both shared memory environment or distributed memory environment. Many synchronization mechanisms are proposed, with their own way to reach certain consistency level. This thesis further found that there is no perfect synchronization mechanism. Each of them has its properties at different level. For example, to enforce strong consistency, writers may loose writing freedom or it would take more time to coordinate. This thesis proposes a framework to generalize all synchronization mechanism in a formal way for better reasoning on properties, from the perspective of multi-writer to single-writer convergence. Therefore, limitations prevent a synchronization mechanism from achieving every property at its optimal level. CAP and ROLL were proposed in previous works to explain such. CAP theorem states that it can only achieve two of Consistency, Availability and Partition tolerance properties. ROLL Theorem uses a framework to model leaderless SMR protocol and states quorum size and fault tolerance are trading off. The thesis covers five properties in a more understandable way to analyze trade-offs and explore new mechanisms.