Title: Verification of Distributed Mutual Exclusion Algorithms.
Abstract: Abstract Many existing token-based, distributed mutualexclusion algorithms can be generalized by a singlealgorithm. The number of messages required to pro-vide mutual exclusion is dependent upon the logicaltopology imposed on the nodes and the policy used toforward subsequent requests.This paper develops models to analyze the per-formance and verify the correctness of the general-ized algorithm. A real-time verification tool, UP-PAAL [2], is used to analyze and verify the algorithm.Both safety and liveness properties are verified. Us-ing the best topology, the generalized algorithm at-tains the same worst-case performance as a central-ized algorithm; that is, three messages per critical sec-tion. However, the generalized algorithm attains bet-ter average-case performance.Keywords: distributed algorithm, mutual exclusion,verification, real-time, token 1 Introduction Many distributed mutual exclusion algorithmshave been proposed [1, 4, 5, 6, 7, 10, 11, 14, 15, 16, 17].These algorithms can be classified into two groups[12, 15]. The algorithms in the first group arepermission-based [1, 5, 6, 14]. A node enters its criti-cal section only after receiving permission from a set ofnodes. The algorithms in the second group are token-based [4, 7, 10, 15, 16, 17]. The possession of a system-wide unique token gives a node the right to enter itscritical section.Lamport proposed one of the first distributedmutual exclusion algorithms [5]. The algorithm ispermission-based and requires 3∗(N −1) messages toprovide mutual exclusion. Another permission-basedalgorithm, proposed by Ricart and Agrawala, reducedthe number of required messages to 2 ∗ (N − 1) mes-sages per critical section entry [13]. Maekawa proposeda permission-based algorithm in which the number ofmessages required is O(√N) [6]. Sanders generalizedpermission-based algorithms [14].Ricart and Agrawala proposed a token-basedalgorithm which is essentially the same as Suzukiand Kasami’s algorithm [16]. Based on Suzuki andKasami’s algorithm, Singhal proposed a heuristically-aided algorithm that uses state information to moreaccurately guess the location of the token [15]. Themaximum number of messages required by these threealgorithms is N.By imposing a tree-based logical structure on thenodes, another class of token-based algorithms hasbeen obtained. In this class of algorithms, all of thenodes, except for the root node, are on a path to theroot node (a sink node) in the logical structure. Thelogical structure determines the path along which arequest message travels. There are two different typesof logical structures: dynamic and static.An algorithm, based on a dynamic logical struc-ture, was proposed by Trehel and Naimi [17]. Thebasic notion underlying this algorithm is path rever-sal. Path reversal at each node is performed as arequest from node x travels along the path from nodex to the root node. As the request travels, node x be-comes the new parent of each node on the path, exceptfor node x. Thus, node x becomes the new root node.A complete analysis of path reversal has been given byGinat [3]. The average number of messages requiredper critical section is O(log(N)).If a static logical structure is used, the basic no-tion underlying the algorithm is what we call edge re-versal [9]. Edge reversal at each node is performedas the request from node x travels along the path fromnode x to the root node. At each node, the directionof each edge on the path is changed to point towardsnode x; that is, to the neighboring node who sent therequest on behalf of node x. However, the shape ofthe logical structure never changes. Suprisingly, thissmall change results in algorithms which have a smallfixed upper bound on the number of messages requiredper critical section, and the upper bound only dependson the logical structure. One such algorithm was pro-posed by Raymond [10]. The algorithm assumes thatthe static logical structure is an unrooted tree. If the
Publication Year: 2008
Publication Date: 2008-01-01
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot