Concurrency: State Models and Java Programs

Chapter 7. Safety and Liveness Properties

A property is an attribute of a program that is true for every possible execution of that program. Properties of interest for concurrent programs fall into two categories: safety and liveness. A safety property asserts that nothing bad happens during execution. A liveness property asserts that something good eventually happens. Another way of putting this is that safety is concerned with a program not reaching a bad state and that liveness is concerned with a program eventually reaching a good state.

In sequential programs, the most important safety property is that the final state is correct. We have already seen that for concurrent programs, important safety properties are mutual exclusion and the absence of deadlock. In the previous chapter, we determined that deadlock is generally a bad state from which no further actions can be executed. In Chapter 4, we saw that allowing more than one process to access a shared variable resulted in interference and thus incorrect or bad states.

The most important liveness property for a sequential program is that it eventually terminates. However, in concurrent programming, we are frequently concerned with systems that do not terminate. In this chapter, we primarily deal with liveness issues relating to resource access: are process requests for shared resources eventually granted? We will see that liveness properties are affected by the scheduling policy that determines which of a set of eligible actions ...