Chapter 7: Safety and Liveness Properties

Overview

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 are chosen for execution.

This chapter explains how we can analyze the finite state models of concurrent systems for both safety and liveness problems. The example of cars crossing a single-lane bridge is used to focus discussion. We then analyze a number of implementations of read/write locks. Read/write locks allow many processes to access a shared resource at the same time for read access, but require write access to be mutually exclusive. They occur in many concurrent programs.