| << Chapter < Page | Chapter >> Page > |
You might have noticed that this example (unlike earlier ones)
only has each process perform their critical section once.No problem, we can put that in a
do loop:
1 /* An overflow bug sneaks into our Mutual exclusion, uh-oh!
2 * Lamport's "Bakery algorithm"3 * Procs which communicate only through ticket[].4 */
56 byte ticket[2];7 int data = 0;
89 active [2] proctype customer()10 {
11 pid me = _pid;12 pid peer = 1-_pid;
1314 do
15 :: skip; /* Doing some non-critical work... */16
17 ticket[me]= 1; /* Declare desire to enter crit section. */18 ticket[me] = ticket[peer]+1;
19 ((ticket[peer]== 0) || (ticket[me]<ticket[peer])) ->20
21 /* Entering critical section. */22 data++;
23 assert (data == 1);24 data--;
25 /* Leaving critical section. */26
27 ticket[me]= 0; /* Relinquish our ticket-number. */
28 od;29 } SPIN verifies thiwait a moment, the verification fails!
And at depth 2058, no less.What's going on?
A clue can be found in scrutinizing the output:
spin: line 17 "mutexG2.pml", Error: value (256->0 (8)) truncated in assignment Our variable
ticket , a
byte ,
is overflowing!
ticket can keep incrementing until overflow.ticket from
byte to
int changes nothing conceptually,
it
does change SPIN's verification.
Re-run the verification with this change.What is the difference?ticket =1 and enter
its critical section.While there, P2 takes
ticket =2,
blocking until P1 is done.Then P2 enters its critical section, but before
P2 finishes P1 again requests its critical section,taking
ticket =3.
This process repeatseach process requesting
the criticalsection (and bumping up the
ticket number)
before its peer finishes.ticket number
(intentionally) drops back to zero.byte :
there is no conceptual difference in the verification errorsbetween using
byte and
int ,
but by keeping the state space from being extraneously large,we get better insight to what the difficulty was.
(Imagine if we'd used
int firstwe might
have seen the state-space error, presumed that other parts ofour program made verification infeasible, crossed our fingers
and given up.)
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|