| << Chapter < Page | Chapter >> Page > |
Since we have not fully specified this example's original system, we will leave the details to the reader's imagination.
In 1997, the Mars Pathfinder seemed to beam its data back to Earth just fine, exceptsometimes it would appear to freeze up. Thefix? Press Control-Alt-Delete from Earth, and re-boot its rover(incurring not only an expensive delay for Mission Control, but the full attention of late-night-TV comedians).
The cause turned out to be a bug in the concurrency protocol, between a low-priority data-gathering mode, which was meantto yield to a high-priority data-sending mode. However, sometimes these priorities would become inverted,with the high-priority thread blocking on the (supposedly) low-priority one. (More detail.) The bug
1 /* From Spin primer/manual, Gerard Holzman. */
23 mtype = { free, busy }; /* states for the variable "mutex" */
4 mtype = { idle, waiting, running } /* states for the processes */5
6 mtype highProc = idle;7 mtype lowProc = idle;
8 mtype mutex = free;9
10 active proctype high_priority()11 {
12 end:13 do
14 :: highProc = waiting;15 atomic {
16 mutex == free ->17 mutex = busy
18 };19 highProc = running;
20 /* work work work; produce data */21 atomic {
22 highProc = idle;23 mutex = free
24 }25 od
26 }27
28 active proctype low_priority() provided (highProc == idle)29 {
30 end:31 do
32 :: lowProc = waiting;33 atomic {
34 mutex == free ->35 mutex = busy
36 };37 lowProc = running;
38 /* work work work; consume data and send it back to Earth. */39 atomic {
40 lowProc = idle;41 mutex = free
42 }43 od
44 }45
4647 /* Note the "provided" clause as part of low_priority()'s declaration.
48 * This condition is monitered and confirmed before every single49 * transition that low_priority() attempts.
50 * (This is a handier syntax than placing that guard condition51 * in front of every single statement within the process.)
52 */
Can you detect the problem using SPIN?
As described previously , livelock is very similar to deadlock. But in livelock, computation doesn't get completely stuckit simply doesn't do anything sufficiently interesting.
In previous examples, processes waited with a guarded statement.
Here, as an example of
busy waiting ,
we repeatedly check for thedesired condition, and otherwise do something.
Busy waiting for a condition that never comes true is one commonsituation that leads to livelock.
1 show int x = 1;
23 active[2] proctype busywait()4 {
5 do6 :: x != 0 ->7 printf( "%d waiting.\n", _pid );
8 :: else ->9 break;
10 od;11
12 printf( "Now this is more interesting.\n" );13 } This example also uses
_pid , a read-only variable
whose value is the process ID number (0-based) of the given process.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|