Different level of consistency needs different level of coordination
Differences of Writing freedom enable the dynamic/static arbiter type and different coordination latency
Bigger loading trades off for better fault tolerance
Dynamic and static arbiter have different limitation on trading off loading and fault tolerance
Analysis
Assuming linearizability for consistency
The split brain problem
Two or more projection result at the end of a pass
Not converged
Caused by insufficient fact spreading
Lemma 1. In the context of linearizability, the amount of fault does not exceed \(\lfloor \frac{n-1}{2} \rfloor\)
\(proof.\) By contradiction. Having half or more failed may end up with two different projection result.
Static arbiter
1RTT to decide in \(pre\)
1RTT to use in \(exe\)
Dynamic arbiter
1RTT to decide
2RTT or even more to linearize
Theorem 1. Under n writing freedom, one round trip is optimal for deciding to write or abort.
\(proof.\) The arbitration rule determines to response negative message to all the other writers except the converged writer as positive.
Need sufficient size to decide static/dynamic arbiter
Combined with lemma 1, all properties are related to quorum.
Key concept for loading trading for fault tolerance
Not only focus on fact spreading, but also on which writer does not get the fact
The principle
There must be at least one writer holding facts across two rounds to deliver them
Count which writer can not deliver
writers without facts + faulty writers
A writer is either without fact or faulty
Theorem 2. To decide a dynamic arbiter, \(2(n − |Q|) + f − 2 < n\) needs to be satisfied
\(proof.\) Writers without facts: \(2(n − |Q|)\), faulty writers: \(f\). Exclude 2 writer for having additional facts.
EPaxos uses \(\lfloor \frac{3n}{4} \rfloor\) quorum size for maxing out the fault tolerance
\(ROLL\) theorem is the theorem for fixed size quorum and dynamic arbiter situation, under the consistency level of linearizability.
Theorem 3. To decide a static arbiter, \((n − |Q|) + f \leq \lceil \frac{n-1}{2} \rceil\) needs to be satisfied.
\(proof.\) Writers without facts: \((n − |Q|)\), faulty writers: \(f\). According to Lemma 1, to have sufficient writers to fail, the combination should not exceed \(\lceil \frac{n-1}{2} \rceil\)
Raft and VR uses \(n\) quorum to tolerate minority fault.
Key concept behind Theorem 2 and 3 can be applied to more situation.
Eventual consistency trades weakest consistency for every other properties to be optimal
For consistency level in-between eventual and linearizability, decompose into the combination of strongest and weakest, to be analyzed in the known way.
The Discussion
Extra findings and details
Properties do not indicate performance.
Clock only can help local resolving, reducing latency by 1 RTT
Apply key concept to dynamic or non-homogeneous quorum
Application logic in synchronization
TOQ uses time to reduce 1 RTT in \(exe\) for EPaxos
Exploring New Mechanism
Use priority tree to resolve conflict locally. Order conflict writes by applying fixed priority.
There are still more details to discuss. Especially on applying to real implementation.
Some optimization performed on the implementation can not be covered in the framework.
Write specification of the framework using TLA+, thinking in a more formal method way.
The end
Special Thanks
Thanks Prof. Chen for allowing me to research the topic I've been looking forward to studying. Thanks Prof. Hsieh for emphasizing the importance of simplicity during graph theory course.
FAQ
Why the analysis is only applicable to the valid synchronization mechanism? Why it can not be placed on others? Without the guarantee on both correctness and progression, the mechanisms can easily be designed to have any property at optimal level. Correctness and progression come at a price only when they are guaranteed, so that there are trade-offs and limits.
Generalize Synchronization Mechanisms for Analyzing Properties Trade-offs and Exploring New Mechanisms 泛化同步機制以分析屬性權衡及探索新機制 (Link to the paper: https://arxiv.org/abs/2309.11972 )
{"showTitle":"false","showTags":"false","slideOptions":"{\"theme\":\"night\",\"transition\":\"slide\"}","title":"Generalize Synchronization Mechanisms for Analyzing Properties Trade-off and Exploring New Mechanisms","description":"Trying to explain synchronization mechanisms universally in a formal way. Newton tried to explained universe as a mechanical machine with math. I am a fan of Newton so I tried to do the same on computing universe, here focusing on synchronization.","image":"https://hackmd.io/_uploads/HJPlvPish.png","contributors":"[{\"id\":\"fc8603a8-fb74-41e4-86f9-f8a28701b0d6\",\"add\":17820,\"del\":5842}]"}