Download Formal Methods for System Development

Chapter 4. Spin introduction and tutorial
inline allocate (pri) {
takemutex(mutex);
if
:: busy ->
givemutex(mutex);
wait(cond[pri]);
:: else
fi;
busy = true;
givemutex(mutex);
}
Figure 4.7: The allocation function for the resource controller example.
mutex is locked, we assert that the variable busy is true, else something has
gone wrong. Then busy is set to false and a search for the next User in line
is started. If there are no one waiting for the resource the mutex is released.
inline deallocate () {
takemutex(mutex);
assert(busy);
busy = false;
if
:: nempty(cond[0].queue) ->
post(cond[0])
:: empty(cond[0].queue) ->
if
:: nempty(cond[1].queue) ->
post(cond[1])
:: empty(cond[1].queue) ->
givemutex(mutex)
fi
fi
}
Figure 4.8: The deallocation function for the resource controller example.
The strong semaphore operations are not as easy as the busy-wait operations we have used earlier. We declare a new type, Semaphore, that has a
count and a queue:
typedef Semaphore {
byte count;
chan queue = [8] of {byte}
}
We model the queue as an asynchronous channel. The channel must hold
as many bytes as we have processes that access that particular semaphore.
It is no real harm in overestimating, as the model will behave correctly.
54