| << Chapter < Page | Chapter >> Page > |
We can modify the
Generalized Race Condition example to eliminate its race condition.
The lock controls access to the shared resource,
z .
1 /* Number of copies of the process to run. */
2 #define NUM_PROCS 33
4 show int z = 0;5 show bool locked = false;
67 active[NUM_PROCS] proctype increment()8 {
9 show int new_z;10
11 atomic {12 !locked ->/* Lock available? */
13 locked = true; /* Acquire lock. */14 }
1516 /* Critical section of code. */
17 new_z = z;18 new_z++;
19 z = new_z;20
21 locked = false; /* Release lock. */22 /* End critical section of code. */
23 }
As described before, when using a lock, we need to acquire thelock, execute the critical section, and release the lock. Releasing the lock is the final action of the critical section,as it allows another process to acquire the lock. To acquire the lock, clearly we need to check whether it is available.This guard is where each process potentially blocks, waiting for its turn to get the block.
The
atomic keyword,
as its name implies, makes a group of statements atomic.Without it, two processes
could first each determine the lock was available, then eachacquire the lock, defeating the purpose of the lock.
What values of
z are possible at the end of this program?
As desired, only the value 3, since there are 3 processes.
Run this code several times and observe its behavior.
Also, eliminate the
atomic keyword and its associated braces, and repeat.
Assume that the
atomic keyword
is removed, and there are only two processes, instead of three.Give a trace where both
are in the critical section at the same time.What are the differences in the state spaces with and without
the
atomic ?
The following figure shows one such trace.
Notice that
z is effectively incremented only once, instead of twice.
increment() , if
atomic keyword were removed.
For brevity, states show the line number for each process,the
z and
locked values, and
each process'
new_z value,
respectively.The critical difference in state spaces is that
the
atomic keyword prohibits
processes interleaving between the guard and its body.This reduces the size of the state space.
In this case, as in many others, it also reduces the numberof different end states and, thus, possible result values.
We now have the tools to demonstrate how a tiny server and its clients can be modeled. The server process is a loop that repeatedlywaits for and then processes requests. Clients send requests. For simplicity, in this example, the server won't communicateany results back to the clients, and the clients will only make one request each.
Servers generally allow multiple kinds of requests. Here, we'll
use one more new piece of Promela syntax,
mtype , to define some named
constants, similar to an enumerated type.
/* Number of each type of client. */
#define NUM_CLIENTS 1/* Define the named constants. */
mtype = {NONE, REQUEST1, REQUEST2};/* Declare a shared variable. */
show mtype request = NONE;active proctype server()
{do
:: request == REQUEST1 ->printf("Processing request type 1.\n");
request = NONE;:: request == REQUEST2 ->printf("Processing request type 2.\n");
request = NONE;od;
}active[NUM_CLIENTS] proctype client1(){
atomic{request == NONE ->request = REQUEST1;
}}
active[NUM_CLIENTS]proctype client2()
{atomic{
request == NONE ->request = REQUEST2;
}} 
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|