Appraising fairness in languages for distributed programming. (English) Zbl 0659.68023

Apt, Krzysztof R.; Francez, Nissim; Katz, Shmuel

Distrib. Comput. 2, No. 4, 226-241 (1988).

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. These notion of fairness most often mentioned for Ada is shown to be fully acceptable. For a model with nonblocking ‘send’ operations, some variants of common fairness definitions are appraised, and two are shown to satisfy the suggested criteria.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68N25	Theory of operating systems

Keywords:

communicating sequential processes; partial order semantics; distributed computation; fairness; semantic criteria; CSP; synchronization

References:

[1]	[ABC] Apt KR, Bougé L, Clermont P (1987/88) Two normal form theorems for CSP programs. Inf Proc Lett 26: 165–171 · Zbl 0631.68026
[2]	[AFK] Apt KR, Francez N, Katz S (1987) Appraising fairness in languages for distributed programming. Proc of 14th ACM-POPL Symp, Munich, West Germany (January 1987) · Zbl 0659.68023
[3]	[AO] Apt KR, Olderog ER (1983) Proof rules and transformations dealing with fairness. Sci Comp Prog 3:65–100 · Zbl 0512.68014
[4]	[AF] Attie P, Francez N (1988) Fairness and hyperfairness in multiparty interactions. MCC-STP Tech Rep (July 1987) · Zbl 0797.68100
[5]	[BK-S 1] Back RJ, Kurki-Suonio K (1983) Decentralization of process nets with centralized control. Proc of 2nd ACM-PODC Symp, Montreal (August 1983)
[6]	[BK-S 2] Back RJ, Kurki-Suonio K (1985) Serializability in distributed systems with handshaking. CMU Tech Rep, pp 85–109
[7]	[BF] Bougé L, Francez N (1988) A compositional approach to superimposition. Proc of 15th ACM-POPL Symp. San Diego, California (January 1988)
[8]	[D] Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18:453–467 · Zbl 0308.68017
[9]	[DM] Degano P, Montanari U (1988) Concurrent histories, a basis for observing distributed systems (to appear in J Comp Syst Sci) · Zbl 0619.68017
[10]	[Fo] Forman I (1986) On the design of large distributed systems. Proc of Int Conf on Comp Lang, Miami Beach, Florida (October 1986)
[11]	[Fr] Francez N (1986) Fairness. In: Gries D (ed) Texts and monographs in computer science series. Springer, New York
[12]	[FdR] Francez N, de Roever WP (1980) Fairness in communicating processes (unpublished memo) Computer Science Department, Utrecht University (July 1980)
[13]	[FK] Francez N, Katz S (1988) Fairness and the axioms of control predicates. To appear in Int J Parallel Programming
[14]	[GdR] Gerth RT, de Roever WP (1984) A proof system for concurrent Ada programs. Science of Computer Programming, vol 4, no 2, pp 159–204 · Zbl 0536.68009
[15]	[GFK 1] Grumberg O, Francez N, Katz S (1986) A complete rule for equifair termination. J Comp Syst Sci 33:313–332 · Zbl 0612.68021
[16]	[GFK 2] Grumberg O, Francez N, Katz S (1984) Fair termination of communicating processes. Proc of 3rd ACM-PODC Symp, Vancouver (August 1984)
[17]	[GFMdR] Grumberg O, Francez N, Makowsky J, de Roever WP (1985) A proof rule for fair termination of guarded commands. Inf Control 66:83–102 · Zbl 0577.68022
[18]	[H] Hoare CAR (1978) Communicating sequential processes Commun ACM 21:666–677 · Zbl 0383.68028
[19]	[HLP] Hennessey W, Wei-Li, Plotkin GD (1983) Semantics for Ada tasks. In: Björner D (ed) Proceedings of TC.2 Working Conference on the Formal Description of Programming Concepts, Garmisch Partenkirchen. North Holland
[20]	[K] Katz S (1987) A superimposition control construct for distributed systems. MCC-STP Tech Rep STP-268-87
[21]	[KP] Katz S, Peled D (1987) Interleaving set temporal logic. Proc of 6th ACM-PODC Symp, Vancouver, Canada (August 1987) · Zbl 0718.03014
[22]	[KdR] Kuiper R, de Roever WP (1983) Fairness assumptions for CSP in a temporal logic framework. In: Björner D (ed) Proceedings of TC.2 Working Conference on the Formal Description of Programming Concepts, Garmisch Partenkirchen, North Holland · Zbl 0512.68022
[23]	[L 1] Lamport L (1978) Time, clocks, and the ordering of events. Commun ACM 21: 558–566 · Zbl 0378.68027
[24]	[L 2] Lamport L (1983) What good is temporal logic? Proc of 9th IFIP Cong, Paris, France (September 1983)
[25]	[LPS] Lehmann D, Pnueli A, Stavi J (1981) Impartiality, justice, and fairness: the ethics of concurrent termination. In: Kariv O, Even S (eds)] Proc of 8th ICALP, Acco, Israel (July 1981) LNCS 115. Springer Berlin Heidelberg New York, pp 264–277 · Zbl 0468.68026
[26]	[OA] Olderog ER, Apt KR. (1988) Fairness in parallel programs, the transformational approach (to appear in ACM Toplas)
[27]	[OL] Owicki SS, Lamport L (1982) Proving liveness properties of concurrent programs. ACM Trans Prog Lang Syst 4(3):455–495 · Zbl 0483.68013
[28]	[P] Plotkin GD (1983) An operational semantics for CSP. In: Björner D (ed) Proceedings of TC.2 Working Conference on the Formal Description of Programming Concepts, Garmisch Partenkirchen. North Holland · Zbl 0512.68012
[29]	[PdR] Pnueli A, de Roever WP (1982) Rendezvous with Ada: a proof-theoretic view. Proceedings of the AdaTec Conference, Crystal City
[30]	[R] Reisig W (1984) Partial order semantics versus interleaving semantics and its impact on fairness. Proc 11th ICALP, Antwerp, 1984 · Zbl 0597.68019
[31]	[RS] Reif J, Spirakis P (1983) Probabilistic bidding gives optimal distributed resource allocation. Aiken Computation Lab Tech Rep, Harvard University (July 1983) · Zbl 0579.68017