Concurrency: State Models and Java Programs

The terms safety and liveness applied to concurrent programs were first introduced by Lamport (1977). In this book, we have adopted a modeling approach to reasoning about concurrent programs and consequently a model-checking approach to verifying properties. As discussed at the end of Chapter 5, an alternative approach is to reason about safety properties of concurrent programs using assertions and invariants specified in predicate logic. The reader should consult Greg Andrews’ book (1991) for an extensive exposition of this approach.

The mechanisms used in this chapter for checking safety and progress properties have been developed by the authors and their colleagues. The safety property technique is due to Cheung and Kramer (1999). Progress checking as described here is due to Giannakopoulou, Magee and Kramer (1999) and is a simplified form of a more general technique for checking that properties specified in Linear Temporal Logic (LTL) hold for a system. The property that our approach checks is that an action always eventually occurs. As an LTL formula, this is specified as ☐ a, where ☐ means always and means eventually. The general technique involves translating the LTL formula into Büchi automata and then composing the Büchi automata with the target system and performing a connected component analysis of the resulting automata (Gribomont and Wolper, 1989). Technically, this is a check that the system is a valid model of the formula – the origin of the term model checking, which we have used in the looser sense to refer to any technique for analyzing models. Büchi automata are a form of finite state automata which recognize infinite sequences of actions. The interested reader should look at Holzmann’s SPIN model checker (Holzmann, 1991, 1997) which uses this approach. The pioneering work on model checking is due to Clarke, Emerson and Sistla (1986). Fred Schneider (1997) provides an introduction to temporal logic and discusses derivation and reasoning about concurrent programs.

Chapter 14 provides more details on the use of LTL for property checking, and introduces fluents to FSP as a means of specifying state-based properties in an event-based formalism such as LTS. Fairness and the use of Büchi automata are also discussed and supported by LTSA for property checking.

The topic of fairness in concurrent programs has an extensive literature. We have used a strong form of fair choice. For an extensive discussion on the different classes of fairness, see the book by Francez (1986).