Graft: General Purpose Raft Consensus in Elixir

被引:4
作者
Le Brun, Matthew Alan [1 ]
Attard, Duncan Paul [1 ]
Francalanza, Adrian [1 ]
机构
[1] Univ Malta, Dept Comp Sci, Msida, Malta
来源
ERLANG '21: PROCEEDINGS OF THE 20TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON ERLANG | 2021年
关键词
Distributed consensus; Raft; Asynchronous components; Elixir; BEAM; Runtime Verification; Testing; HENNESSY-MILNER LOGIC;
D O I
10.1145/3471871.3472963
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present Graft, a generic tool for creating distributed consensus clusters running the Raft algorithm using state machines in Elixir. Our tool exhibits performance that is comparable to that of the Raft implementation supporting the original proposal, as well as the performance of other state-of-the-art Raft implementations running on the BEAM. The correctness of our tool is also ascertained through a number of complementary verification methods.
引用
收藏
页码:2 / 14
页数:13
相关论文
共 48 条
[1]  
Aceto L., 2017, 37 IARCS ANN C FDN S, DOI [10.4230/LIPIcs.FSTTCS.2017.7, DOI 10.4230/LIPICS.FSTTCS.2017.7]
[2]  
Aceto L., 2018, LIPICS
[3]   Adventures in Monitorability: From Branching to Linear Time and Back Again [J].
Aceto, Luca ;
Achilleos, Antonis ;
Francalanza, Adrian ;
Ingolfsdottir, Anna ;
Lehtinen, Karoliina .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL)
[4]   Determinizing monitors for HML with recursion [J].
Aceto, Luca ;
Achilleos, Antonis ;
Francalanza, Adrian ;
Ingolfsdottir, Anna ;
Kjartansson, Saevar Orn .
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2020, 111
[5]   RECOGNIZING SAFETY AND LIVENESS [J].
ALPERN, B ;
SCHNEIDER, FB .
DISTRIBUTED COMPUTING, 1987, 2 (03) :117-126
[6]  
Armstrong J., 2007, Programming Erlang: Software for a Concurrent World, V1st
[7]   Better Late Than Never or: Verifying Asynchronous Components at Runtime [J].
Attard, Duncan Paul ;
Aceto, Luca ;
Achilleos, Antonis ;
Francalanza, Adrian ;
Ingolfsdottir, Anna ;
Lehtinen, Karoliina .
FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 :207-225
[8]   A Monitoring Tool for a Branching-Time Logic [J].
Attard, Duncan Paul ;
Francalanza, Adrian .
RUNTIME VERIFICATION, (RV 2016), 2016, 10012 :473-481
[9]  
Attard Duncan Paul, 2021, DETECTER TUTORIAL
[10]  
Baier C, 2006, LECT NOTES COMPUT SC, V4229, P212