Fairness

One of the main trends in recent developments in computer systems and programming languages is the inclusion of concurrency (or parallelism) and nondeterminism. Consequently, much recent research is devoted to the theory of these two modes of computation. A major direction within this theory is concerned with the semantics of programming languages expressing concurrency and nondeterminism and with verification of concurrent and nondeterministic programs. Among the new problems that the study of concurrency and nondeterminism encountered is that of fairness. This issue has revealed itself in many different contexts, as many facets of some very basic phenomenon. Some research directions, such as denotational semantics, had to solve some difficult mathematical problems (e.g. the power domain [PL 76, S 78, LE 76]); others, such as partial correctness proofs, needed some new insights (e.g. the discovery of noninterference [OG 76], [LA 77] and of cooperation [AFR 80], [LG 81] embodying relations among proofs). No research topic, however, raised controversy as much as the issue of fairness: Is it a “legitimate” (whatever that may mean) feature to be included in a programming language? Is it a “legitimate” area of study within computer science (as opposed to pure mathematics)?

The original proof method for termination of programs originated in [FL 67], for a family of flowchart-like programs, and it still underlies proof-methods for more elaborate kinds of programs. The basic idea is to associate some kind of a measure or ranking, with intermediate states of a computation, which decreases as the computation proceeds. The ranking has to be such that no infinite strictly decreasing sequence of ranks is possible. As a result, no infinite computation is possible.

We start by reviewing some of the basic notions involved. Then the original Floyd-method is explained in terms of a deterministic sub-language of GC, after which the method is extended to nondeterministic GC programs.

In this chapter we extend the use of direct well-foundedness arguments to prove termination of GC programs under a variety of scheduling policies for repeated choices among the guards of a repetitive statement.

In this chapter we present an alternative method for proving termination of GC programs under various fairness assumptions. The presentation is based on [AO 83] and [APS 84]. The main idea of this approach is the following: reduce the fair-termination problem of GC programs to ordinary (nondeterministic) termination of GC _R programs, an augmentation of GC with random assignments. A similar idea is mentioned also in [B 82] and [PA 81].

The aim of this chapter is to introduce extensions and generalizations of the previously studied concepts of fairness, in order to understand better both the scope of applicability and limitations of the proof methods for fair termination introduced. For these extensions and generalizations it is assumed that states may be augmented by auxiliary variables (and auxiliary assignments to them), by means of which it is possible to express properties of any prefix of the computation up to any given intermediate state occurrence.

We first study the property of equifair termination, a strengthening of fair termination imposing stronger restrictions on infinite computations, requiring infinitely many equalizations among sets of directions along infinite computations. In particular, we present proof rules for equifair termination for GC and prove their soundness and semantic completeness with respect to the semantics of computation trees. This is an attempt towards understanding properties of programs executed under a variety of restrictions on infinite behavior, a variety richer than the previously discussed fairness assumption, by means of a representative concept. The material in these sections is based on [GF 82] and [GFK 83]. Then we introduce the abstract notion of generalized fairness, relative to an arbitrary finite set of pairs of state conditions, and study termination under it, thereby generalizing both fairness and equifairness, as well of a whole family of related concepts. All these concepts have in common the property that they require similar proof methods for proving termination, and share a similar construction for completeness proofs. This section is based on [FK 83].

Then, we introduce the concept of extreme fairness, which requires yet stronger properties of the scheduler. Its main merit is its constituting a better approximation to probabilistic termination (termination with probability 1 when selection probabilities are attributed to directions). We present a proof rule for Extremely Fair Termination; however, it is not known whether this rule is complete for the strong version. The exposition is an adaptation of [PN 83] to our context and terminology.

The method of the helpful direction is applied to a language in which concurrency takes place among disjoint processes communicating by means of message passing. As mentioned before, the relativized version of the method is applied, as the language considered does not have the closure properties needed to reduce eventual occurrence of a condition to (fair) termination of a derived program. The main interesting new phenomena discussed are the impacts of simultaneity (in terms of joint enabledness) and overlapping computations due to concurrency, on fair termination. As a consequence, one can now formalize arguments which characterize behaviours such as the ability of a process to communicate a finite unbounded number of times and yet always terminate. The presentation basically follows [GFK 84].

The method of explicit schedulers is applied to a language in which concurrent processes communicate using shared variables. Such a language emphasizes mutual exclusion and not simultaneity. The main aspect treated is that of the transformations realizing fairness, taken from [OA 84].

The application of a particular method to a particular programming language is immaterial and both methods may be successfully applied to both languages. We decided to follow existing presentations. The reader should be able at this stage to figure out the details.

In both cases, it is found convenient to model concurrent executions of communicating processes by interleaving their atomic actions. Once fairness assumptions are included, the interleaving model is somewhat more satisfactory than in the case of arbitrary interleaving. Still, attempts are made also to capture a more “truly concurrent” model. Obviously, this distinction collapses if one is interested only in the state-transformation semantics of concurrent programs. Due to the possibility of using nondeterministic interleaving to model concurrency it became possible to use the successful tools for proving fair termination in a larger context.

In the previous chapters we described a variety of proof rules for proving fair termination. All these rules were described independently of any formal assertion language in which the various predicates needed for the proof might be expressed. In particular, the completeness proofs establish the existence of the sets of states needed without their representation by a formula in a calculus.

In this chapter we deal with the issue of syntactic expressibility in a formalized calculus. We introduce an assertion language, which we call L _μ , based on the (positive) μ-calculus and show that this language is sufficiently powerful for our needs. This language has already been used in the past to express predicates needed in termination proofs of recursive procedures [HP 73, deB 80].

The main concern is to show that in this calculus it is possible to express formally the weakest precondition for fair termination (fwp), characterizing the set of all the (initial) states for which no infinite fair computations of a given program exist. The first discussion of such a predicate transformer for weak fairness appears in [PA 81]; for unconditional and strong fairness we follow the ideas of [deR 81], and, mainly, of [SdeRG 84].

In this chapter a different pattern of reasoning is introduced, known as temporal-reasoning. It uses a notation which is directly interpreted on infinite sequences (or trees) which, in turn, can be used to represent the evolution in time of the program state. An important distinguished characteristic of this approach (as presented here) is its being endogenous, i.e. it considers the set of complete computation sequences (or trees) as given, and reasons directly about the behavior of the whole program.

Thus, given a program, the reasoning is factored as follows:

Another observation is that the temporal approach is rather more powerful for general liveness properties, of which termination is just a special case. Hence, in dealing with fair termination of GC programs, one does not take full advantage of the whole power of the system.

In this chapter we examine the fairness notions arising in the context of functional (or applicative) languages. As a representative language we have chosen Milner’s CCS (calculus for communicating processes) [M 80]. A similar formalism, with more primitive operators, which is also concerned with fairness, is that of Bergstra and Klop process algebra [BK 85]. There, the stress is more on the algebraic treatment.

Some new aspects of fairness are treated in the literature in the context of CCS. One notable difference from the assumptions in previous chapters is that dynamic networks are considered (i.e., with a changing number of processes and interconnections). This issue arises due to presence of recursion over concurrency, in contrast to using iteration (tail recursion) in the previously discussed languages.

Another new aspect arises due to the presence of a restriction (or hiding) operator, which forms a natural ground for distinguishing between structural fairness, based on the structure of the processes, and that of observable fairness, which restricts attention to observable communications only.

Though the issues raised in Chapter 5 regarding conspiracies (or their absence) apply to CCS as well, they were not explicitly treated in the literature in this context.

We mention here also that termination is not a central issue in CCS, hence the discussion is not focused on fair termination. Rather, the central issue is rules for fair behaviour. Thus, this chapter is concerned with generating fairness rather then with the consequences of assuming it. In this way, a metric characterization of fair CCS sequences is also discussed, closely following [C 85]. Finally, CCS turns to be a convenient tool for discussing (briefly) one other notion, that of finite delay as a primitive operator, which was mentioned in the introduction chapter as a fairness-like concept.