| << Chapter < Page | Chapter >> Page > |
Previously ,
we claimed that adding a lock fixed the racecondition of the previous example. Let's now verify that claim.
The following is the locking version of the code augmented withthe same assertion code just used.
Note that the assertion needs to be inside the critical section.(Otherwise, process B could execute its critical section, changing
z ,
in between process A's critical section and its assertion.)
/* Number of copies of process to run. */
#define NUM_PROCS 3show int z = 0;
show bool locked = false;active[NUM_PROCS] proctype increment(){
show int new_z;/* A saved copy of the old z, for the assertion. */
show int old_z;atomic {
!locked ->/* Lock available? */
locked = true; /* Acquire lock. */}
/* Critical section of code. */old_z = z;
new_z = old_z + 1;z = new_z;
assert(z == old_z+1);locked = false; /* Release lock. */
/* End critical section of code. */} Run the verification as before. As expected, no errors are found.Happily, this time no error messages are reported before the version informationin the "Verification Output" window, and SPIN doesn't suggest any guided simulation.
A previous exercise asked you to write a small deadlocking program,
and provided one solution.Running such a program in SPIN's simulation
mode, some execution paths result in deadlock,
Run SPIN's verifier on your tiny deadlocking program.
The deadlock is reported by a somewhat obscure error message:
pan: invalid end state (at depth 0)
pan: wrote pan_in.trail As usual,
xspin allows
you to easily run the guided simulation it found.
Deadlock occurs in a state when nothing further will happenthat is, there are no outgoing edges in the state space.We call this an end state . Most programs we've seen previously have a valid end state: all processes complete their last line.In contrast, in deadlock we are in an end state, yet at least one process hasn't completed.Henceinvalid. SPIN checks for end states bysearching the entire state space (either by a depth- or breadth-first search).
We've mentioned that valid end states are those where every process has completed its last line,and that deadlock ends with at least one process which hasn't completed.However, that's not enough to conclude deadlock: sometimes it is desirable to have a trace reach an end-statewith a process still (say) waiting for more input. Consider a server and its clients.By default, the server waits and does nothing. Only when a client makes a request, the server responds and does something.If all clients exit, it is expected, not an error, for the server to be blocked waiting for another request.In SPIN, we need to notate that it is valid for the server to end at that point, and not actually deadlock.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|