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.