<< Chapter < Page Chapter >> Page >

They following algorithm is an attempt to implement mutual exclusion for two processes.Here, each process is willing to defer to the other. (It also introduces Promela's goto , which lets you branch to a label; this is an alternate wayof implementing loops and other control flow.)

Verify whether the algorithm is correct or not.

  • Verify using SPIN's built-in checks, without using temporal logic.
  • Verify using temporal logic.
  • If it is incorrect, find a shortest possible trace when it fails.

1 int x, y, z; 23 active[2] proctype user()4 { 5 int me = _pid+1; /* me is 1 or 2. */6 7 L1:8 x = me; 9 if10 :: (y != 0&&y != me) ->goto L1 /* Try again. */ 11 :: (y == 0 || y == me) /* Continue... */12 fi; 1314 z = me; 15 if16 :: (x != me) ->goto L1 /* Try again. */ 17 :: (x == me) /* Continue... */18 fi; 1920 y = me; 21 if22 :: (z != me) ->goto L1 /* Try again. */ 23 :: (z == me) /* Continue... */24 fi; 2526 /* Entering critical section. */ 27 /* ... */28 29 /* Leaving critical section. */30 }

As usual, we must check that no more than one process is in the critical section at a time. We canour usual code in_crit++; assert(in_crit == 1);in_crit--; and declaring in_crit global. This code passes verification, but warns us that this code isn't necessarily even executed!

For a critical section protocol to be valid, it must also guarantee that each process eventually entersthe critical section. Since the goto s create a control flow loop, we can check this by looking for non-progress cycles,labeling the critical section as progress.

The shortest counter-example trace. For brevity, the local values of me are not shown, since they cannot vary.

Using temporal logic, we can create a formula that describe our desired behavior:``Eventually, each process gets to the critical section, but not both at the same time.''One such formula is ( p q ( p q ) ) where we define #define p (user[0]@crit)#define q (user[1]@crit) and define the label crit in the critical section.

This is a Promela version of an algorithm once recommended by a major computer manufacturer.As you can see, like many other mutual exclusion algorithms that have been proposed, it is flawed.

The following is pseudocode for an attempt to implement critical sections for n processes. It is based on the idea that processes take numbers,and the one with the lowest number proceeds next. This algorithm has one small flaw.Your task is to find and fix the flaw. In particular, show the following steps of this process.

  • Implement this algorithm in Promela, and show the resulting code. Include any code added for verificationpurposes, although that is counts towards the next problem's score.
  • Show the use(s) of SPIN to verify that there is a flaw and to determine what the flaw is. Briefly describe the flaw.
  • Fix the flaw in the code, and show either the fix or the resulting code. Again, include any code added for the next problem'sverification.
  • Show the use(s) of SPIN to verify your final implementation.

Hints: First, do not radically change the algorithm. There is a straightforward solution that only changes/addsa line or two. Second, do not overly serialize the code.Since the entry protocol's for loop is already serialized, this really means that each each process should be able to calculate max concurrently.

  • Shared variable declarations. /* Is Pi choosing a number? */ boolean choosing[n]; /* Pi's number, or 0 if Pi has none. */unsigned int number[n];
  • Global initialization.Occurs once, before any process attempts to enter its critical section. /* No process has a number. */ for all j{0,,n-1} number[j]= 0;
  • Critical section entry protocol, for process i . I.e. , each process has the following code immediately before its critical section. /* Choose Pi's number. */ choosing[i]= true; number[i]= max(number[0],number[1],,number[n-1]) + 1;choosing[i] = false;/* For all other processes,*/ for all j{0,,i-1, i+1,,n-1} in some serial order /* Wait if the other process is currently choosing. */while (choosing[j]) /* nothing */ ;/* Wait if the other process has a number and comes ahead of us. */ if ((number[j]>0)&&(number[j]<number[i]))while (number[j]>0) /* nothing */ ; Note that, because of the if 's test, it is equivalent to allow j to get the value i in this loop, as well. Although less intuitive, that simplifies the loop.
  • Critical section exit protocol, for process i . I.e. , each process has the following code immediately after its critical section. /* Clear Pi's number. */ number[i]= 0;

The problem with the given code is that the concurrent max computations does not necessarily result in each element of number[] being unique. Uniqueness is assumed by the following conditional toprioritize the processes:

if ((number[j]>0)&&(number[j]<number[i]))

One of the hints precludes changing the max calculation to produce uniqueness. So, we need a way to prioritize processes whenthey receive the same number. This is most easily accomplished by using their process IDs:

if ((number[j]>0)&&((number[j]<number[i]) ||((number[j] == number[i])&&j<i)))

Of course, j>i is also fine.

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?

Ask