CS 511: Assignment 5

• Assignment Objectives and Policies

Get acquainted with

• simple model development in Promela;

• basic model checking in Spin;

The following Assignment Policies should be upheld:

Collaboration Policy. This homework must be done in groups of at most two. 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.

1

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. 2 is taken from pp. 238-239.

• 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.

2

• Part I: CR-LEA

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

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 n(n+1)

2

messages to elect a leader). DKR-LEA has message complexity O(N log N).

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.

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

3

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. 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

n2 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).

• The code itself is from the spin website.

4

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;

10 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

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

16 out ! one ( mynumber );

17 end :do

18 :: inp ? one ( nr ) ->

19 if

20 :: 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

29 :: else ->

30 out ! one ( nr )

31 fi

32

33 :: inp ? two ( nr ) ->

34 if

35 :: 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

43 :: else ->

44 out ! two ( nr )

45 fi

46 :: inp ? winner , nr ->

47 if

48 :: nr != mynumber ->

49 printf (" MSC : LOST \n" );

50 :: else ->

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

52 fi ;

53 if

54 :: k n o w _ w i n n e r

55 :: else -> out ! winner , nr

56 fi ;

57 break

58 od

59 }

5

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 ++

17 :: I > N ->/* assigned all numbers 1.. N */

18 break

19 od ;

20

21 /* start all nodes in the ring */

22 proc = 1;

23 do

24 :: proc <= N ->

25 run nnode ( q [ proc -1] , q [ proc % N ] , Ini [ proc -1]);

26 proc ++

27 :: proc > N ->

28 break

29 od

30 }

31 }

4.3 Verification

1. Using assertions:

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

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

• Submission Instructions

Submit your Promela source code via Canvas by the indicated date and time.

Submit a zip file named Assignment5.zip containing:

1. The Promela source for the first exercise

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

In total you should have 4 files.

1. CR-LEA source code

6

2. CR-LEA running output as txt

3. DKR-LEA source code with assertion statements

4. DKR-LEA running output as txt

7