Suzuki-Kasami Distributed Mutual Exclusion Algorithm (SKDMXA) that is proposed in [1] is analyzed. --------------------------------------------------------------------- Author: Kazuhiro Ogata Email: ogata@jaist.ac.jp [1] I. Suzuki and T. Kasami: A distributed mutual exclusion algorithm, ACM TOCS, 3(4):344-349, 1985 This directory contains the three files. 1. skdmxa.sal - A finite model of the algorithm: Each node makes requests a finite times to enter its critical section. This model does not satisfy the lockout (starvation) freedom property. 2. fix_skdmxa.sal - A fixed version of the above model. This model satisfies the lockout (starvation) freedom property. 3. inf_skdmxa.sal - A infinite model of the algorithm: Each node makes requests an unbounded times to enter its critical section. k-induction is used to prove that this model satisfies the mutual exclusion property. First the algorithm is briefly described. The program executed by each node i \in {1,...,N} can be described as this procedure P1; begin requesting := true; if not have_privilege then begin rn[i] := rn[i] + 1; for all j in {1,2,...,N} - {i} do send request(i,rn[i]) to node j; wait until privilege(queue,ln) is received; have_privilege := true end; Critical Section; ln[i] := rn[i]; for all j in {1,2,...,N} - {I} do if not in(queue,j) and (rn[j] = ln[j] + 1) then queue := append(queue,j); if queue =/= empty then begin have_privilege := false; send privilege(tail(queue),ln) to node head(queue) end; requesting := false end; procedure P2; { requesting(j,n) is received; P2 is indivisible } begin rn[j] := max(rn[j],n); if have_privilege and not requesting and (rn[j] = ln[j] + 1) then begin have_privilege := false; send privilege(queue,ln) to node j end end; where N is the number of nodes, requesting and have_privilege are Boolean variables, rn and ln are integer arrays of size N, and queue is the queue of integers. For each node i \in {1,...,N}, initially, requesting is false, have_privilege is true if i = 1 and false otherwise, rn[j] and ln[j] for each j \in {1,...,N} are 0, and queue is empty. Basically, rn[j] is the number of requests made by node j and ln[j] is the number of the accomplished ones of them. The basic idea in the algorithm is to transfer the privilege for entering a critical section with a single privilege message. Next the common part of the three models is described. The algorithm is modeled with 13 sets of transitions (try, set_req, check_priv, inc_req_no, send_req, wait_priv, exit, complete_req, update_queue, check_queue, transfer_priv, reset_req, and receive_req), each of which denotes part of the algorithm as this try: procedure P1; begin set_req: requesting := true; check_priv: if not have_privilege then begin inc_req_no: rn[i] := rn[i] + 1; send_req: (denoting one iteration of the loop) for all j in {1,2,...,N} - {i} do send request(i,rn[i]) to node j; wait_priv: wait until privilege(queue,ln) is received; have_privilege := true end; Critical Section; exit: (leaving the ciritical section) complete_req: ln[i] := rn[i]; update_queue: (denoting one iteration of the loop) for all j in {1,2,...,N} - {I} do if not in(queue,j) and (rn[j] = ln[j] + 1) then queue := append(queue,j); check_queue: if queue =/= empty then begin transfer_priv: have_privilege := false; send privilege(tail(queue),ln) to node head(queue) end; reset_req: requesting := false end; receive_req: procedure P2; { requesting(j,n) is received; P2 is indivisible } begin rn[j] := max(rn[j],n); if have_privilege and not requesting and (rn[j] = ln[j] + 1) then begin have_privilege := false; send privilege(queue,ln) to node j end end; The first 12 sets of transitions are related to 12 labels (rem, l1, l2, l3, l4, l5, cs, l6, l7, l8, l9, and l10). If a node is at rem, l1, l2, l3, l4, l5, cs, l6, l7, l8, l9, and l10, then the node is ready to execute try, set_req, check_priv, inc_req_no, send_req, wait_priv, exit, complete_req, update_queue, check_queue, transfer_priv, reset_req, and receive_req, respectively. The following types are defined. Node_Id: TYPE = [1..N]; Queue_Idx: TYPE = [0..(L+1)]; Node_Id denotes node IDs, and Queue_Idx denotes indexes of arrays used to model queues. N is the number of nodes, and L is the capacity of queues. The queue is modeled as an array data and a pointer tl as this Queue: TYPE = [# data: ARRAY Queue_Idx OF Node_Id, tl: Queue_Idx #]; tl points an element into which a next item is put. If tl is 1, the queue is empty, and if tl is L+1, the queue is saturated. If the queue is not empty, data[1] is the top element. L should be greater than or equal to the number N of nodes. The algorithm involves two kinds of messages: request and privilege messages. The types for these messages are defined as this Request: TYPE = [# node: Node_Id, no: Bnat #]; Privilege: TYPE = [# queue: Queue, done: ARRAY Node_Id OF Bnat #]; The network is modeled as two channels for each ordered pair (i,j) of nodes. The capacity of each channel is 1. Channels are modeled as arrays as this GLOBAL reqmedium : ARRAY Node_Id OF ARRAY Node_Id OF ReqMsg GLOBAL privmedium : ARRAY Node_Id OF ARRAY Node_Id OF PrivMsg The two types ReqMsg and PrivMsg are defined as this ReqMsg: TYPE = [# new: BOOLEAN, req: Request #]; PrivMsg: TYPE = [# new: BOOLEAN, priv: Privilege #]; A channel is empty if the corresponding new field is false, and contains a message otherwise. Then each model is described. 1. A finite model of the algorithm (skdmxa.sal). In order to make the state space finite, the number of requests made by each node should be finite. Then, each node is supposed to make requests M times to enter its critical section. The finite model where N = 2, L = 2 and M = 2 is analyzed as follows: sal-smc -v 3 --assertion='skdmxa{;2,2,2}!mutex' sal-wmc -v 3 --assertion='skdmxa{;2,2,2}!reachable' sal-deadlock-checker -v 3 --module='skdmxa{;2,2,2}!system' sal-smc -v 3 --assertion='skdmxa{;2,2,2}!lofree' The first one checks if the finite model satisfies the mutual exclusion property, the second one checks if there exists an execution path such that each node enters its critical section, the third one checks if there exist any deadlock states, and the last one checks if the finite model satisfies the lockout freedom property. The results of the first three analyses are as expected. But, the last analysis finds a counterexample. Any model checker of SAL 2.1 does not suppose any fairness to model-check liveness properties. In the last analysis, wait_priv and receive_req are given weak fairness. 2. A fixed finite model of the algorithm (fix_skdmxa.sal). Counterexamples given by the last analysis of the previous model indicate that a node should not receive any request messages if the node is at l7, l8 or l10. Therefore, NOT(pc = l7) AND NOT(pc = l8) AND NOT(pc = l10) is added to the guard of receive_req. As the previous model, the fixed finite model where N = 2, L = 2 and M = 2 is analyzed as follows: sal-smc -v 3 --assertion='skdmxa{;2,2,2}!mutex' sal-wmc -v 3 --assertion='skdmxa{;2,2,2}!reachable' sal-deadlock-checker -v 3 --module='skdmxa{;2,2,2}!system' sal-smc -v 3 --assertion='skdmxa{;2,2,2}!lofree' For this model, all the results are as expected. 3. A infinite model of the algorithm (inf_skdmxa.sal). In this model, each node can make requests an unbounded times to enter its critical section. Therefore, the state space can be infinite, and only the infinite bounded model checker can be used to analyze the model. k-induction is used to prove that the model satisfies the mutual exclusion property as this sal-inf-bmc -v 3 -i -ice -d 1 -l lemma1 -l lemma2 --assertion='inf_skdmxa{;2,2}!mutex' The two lemmas are used. They are proved with k-induction as this sal-inf-bmc -v 3 -i -ice -d 1 --assertion='inf_skdmxa{;2,2}!lemma1' sal-inf-bmc -v 3 -i -ice -d 1 -l lemma1 --assertion='inf_skdmxa{;2,2}!lemma2'