More Web Proxy on the site http://driver.im/

research-article

Construction and formal verification of a fault-tolerant distributed mutual exclusion algorithm

Author:

Evgeniy ShishkinAuthors Info & Claims

Erlang 2017: Proceedings of the 16th ACM SIGPLAN International Workshop on Erlang

Pages 1 - 12

https://doi.org/10.1145/3123569.3123571

Published: 08 September 2017 Publication History

Abstract

Distributed fault-tolerant control algorithms are in great demand nowadays due to their practical importance in cloud computing, Internet of Things (IoT) technology, swarm robotics, and other areas. It is usually hard to make a distributed algorithm fault-tolerant. It is even harder to ensure that such algorithm behaves correctly in the presence of faults of some kind.

In this work, we construct a reliable, adaptive, fault-tolerant distributed mutual exclusion algorithm based on the well-known Ricart-Agrawala algorithm. In order to formally verify it, we use a hybrid approach of deductive reasoning and bounded model-checking.

First, a safety property of the Ricart-Agrawala algorithm is proved in Calculus of Inductive Constructions of Coq proof assistant using assertional reasoning. Then, an extension of that algorithm turning it into fault-tolerant and adaptive to participants set change, is formalized in TLA and checked on a bounded model.

Besides constructing and verifying the algorithm, this work aims to familiarize those interested in constructing highly reliable components with well established verification methods that were used to verify the proposed algorithm.

References

[1]

Joe Armstrong. 2007. Programming Erlang: software for a concurrent world. Pragmatic Bookshelf.

[2]

Thomas Arts and Mads Dam. 1999. Verifying a distributed database lookup manager written in Erlang. In International Symposium on Formal Methods. Springer, 682–700.

[3]

Yves Bertot and Pierre Castéran. 2013. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions . Springer Science & Business Media.

[4]

Tim Carsten. 2013. Verlang repository. "https://github.com/tcarstens/verlang" . (2013). Accessed: 2017-05-26.

[5]

Tushar Deepak Chandra and Sam Toueg. 1996. Unreliable failure detectors for reliable distributed systems. Journal of the ACM (JACM) 43, 2 (1996), 225–267.

Digital Library

[6]

Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. 2009. A reduction theorem for the verification of round-based distributed algorithms. Reachability problems (2009), 93–106.

[7]

Bernadette Charron-Bost and Stephan Merz. 2009. Formal Verification of a Consensus Algorithm in the Heard-Of Model. Int. J. Software and Informatics 3, 2-3 (2009), 273–303.

[8]

Bernadette Charron-Bost and André Schiper. 2009. The heard-of model: computing in distributed systems with benign faults. Distributed Computing 22, 1 (2009), 49–71.

Digital Library

[9]

Flaviu Cristian, Houtan Aghili, Ray Strong, and Danny Dolev. 1995. Atomic broadcast: From simple message diffusion to Byzantine agreement. Information and Computation 118, 1 (1995), 158–179.

Digital Library

[10]

Cezara Drăgoi, Thomas A Henzinger, and Damien Zufferey. 2016. PSync: a partially synchronous language for fault-tolerant distributed algorithms. ACM SIGPLAN Notices 51, 1 (2016), 400–415.

Digital Library

[11]

Clara Benac Earle, Lars-Åke Fredlund, and John Derrick. 2005. Verifying faulttolerant erlang programs. In Proceedings of the 2005 ACM SIGPLAN workshop on Erlang . ACM, 26–34.

Digital Library

[12]

Tzilla Elrad and Nissim Francez. 1982. Decomposition of distributed programs into communication-closed layers. Science of Computer Programming 2, 3 (1982), 155–173.

[13]

Lars-Åke Fredlund and Hans Svensson. 2007. McErlang: a model checker for a distributed functional programming language. In ACM SIGPLAN Notices, Vol. 42. ACM, 125–136.

Digital Library

[14]

Qiang Guo. 2007. Verifying Erlang/OTP components in µCRL. In International Conference on Formal Techniques for Networked and Distributed Systems . Springer, 227–246.

[15]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles . ACM, 1–17.

Digital Library

[16]

Mauro Jaskelioff and Stephan Merz. 2005. Proving the correctness of Disk Paxos. The Archive of Formal Proofs (June 2005). http://isa-afp.org/entries/DiskPaxos. shtml, Formal proof development.

[17]

Leslie Lamport. 2002. Specifying systems: the TLA+ language and tools for hardware and software engineers . Addison-Wesley Longman Publishing Co., Inc.

[18]

Thomas Noll, Lars-ake Fredlund, and Dilian Gurov. 2001. The Erlang verification tool. In TACAS. Springer, 582–586.

[19]

Diego Ongaro and John K Ousterhout. 2014. In search of an understandable consensus algorithm. In USENIX Annual Technical Conference. 305–319.

Digital Library

[20]

Vincent Rahli, David Guaspari, Mark Bickford, and Robert L Constable. 2015. Formal specification, verification, and implementation of fault-tolerant systems using EventML. Electronic Communications of the EASST 72 (2015).

[21]

Glenn Ricart and Ashok K Agrawala. 1981. An optimal algorithm for mutual exclusion in computer networks. Commun. ACM 24, 1 (1981), 9–17.

Digital Library

[22]

Aleta M Ricciardi and Kenneth P Birman. 1993. Process membership in asynchronous environments . Technical Report. Cornell University.

[23]

Ekaterina Sedletsky, Amir Pnueli, and Mordechai Ben-Ari. 2000. Formal verification of the Ricart-Agrawala algorithm. In International Conference on Foundations of Software Technology and Theoretical Computer Science . Springer, 325–335.

[24]

Evgeniy Shishkin. 2017. RAPlus repository. "https://bitbucket.org/unboxed_ type/ra_mutex" . (2017). Accessed:2017-05-26.

[25]

Ulf Wiger and Thomas Arts. 2013. The locks application. "https://github.com/ uwiger/locks" . (2013). Accessed: 2017-05-26.

[26]

James R Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D Ernst, and Thomas Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In ACM SIGPLAN Notices, Vol. 50. ACM, 357–368.

Digital Library

Cited By

Rabhi MDi Pietro R(2024)An efficient failure-resilient mutual exclusion algorithm for distributed systems leveraging a novel zero-message overlay structureComputer Communications10.1016/j.comcom.2024.02.007218(1-13)Online publication date: Mar-2024
https://doi.org/10.1016/j.comcom.2024.02.007
Hashem ISiddiqa AAlaba FBilal MAlhashmi S(2024)Distributed intelligence for IoT-based smart cities: a surveyNeural Computing and Applications10.1007/s00521-024-10136-y36:27(16621-16656)Online publication date: 22-Jul-2024
https://doi.org/10.1007/s00521-024-10136-y
Phyo YOgata K(2018)Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks2018 25th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2018.00023(89-98)Online publication date: Dec-2018
https://doi.org/10.1109/APSEC.2018.00023

Index Terms

Construction and formal verification of a fault-tolerant distributed mutual exclusion algorithm
1. Software and its engineering
  1. Software organization and properties
    1. Extra-functional properties
      1. Software fault tolerance
    2. Software functional properties
      1. Formal methods
        Software verification

Recommendations

Verification of a Hierarchical Generic Mutual Exclusion Algorithm
FORTE '08: Proceedings of the 28th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems

In distributed environments, the shared resources access control by mutual exclusion paradigm is a recurrent key problem. To cope with the new constraints implied by recently developed large scale distributed systems like grids, mutual exclusion ...
Verifying mutual exclusion and liveness properties with split preconditions
Abstract
This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual exclusion algorithm for two process ...
On the completeness of bounded model checking for threshold-based distributed algorithms

Counter abstraction is a powerful tool for parameterized model checking, if the number of local states of the concurrent processes is relatively small. In recent work, we introduced parametric interval counter abstraction that allowed us to verify the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

Erlang 2017: Proceedings of the 16th ACM SIGPLAN International Workshop on Erlang

September 2017

65 pages

ISBN:9781450351799

DOI:10.1145/3123569

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 September 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '17

Sponsor:

SIGPLAN

ICFP '17: ACM SIGPLAN International Conference on Functional Programming

September 8, 2017

Oxford, UK

Acceptance Rates

Overall Acceptance Rate 51 of 68 submissions, 75%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
144
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Rabhi MDi Pietro R(2024)An efficient failure-resilient mutual exclusion algorithm for distributed systems leveraging a novel zero-message overlay structureComputer Communications10.1016/j.comcom.2024.02.007218(1-13)Online publication date: Mar-2024
https://doi.org/10.1016/j.comcom.2024.02.007
Hashem ISiddiqa AAlaba FBilal MAlhashmi S(2024)Distributed intelligence for IoT-based smart cities: a surveyNeural Computing and Applications10.1007/s00521-024-10136-y36:27(16621-16656)Online publication date: 22-Jul-2024
https://doi.org/10.1007/s00521-024-10136-y
Phyo YOgata K(2018)Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks2018 25th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2018.00023(89-98)Online publication date: Dec-2018
https://doi.org/10.1109/APSEC.2018.00023

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents