Page 203 - 《软件学报》2021年第6期

谷晓松 等:支持乱序执行的 Raft 协议 1777

ParallelRaft-SE 到 Multi-Paxos 的精化关系以及 ParallelRaft-CE 的正确性.
目前,我们正在使用 TLAPS(TLA+Proof System) [14,36] 定理证明系统为 ParallelRaft-CE(以及 Raft)开发机械
化正确性证明.此外,我们还将从顺序/乱序提交、顺序/乱序执行的角度对已知的分布式共识协议进行综述,并利
用形式化方法研究它们之间的关系.

References:
[1] Fischer MJ, Lynch NA, Paterson MS. Impossibility of distributed consensus with one faulty process. Journal of the ACM (JACM),
1985,32(2):374−382. [doi: https://doi.org/10.1145/3149.214121]
[2] Herlihy M. Wait-Free synchronization. ACM Trans. on Programming Languages and Systems (TOPLAS), 1991,13(1):124−149.
[doi: https://doi.org/10.1145/114005.102808]
[3] Weil SA. Ceph: Reliable, scalable, and high-performance distributed storage [Ph.D. Thesis]. Santa Cruz: University of California,
2007.
[4] Corbett JC, Dean J, Epstein M, Fikes A, Frost C, Furman JJ, Ghemawat S, Gubarev A, Heiser C, Hochschild P, Hsieh W. Spanner:
Google’s globally distributed database. ACM Trans. on Computer Systems (TOCS), 2013,31(3):1−22.
[5] https://www.mysql.com/
[6] Zheng J, Lin Q, Xu J, Wei C, Zeng C, Yang P, Zhang Y. PaxosStore: High-availability storage made practical in WeChat. Proc. of
the VLDB Endowment, 2017,10(12):1730−1741.
[7] Cao W, Liu Z, Wang P, Chen S, Zhu C, Zheng S, Wang Y, Ma G. PolarFS: An ultra-low latency and failure resilient distributed file
system for shared storage cloud database. Proc. of the VLDB Endowment, 2018,11(12):1849−1862.
[8] Lamport L. Paxos made simple. ACM Sigact News, 2001,32(4):18−25.
[9] Lamport L. The part-time parliament. ACM Trans. on Computer Systems (TOCS), 1998,16(2):133−169.
[10] Ongaro D, Ousterhout J. In search of an understandable consensus algorithm. In: Proc. of the 2014 USENIX Annual Technical
Conf. ({USENIX}{ATC} 2014). 2014. 305−319.
[11] Schneider, Fred B. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys,
1990,22(4):299−319.
[12] Abadi M, Lamport L. The existence of refinement mappings. Theoretical Computer Science, 1991,82(2):253−284.
[13] Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston: Addison-Wesley
Longman Publishing Co., Inc., 2002.
[14] Lamport L. The TLA+ hyperbook. 2015. http://research.microsoft.com/enus/um/people/lamport/tla/hyperbook.html
[15] Lamport L. The temporal logic of actions. ACM Trans. on Programming Languages and Systems (TOPLAS), 1994,16(3):872−923.
[16] Yu Y, Manolios P, Lamport L. Model checking TLA+ specifications. In: Proc. of the Advanced Research Working Conf. on
Correct Hardware Design and Verification Methods. Berlin, Heidelberg: Springer-Verlag, 1999. 54−66.
[17] https://github.com/HappyCS-Gu/Parallel-Raft-tla
[18] Yi XC, Wei HF, Huang Y, Qiao L, Lü J. TPaxos consensus protocol in PaxosStore: Derivation, specification, and refinement. Ruan
Jian Xue Bao/Journal of Software, 2020,31(8):2336−2361 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/
5964.htm [doi: 10.13328/j.cnki.jos.005964]
[19] Ji Y, Wei HF, Huang Y, Lü J. Specifying and verifying CRDT protocols using TLA+. Ruan Jian Xue Bao/Journal of Software,
2020,31(5):1332−1352 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5956.htm [doi: 10.13328/j.cnki.jos.
005956]
[20] Lamport L. Summary of tla+. http://lamport.azurewebsites.net/tla/summary-standalone.pdf
[21] Yuan D, Luo Y, Zhuang X, Rodrigues GR, Zhao X, Zhang Y, Jain PU, Stumm M. Simple testing can prevent most critical failures:
An analysis of production failures in distributed data-intensive systems. In: Proc. of the 11th USENIX Symp. on Operating Systems
Design and Implementation (OSDI). 2014. 249−265.
[22] Ongaro D. Consensus: Bridging theory and practice [Ph.D. Thesis]. Stanford University, 2014.
[23] Lampson B. The ABCD’s of Paxos. In: Proc. of the 20th Annual ACM Symp. on Principles of Distributed Computing (PODC),
Vol.1. 2001. 13.