Skip to main content

Über dieses Buch

The main purpose of this book is to bring together much of the research conducted in recent years in a subject I find both fascinating and impor­ tant, namely fairness. Much of the reported research is still in the form of technical reports, theses and conference papers, and only a small part has already appeared in the formal scientific journal literature. Fairness is one of those concepts that can intuitively be explained very brieft.y, but bear a lot of consequences, both in theory and the practicality of programming languages. Scientists have traditionally been attracted to studying such concepts. However, a rigorous study of the concept needs a lot of detailed development, evoking much machinery of both mathemat­ ics and computer science. I am fully aware of the fact that this field of research still lacks matu­ rity, as does the whole subject of theoretical studies of concurrency and nondeterminism. One symptom of this lack of maturity is the proliferation of models used by the research community to discuss these issues, a variety lacking the invariance property present, for example, in universal formalisms for sequential computing.



Chapter 0. Introduction

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)?
Nissim Francez

Chapter 1. Termination and Well-Foundedness

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.
Nissim Francez

Chapter 2. The Method of Helpful Directions

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.
Nissim Francez

Chapter 3. The Method of Explicit Scheduler

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 reduction method is such that it uses random-assignment (of natural numbers) to explicitly represent the fair scheduler within the program. Once this transformation is carried out, the resulting nondeterministic program will have a variant decreasing along every direction whenever the original program is fairly terminating. Finally, the effect of the transformation is simulated within a proof rule, which now serves for proving properties of the original, untransformed, program.
Nissim Francez

Chapter 4. Extension and Generalizations of Fairness

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.
Finally, we consider another modification of the fairness concept, whereby the focus is shifted from fair selection of directions to fair reachability of predicates, following [QS 83].
Nissim Francez

Chapter 5. Fair Termination of Concurrent Processes

Though the main interest and motivation for the consideration of fair termination stems from concurrency, almost all of the recent results are formulated in terms of nondeterministic programs, as discussed in previous chapters. The main reason for this is the elegance of formalisms for structured nondeterminism, such as Guarded Commands. In this chapter, we present extensions of the methods to concurrency, trying to preserve as much as possible the structured approach.
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.
Nissim Francez

Chapter 6. Syntactic Expressibility

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].
The version of the μ-calculus used is augmented with (constants denoting) all the recursive ordinals, an odering relation (on ordinals) and the characteristic predicate for the closing ordinal (of a structure). A similar language is used also by [AP 82] in the context of random assignments. A source book for the mathematics of monotone operators and inductivity is [MO 74].
Nissim Francez

Chapter 7. Fairness in Temporal Logic

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:
define the set of all its computation histories,
prove any required property in terms of these histories, independently of the program.
This may be contrasted with the exogenous approach of the proof rules in previous chapters, where the rules related properties of the whole program to properties of its parts.
One consequence of this distinction is that the temporal approach is more suitable for dealing with programs presented as transition systems in contrast to the exogenous systems, that fit nicely in dealing with well-structured programs. Recently several attempts were made to provide temporal semantics in a more structured, compositional way.
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.
Nissim Francez

Chapter 8. The Functional Approach

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.
The presentation follows closely the main work on fairness in CCS, namely [CS 85].
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.
Nissim Francez


Weitere Informationen