Liveness and Fairness
This note is devoted to liveness and progress properties. They are properties stating intuitively that “something good will eventually happens”. For instance, the absence of starvation for any of the dining philosophers in [1] is a liveness property and so is the possibility of being allowed to copy in the printer and scanner example also presented in [1].
We shall see how progress and liveness properties can be specified in the recursive extension of HML [1], however as it turns out, these kind of properties we must specify using minimal fixed points instead of as for safety properties using the maximal fixed points.
For illustration purposes, we shall use the classical example of readers and writers as our running example.
The examples of models to be run in MWB in this note are presented with emphasis on readability and may thus not compile due to extra line breaks.
References
[1] J.C. Godskesen. Deadlocks and safety properties (version 1.2), 2005. Teaching notes, IT University of Copenhagen.
[2] B. Victor. The mobility workbench user’s guide, polyadic version 3.122. Technical report, SICS, Stockholm, Sweden, 1995.
Monitors and Semaphores
So far we talked about synchronization through shared objects and the interference problem. Mutual exclusion solves the problem! Monitors and semaphores may help to obtain mutual exclusion. In this note we explain the concepts of semaphores and monitors.
The examples of models to be run in the Mobility Workbench (MWB) in this note are presented with emphasis on readability and may thus not compile due to extra line breaks.
Part of this note and some of the examples in this note are inspired by [1].
The exercises affiliated with this lecture are to be found in Section 6
References
[1] J. Magee and J. Kramer. Concurrency — State Models & Java Programs. Worldwide Series in Computer Science. JohnWiley & Sons, 1999.
