Appraising fairness in distributed languages

ABSTRACT

The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate for CSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully acceptable for a model with an n-way synchronization mechanism. Finally, the notion of fairness most often mentioned for Ada is shown to be fully acceptable.

REFERENCES

• 1: {AO} K.R. Apt, E.-R. Olderog, Proof rules and transformations dealing with fairness, SCP 3, pp. 65- i00, 1983.
• 2: {AC} K.R. Apt, Ph. Clermont, Two normal form theorems for CSP programs. IBM T.J Watson research Center RC I0975, July 1985
• 3: 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]
• 4: {BK-S2} RJ. Back and K. Kurki-Suonio, $cdalizability in distributed systems with handshaking, CMU TR 85-109, 1985.
• 5: Pierpaolo Degano , Ugo Montanari, Concurrent histories: a basis for observing distributed systems, Journal of Computer and System Sciences, v.34 n.2-3, p.422-461, April/June 1987 [doi>10.1016/0022-0000(87)90032-8]
• 6: {Fo} I. Forman, On the design of large distributed systems, ~oceedings of International Conference on Computer Languages, Miami Beach, Florida, October, 1986.
• 7: {Fr} N. Frmlcez, Fairness, Texts and monographs in computer science series (D. Gales, ed.), Springer-Verlag, New York, 1986.
• 8: {FdR} N. Francez and W. P. de Roever, Fairness in communicating processes, unpublished memo, Computer Science Dept., Utrecht University, July 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: Orna Grumberg , Nissim Francez , Shmuel Katz, Fair termination of communicating processes, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.254-265, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806752]
• 11: Orna Grumberg , Nissim Francez , Johann A. Makowsky , Willem P. de Roever, A proof rule for fair termination of guarded commands, Information and Control, v.66 n.1-2, p.83-102, July/Aug. 1985 [doi>10.1016/S0019-9958(85)80014-0]
• 12: {H} C.A.R. Home, Communicating sequential processes, CACM 21, 8, August 1978.
• 13: {HLP} W. Hennessey, Wei-Li, G. Plotldn, Semantics for Ada tasks, proceedings of TC.2 Working conference on the formal description of programming concepts, Garmisch Partenkirchen (D. Biomer, ed.), North Holland, 1983.
• 14: {KdR} R. Kuiper and W.P. de Roever, Fairness assumptions for CSP in a temporal logic framework, proceedings of TC.2 Working conference on the formal description of programming concepts, Garmisch Partenkirchen OD. Biomer, ed.), North Holland, 1983.
• 15: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 16: {L2} L. Lamport, What good is temporal logic?, proceedings of IPIP 9th world congress, Paris, France, September 1983.
• 17: 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
• 18: {OA} E.-R. Olderog, K.R. Apt, Fairness in parallel programs, the transformational approach, TR 86-I 1, Univ. of Kiel, 1986 (submitted for publication).
• 19: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 20: {P} G.D. Plotlfin, An operational semantics for CSP, proceedings of TC.2 Working conference on the formal description of programming concepts, Garmisch Partenkirchen (D. Biorner, ed.), North Holland, 1983.
• 21: {PdR} A. Pnueli and W,P. de Rocver, Rendezvous with Ads: a proof-theoretic view, RUU-CS-82-12, University of Utrecht, July 1982. Also in: proceedings of the AdaTec conference, Crystal City, 1982.
• 22: 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
• 23: {RS} J. Reif, P. Spirakis, Probabilistic bidding gives optimal distributed resource allocation, TR, Aiken Computation Lab, July 1983.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Alternation and nondeterminism; Parallelism and concurrency
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Algorithms, Languages, Theory