sasa: a SimulAtor of Self-stabilizing Algorithms

被引:1
作者
Altisen, Karine [1 ]
Devismes, Stephane [2 ]
Jahier, Erwan [1 ]
机构
[1] Univ Grenoble Alpes, Grenoble INP, VERIMAG, CNRS, F-38000 Grenoble, France
[2] Univ Picardie Jules Verne, MIS, F-80039 Amiens 1, France
关键词
simulation; debugging; reactive programs; synchronous languages; distributed computing; self-stabilization; atomic-state model;
D O I
10.1093/comjnl/bxab196
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
In this paper, we present sasa, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. sasa is implemented as a faithful representation of the atomic-state model (also called the locally shared memory model with composite atomicity). This model is the most commonly used one in the self-stabilizing area to prove both the correct operation of self-stabilizing algorithms and complexity bounds on them. sasa encompasses all features necessary to debug, test and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Properties of algorithms can be checked using formal test oracles. The sasa distribution also provides several facilities to easily achieve (batch-mode) simulation campaigns. We show that the lightweight design of sasa allows to efficiently perform huge such campaigns. Following a modular approach, we have aimed at relying as much as possible the design of sasa on existing tools, including ocaml, dot and several tools developed in the Synchrone Group of the VERIMAG laboratory.
引用
收藏
页码:796 / 814
页数:19
相关论文
共 42 条
[1]  
Adamek Jordan, 2012, Stabilization, Safety, and Security of Distributed Systems. Proceedings of the 14th International Symposium, SSS 2012, P126, DOI 10.1007/978-3-642-33536-5_13
[2]   Evaluating and optimizing stabilizing dining philosophers [J].
Adamek, Jordan ;
Farina, Giovanni ;
Nesterenko, Mikhail ;
Tixeuil, Sebastien .
JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2017, 109 :63-74
[3]   SASA: A SimulAtor of Self-stabilizing Algorithms [J].
Altisen, Karine ;
Devismes, Stephane ;
Jahier, Erwan .
TESTS AND PROOFS (TAP 2020), 2020, 12165 :143-154
[4]   A FRAMEWORK FOR CERTIFIED SELF-STABILIZATION [J].
Altisen, Karine ;
Corbineau, Pierre ;
Devismes, Stephane .
LOGICAL METHODS IN COMPUTER SCIENCE, 2017, 13 (04)
[5]  
Arora A., 1991, Parallel Processing Letters, V1, P11, DOI 10.1142/S0129626491000161
[6]  
Bernard S, 2010, LECT NOTES COMPUT SC, V5935, P167, DOI 10.1007/978-3-642-11322-2_19
[7]  
Bertot Y., 2004, COQART CALCULUS INDU, DOI [10.1007/978-3-662-07964-5, DOI 10.1007/978-3-662-07964-5]
[8]  
Boulinier C., 2007, THESIS U PICARDIE JU
[9]   The KIND 2 Model Checker [J].
Champion, Adrien ;
Mebsout, Alain ;
Sticksel, Christoph ;
Tinelli, Cesare .
COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II, 2016, 9780 :510-517
[10]   SELF-STABILIZING DEPTH-1ST SEARCH [J].
COLLIN, Z ;
DOLEV, S .
INFORMATION PROCESSING LETTERS, 1994, 49 (06) :297-301