Fair termination of communicating processes

ABSTRACT

Fairness has become one of the main issues in the theory of non-determinism and concurrency. Recently, the problem of proof rules for fair termination of programs (and some of its variants) has attracted considerable attention ([AO83], [APS82], [GFK83], [GFMR81], [LPS81], [P83]). However, 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. The main reason for this is the elegance of formalisms for structured nondeterminism, such as Guarded Commands [DIJ76], and their convenience for syntax directed proofs. Other attempts use transition-systems as the program model, and temporal logic as the underlying reasoning formalism ([QS82], [P83]), thereby giving up the structured, syntax-directed, approach. A phenomenon inherently related to fairness is that of “unbounded nondeterminism”, whereby a program can produce an infinite set of final outcomes and yet always terminate. Such a behaviour is attributed to random assignments [AP83]. Thus, a classical example of a fairly terminating nondeterministic program is a “random (natural) number' generator”. The presence of unbounded nondeterminism forces the use of countable ordinals (higher than &ohgr;) in proofs of fair termination appealing directly to well-foundedness arguments.

REFERENCES

• 1: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 2: K.R. Apt, E.R. Olderog, "Proof rules and transformations dealing with fairness", Science of Computer Programming 3, 1983.
• 3: K.R. Apt, A. Pnueli and J. Stavi, Fair termination revisited with delay, TR 82-51, LIPT, University of Paris, October 1982. Also in: Proc. 2nd Conference of Foundations of Software Technology and Theoretical Computer Science (FST-TCS), Bangalore, India, December 1982. To appear in TCS.
• 4: R. J. R. Back , R. Kurki-Suonio, Decentralization of process nets with centralized control, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.131-142, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806716]
• 5: R.J.J. Back, K. Kurki-Suonio, Cooperation in distributed systems using symmetric multi-process handshakes, TR University of Helsinki, 1983.
• 6: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 7: Nissim Francez , Dexter Kozen, Generalized fair termination, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.46-53, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800515]
• 8: N. Francez and W.P. de Roever, "Fairness in communicating processes", manuscript, 1980.
• 9: Orna Grumberg , Nissim Francez , Shmuel Katz, A Compete Proof Rule for Strong Equifair Termination, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.257-278, June 06-08, 1983
• 10: O. Grumberg, N. Francez, J.A. Makowsky and W.P. Roever, "A proof rule for fair termination of guarded commands", Proceedings of the Int. Symposium on Algorithmic Languages, Amsterdam, October 1981, North-Holland, 1981.
• 11: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 12: David Harel, A general result on infinite trees and its applications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.418-427, December 1984 [doi>10.1145/800057.808708]
• 13: R. Kuiper and W.P. de Roever, "Fairness assumptions for CSP in a temporal logic framework", IFIP-TC2 Working Conference on formal description of programming concepts, Germisch, 1982.
• 14: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 15: Amir Pnueli, On the extremely fair treatment of probabilistic algorithms, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.278-290, December 1983 [doi>10.1145/800061.808757]
• 16: Wolfgang Reisig, Partial Order Semantics versus Interleaving Semantics for CSP-like Languages and its Impact on Fairness, Proceedings of the 11th Colloquium on Automata, Languages and Programming, p.403-413, July 16-20, 1984
• 17: J.P. Queille, J. Siffakis, "A temporal logic to deal with fairness in transition systems", Proceedings of FOCS Conference (IEEE), 1982.
• 18: Aravinda Prasad Sistla, Theoretical issues in the design and verification of distributed systems, 1983

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Alternation and nondeterminism

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: CSP

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Partial evaluation

General Terms:
Algorithms, Languages, Verification