Homework Assignment #5 Solution

Contents




Assignment Objectives and Policies



Get acquainted with




simple model development in Promela; basic model checking in Spin;




the use of LTL formulas for expressing properties of systems. The following Assignment Policies should be upheld:




Collaboration Policy. This homework may be done in individually or in pairs. Use of the Internet is allowed, but should not include searching for existing solutions. In case it is done in pairs, only one of the members should submit through Canvas.




Under absolutely no circumstances code can be exchanged between students. Excerpts of code presented in class can be used.




Assignments from previous offerings of the course must not be re-used. Violations will be penalized appropriately.




Late Policy. Late submissions are allowed with a penalty of 2 points per hour past the deadline.




Note: This assignment draws from [?]. In particular, the description given in Sec. ?? is taken from pp. 238-239.



















1












Leader Election



In current distributed systems several services are offered by some dedicated process(es) in the system. Consider, for example, address assignment and regis-tration, query coordination in a distributed database system, clock distribution, token regeneration after token loss in a token ring network, initiation of topology updates in a mobile network, load balancing, and so forth. Usually many pro-cesses in the system are potentially capable of providing these services. However, for consistency reasons it is usually the case that at any time only one process is allowed to actually provide a given service. This process – called the “leader”




– is in fact elected. Leader election is a simple form of symmetry breaking. Sometimes it suffices to elect an arbitrary process, but for other services it is important to elect the process with the best capabilities for performing that service. Here we abstract from specific capabilities and use ranking on the basis of process identities. Each process has a unique identity, and it is assumed that a total ordering exists on these identities. The idea is therefore that the higher the process’ identity, the better its capabilities.




The process of choosing a leader is known as leader election. A leader election algorithm (LEA):




is decentralized;




each node has the same local algorithm;




each node has a unique ID and IDs form a totally ordered set; upon termination one node is ’leader’ and the rest are ’lost’.




In this assignment we are going to look at two leader election algorithms on a ring topology:




Part I: Chang-Roberts LEA or CR-LEA.




Part II: Dolev-Klawe-Rodeh LEA or DKR-LEA (http://w3.cs.huji. ac.il/~dolev/pubs/n-log-n.pdf).




In each of these two algorithms, initially all processes are active. A process may become passive, in which case it is out of the race to become leader. The conditions under which it becomes passive depends on the algorithm and will be made precise below.




Part I: CR-LEA



This part of the assignment requests that you perform the task of implementing CR-LEA in Promela.
















2















3.1 CR-LEA Description




The idea of the algorithm is that only the message with the highest id completes one round in the ring. Each node in the ring should behave as indicated by the following pseudocode:




1 send ( id ) to next process in ring ;




while ( true ) do
3receive ( m );

4
if ( m = id ) then
stop ;
/*
process
is the leader
*/
5
if
( m

id )
then
send ( m ); /*
forward
identifier ,
id
becomes passive */
6
if
( m
<
id )
then
do nothing ; /* purge
message */




od



Once the leader is elected, every node should be informed and print out the following message exactly once (per node): “I am node X and I know the leader is Y”.




Finally, make sure that the execution of your implementation does not end in a timeout.




Note: CR-LEA has message complexity O(N2) (it takes at most messages to elect a leader). DKR-LEA has message complexity O(N log




3.2 Implementation




Implement CR-LEA in Promela. Nodes should be connected in a ring topology. The buffer size for the Promela channels should be set to 2 N where N is the number of processes in the network.

Hint: It is strongly recommended that, on a first reading, you continue with the next section. The implementation for DKR-LEA will be provided for you, and will serve as a guideline for implementing, the more simple, CR-LEA.




Part II: DKR-LEA



This part of the assignment requests that you perform just one task, namely verify properties of DKR-LEA using LTL formulae.




4.1 DKR-LEA Description




An implementation of DKR-LEA in Promela is provided for you below. First, an informal description. DKR adapts ideas from Franklin’s algorithm (which applies to undirected rings) with the aim of improving the message complexity of the Chang-Roberts algorithm. The basic idea depends on the fact that, since order of communication is preserved, the effect of the algorithm is as though the activities of the system could be separated into synchronous phases. Initially all processes are active. In each phase, sufficient messages are passed so that each active process learns the current numbers of the two closest active processes on its left. With this information, each active process can determine if it is the active process immediately following a local maximum. If so, it assumes the local maximum as its own number, and continues as active on to the next phase.







3















If not, it becomes passive and merely acts as a communication relay, passing on the messages initiated by active processes during later phases.




4.2 Implementation




Consider the following implementation1 in Promela of DKR-LEA. It consists of two proctypes, nnode and init. The code for these proctypes are presented in two parts to ease readability. The former is the code that runs on each node in the ring; the latter initializes the ring.




It is suggested that you perform a symbolic execution of this algorithm in a ring with 5 nodes n1 with id 1, : : :, n5 with id 5, connected as follows:








n1 h
n2
v
n5




=






!

n3 /n4







To simplify the state of the system you can write the messages that are exchanged on the arrows, the local state of each node next to the name of the node and you may assume that all nodes fire messages at the same time (although of course this is not necessarily the case in practice).












4.2.1
Part 1


















1
# define
N
5
/*
number
of pr oc e ss e s in the ring */


2
# define
L
10
/*
size
of
buffer
( =
2*N)
*/


3
byte I ;




/*
will
be
used in
init
for
a s si gn i ng
ids to nodes */
4






















5
mtype = { one ,
two ,
winner
};


/* symb . Msg . Names */


6
chan q [ N ] = [ L ]
of {
mtype ,
byte };
/* a s y n c h r o n o u s
channels
*/
7






















8
proctype
nnode
( chan
inp , out ;
byte mynumber )






{bit Active = 1 , k n o w _ w i n n e r = 0;
byte nr , maximum = mynumber , n e i g h b o u r R ;



11




















12
xr
inp ;
/*
channel
a s se r ti on : e x cl us i ve
recv
access
to
channel
in */
13
xs
out ;
/*
channel
a s se r ti on : e x cl us i ve
send
access
to
channel
out */
14























printf ( " MSC : %d\n" , mynumber );



out ! one ( mynumber );
end :do
:: inp ? one ( nr ) -
if
:: Active -
21
if
22
:: nr != maximum -
23
out ! two ( nr );
24
n e i g h b o u r R = nr
25
:: else -
26
k n o w _ w i n n e r = 1;
27
out ! winner , nr ;
28
fi
:: else -
30 out ! one ( nr )

fi



32




:: inp ? two ( nr ) -



if
:: Active -
36
if
37
:: n e i g h b o u r R nr && n e i g h b o u r R maximum -
38
maximum = n e i g h b o u r R ;
39
out ! one ( n e i g h b o u r R )
40
:: else -
41
Active = 0
42
fi
:: else -
44 out ! two ( nr )

fi
:: inp ? winner , nr -
if
:: nr != mynumber -
49 printf (" MSC : LOST \n" );

:: else -
51 printf (" MSC : LEADER \n" );

fi ;
if
:: k n o w _ w i n n e r
:: else - out ! winner , nr
fi ;
break
od
}


4.2.2 Part 2




The init process assigns random ids to each node and then starts them.




1 init {




byte proc ;
3 byte Ini [6]; /* N <=6 ra n do m iz e the process numbers */

atomic {
5 I = 1; /* pick a number to be assigned 1.. N */

do
:: I <= N -
8
if
/*
non - d e t e r m i n i s t i c choice */
9
:: Ini [0]
==
0
&&
N
=
1
-
Ini [0]
=
I
10
:: Ini [1]
==
0
&&
N
=
2
-
Ini [1]
=
I
11
:: Ini [2]
==
0
&&
N
=
3
-
Ini [2]
=
I
12
:: Ini [3]
==
0
&&
N
=
4
-
Ini [3]
=
I
13
:: Ini [4]
==
0
&&
N
=
5
-
Ini [4]
=
I
14
:: Ini [5]
==
0
&&
N
=
6
-
Ini [5]
=
I /* works for up to N=6 */
15
fi ;






















16
I ++






















:: I N -/* assigned all numbers 1.. N */
break
od ;



20




/* start all nodes in the ring */



proc = 1;
do
:: proc <= N -
run nnode ( q [ proc -1] , q [ proc % N ] , Ini [ proc -1]);
proc ++
:: proc N -
break
od
}
}



4.3 Verification




Using assertions:



Verify that if a node is selected as leader, then its id is the maximum one.



Verify that only one leader is elected. Hint: add a variable nr_leaders to count the number of processes that think they are leaders.



Using LTL formulae:



Some node is eventually elected as leader. Hint: use nr_leaders.



Eventually, it will always be true that there is exactly one elected leader



It is always the case that there are either 0 or 1 leaders chosen.



Submission Instructions



Submit your Promela source code via Canvas by the indicated date and time. Submit a zip file named Assignment5_<Surnames.zip (where <Surnames should be replaced by the surnames of the team members) containing:



6
The Promela source for the first exercise



The Promela source for each verification item together with the output from spin (save as text).



In total you should have 10 files.




CR-LEA source code



CR-LEA running output as txt



DKR-LEA source code with assertion statements



DKR-LEA running output as txt



DKR-LEA source code with ltl statement 1 at top of file



DKR-LEA source code with ltl statement 2 at top of file



DKR-LEA source code with ltl statement 3 at top of file



DKR-LEA ltl statement 1 verification output as txt



DKR-LEA ltl statement 2 verification output as txt



DKR-LEA ltl statement 3 verification output as txt


























































































7