| << Chapter < Page | Chapter >> Page > |
If we run SPIN's verifier on the code for the Tiny Server and Clients example , we get a spuriousinvalid end stateerror, since we expect the client to be alive and listening forfor any more requests.
To let SPIN know that is acceptable and shouldn't actually
be considered deadlock, we label the beginning ofthe server loop as being a valid end state:
We give it a label whose first threeletters are
end , as shown below.
Run the verifier again on this, and there shouldbe no error message.
1 /* Number of each type of client. */
2 #define NUM_CLIENTS 13
4 /* Define the named constants. */5 mtype = {NONE, REQ1, REQ2};
67 /* Declare a shared variable. */
8 show mtype request = NONE;9
10 active proctype server()11 {
12 /* Waiting for a request is a valid place to end. */13 endwait:
14 do15 :: request == REQ1 ->16 printf("Processing request type 1.\n");
17 request = NONE;18 :: request == REQ2 ->19 printf("Processing request type 2.\n");
20 request = NONE;21 od;
22 }23
24 active[NUM_CLIENTS]proctype client1()
25 {26 atomic {
27 request == NONE ->28 request = REQ1;
29 }30 }
3132 active[NUM_CLIENTS] proctype client2()33 {
34 atomic {35 request == NONE ->36 request = REQ2;
37 }38 }
More formally, what this does is to tag some of the states in the state space as being valid, if they happen tobe an end-state.
endwait label
makes the bottom two states be valid end states.Putting the
end label in front of the entire
do statement may not seem as natural to you as:
do
::end1:
request == REQ1 ->::
end2:request == REQ2 ->od; However, this is
not acceptable!
Try it, by entering the changes and running a syntax check.The problem is that
end1 and
end2 both represent the same program point, where the program
waits for some guard to become true.It would be nonsensical to have (say) one of the two guards
labeled an end-state without the other one being an end-state.To prevent surprising inconsistencies, Promela disallows
labels in front of individual guards of a compound statement.
There are other syntactic restrictions of where labels can appear.
The most commonly encountered is that they cannot appearat the end of a statement block. For example, instead of
{
x = 1;y = 2;
label: /* Label not allowed here. */} you can introduce a dummy statement, and label it:
{
x = 1;y = 2;
label:skip; /* A statement that does nothing. */
}
It's worth showing several examples of correct and incorrect concurrentprograms, and how SPIN can implement and attempt to verify them. We'll examine a sequence of programs, all dealing with mutualexclusion protocols. We hope to leave the gentle reader with an appreciation ofthe non-obvious nature of concurrent bugs (and hence the value of automated verification).
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|