On Fairness Notions in Distributed Systems
II. Equivalence-Completions and Their Hierarchies∗
Yuh-Jzer Joung†
Department of Information Management, National Taiwan University, Taipei 106, Taiwan
E-mail: [email protected] Received October 4, 1996
This is the second part of a two-part paper in which we discuss the implementability of fairness
notions in distributed systems where asynchronous processes interact via multiparty interactions. We
focus here on equivalence-robust fairness notions where equivalence computations are either all fair or all unfair. Francez et al. (1992, Formal Aspects Comput. 4, 582–591) propose a notion of completion to transform a non-equivalence-robust fairness notion to an equivalence-robust one while maintain-ing several properties of the source. However, a completion may not preserve strong feasibility—a necessary and sufficient condition for a completion to be implementable. In this paper, we study the system requirement for a completion to be strongly feasible and determine the strongest imple-mentable completion for every given fairness notion. Moreover, for most systems we obtain a fairness notion, which we refer to as SG+, such that SG+is the strongest fairness notion that is both imple-mentable and equivalence-robust. We also provide a comprehensive comparison of SG+and several well-known fairness notions and their minimal and maximal completions. Finally, we show that if equivalence-robustness is dropped, then in general it is impossible to define a fairness notion that is implementable and stronger than all other implementable fairness notions, unless the system consists of only one interaction. This implies plenty of leeway in the design of fairness notions suitable for various applications. °C2001 Academic Press
INTRODUCTION
This is the second part of a two-part paper in which we discuss the implementability of fairness notions in distributed systems where asynchronous processes interact via multiparty interactions. In Part I [5] we have presented a necessary and sufficient criterion for determining the implementability of fairness notions. We focus here on equivalence-robust fairness notions where equivalent computations are either all fair or all unfair.
1. EQUIVALENCE-ROBUSTNESS AND COMPLETIONS
Intuitively, equivalence-robustness ensures that different observations of the same partial-order com-putation obtain the same property of the system [6]. It thus serves as a natural bridge over the gap between interleaving semantics and partial-order semantics, which is highly desirable in distributed languages [3]. Furthermore, as we have shown in Part I, under strong feasibility equivalence-robustness suffices to guarantee the implementability of a fairness notion.
As it turns out, however, several important fairness notions are strongly feasible but are not equivalence-robust. For example, consider the notion of strong interaction fairness (SIF), which re-quires an interaction that is infinitely often enabled to be executed infinitely often. Assume a systemIS with three interactions x12, x13, and x24depicted in Fig. 1, where x12involves p1and p2, x13involves p1 and p3, and x24involves p2and p4. SIF is strongly feasible for the system because a nonblocking sched-uler satisfying SIF can be constructed by always choosing as the continuation the enabled interaction that is executed the least often; tie is broken arbitrarily. Then the computationπ = (p1p3x13p2p4x24)ω ∗A preliminary version of this paper appeared as Y.-J. Joung, 1996, On strong feasibilities of equivalence-Completions, in
“Proceedings of the 15th Annual ACM Symposium on Principles of Distributed Computing,” Philadelphia, PA, pp. 156–165. This research was supported by the National Science Council, Taipei, Taiwan, Grants NSC 85-2213-E-002-059 and NSC 86-2213-E-002-053, and by the 1997 Research Award of College of Management, National Taiwan University.
† The author is currently visiting Laboratory for Computer Science, Massachusetts Institute of Technology (1999–2000).
35
0890-5401/01 $35.00 Copyright°C2001 by Academic Press
FIG. 1. A system of four processes p1, p2, p3, and p4and three interactions x12, x13, and x24.
satisfies SIF, but its equivalent computationψ = (p1p3p2x13p4x24)ω does not because x12 is now enabled in every state immediately after p2is ready but it is never executed.
Francez et al. [3] propose a notion of completion to transform a non-equivalence-robust fairness notion to an equivalence-robust one while maintaining most properties of the source. To understand completions, consider Fig. 2. In this figure, run(IS) denotes the set of all possible computations of a systemIS, while C(IS) denotes the set of computations allowed by a fairness notion C. Each partition represents an equivalence class induced by the equivalence relation considered above by permuting independent actions. Of these equivalence classes, Xi’s are said to be purely fair because they are
contained inC(IS), while Yj’s are purely unfair because they do not intersectC(IS). The classes Zk’s
are mixed as they contain both fair and unfair computations. A completion has to resolve the fairness of the mixed classes. Thus, the minimal completion (i.e., the strongest completion) can be obtained by treating all mixed classes as unfair, whereas the maximal completion (i.e., the weakest completion) can be obtained by treating all mixed classes as fair. A semantic comparison of the two can be found in [3]. In general, fewer liveness properties can be assumed for programs using the weakest completion, while the strongest completion has exactly the opposite characteristics.
Unfortunately, a completion may not necessarily preserve strong feasibility, meaning that it may not even be implementable. To see this, consider again the system shown in Fig. 1. The computation
π = (p1p3x13p2p4x24)ω
is inevitable to all strongly feasible fairness notions ofIS, meaning that they must consider π as fair. This is because at any point of the computation at most one interaction is enabled. Thus according to the strong feasibility criterion, when only one interaction is enabled, there must be a continuation allowing the interaction to be executed. (Otherwise the system could be deadlocked if, say when x13is enabled, the scheduling algorithm chooses to wait for more interactions to be enabled while p2and p4 instead are busy doing their local actions forever.) So any completion of SIF, e.g., the minimal completion, that excludes the equivalence class ofπ would not be strongly feasible.
In this paper we determine, for any given fairness notionC, the strongest strongly feasible completion ofC. Recall that strong feasibility is sufficient and necessary to guarantee the implementability of a completion. So we are looking for a strongest implementable completion ofC. Our results show that if no interaction contains an interaction (an interaction x contains y if x 6= y and the set of participants of y is a subset of x),1then the strongest implementable completion ofC exists; otherwise, in general no such completion is possible.
Furthermore, there exists a fairness notion, which we refer to as SG+, such that when interactions are not allowed to contain interactions, SG+is the strongest implementable fairness notion satisfying equivalence-robustness. In other words, all other implementable and equivalence-robust fairness notions must be weaker than SG+, and all other equivalence-robust fairness notions that are stronger than SG+ or incomparable with SG+ must not be implementable. We also compare SG+ with several existing fairness notions. The results indicate that SG+ is equivalent to SIF+ and SPF+ and is stronger than WIF and WPF+, where SIF+, SPF+, and WPF+ are the maximal completions of SIF, SPF, and WPF, respectively. In particular, when interactions are CSP-like bipartied, SG+is also equivalent to SPF. So SPF is the strongest equivalence-robust property one can observe from a CSP-like program executing in any asynchronous environment. Conversely, if interactions can contain interactions, then in general the strongest implementable and equivalence-robust fairness notion does not exist.
1Note that although x contains y, the establishment of y does not depend on the establishment of x. In the literature, some
languages (e.g., IP and Script) allow participants of an interactionv to establish a “subinteraction” within v. So the subinteraction can be established only whenv has been established.
FIG. 2. The fairness-equivalence partitioning [3].
Finally, we show that if equivalence-robustness is not required, then no system can have a strongest implementable fairness notion, unless the system consists of only one interaction. So, in general, for any implementable fairness notionC, there exists another implementable fairness notion C0such that
C0 is either strictly stronger thanC or is incomparable with C. This implies plenty of leeway in the design of fairness notions suitable for various applications.
The rest of the paper is organized as follows. Section 2 provides some preliminaries. Section 3 considers the implementability of completions. Section 4 presents a comprehensive analysis of several commonly used fairness notions and their minimal and maximal completions. The impossibility result of a strongest implementable fairness notion is the subject of Section 5. Section 6 concludes.
2. PRELIMINARIES
We shall follow the same notations as those given in Part I. In addition, we shall use eq(π) to denote the equivalence class ofπ, i.e., the set of runs that are equivalent to π. Moreover, for notational simplicity we shall use a set P in a run to denote an arbitrary sequence of ready transitions, one by each process in P, where each ready transition is of the form pi· {x ∈I| pi ∈ Px}. For example, assume that
Px12 = {p1, p2} and Px23 = {p2, p3}. Then Px12x12Px23x23 represents a partial run in which p1and p2
become ready (in arbitrary order), they execute x12, and then p2and p3become ready (again, in arbitrary order) and execute x23. Likewise, (Px12 ∪ Px23)x12Px12x23represents a partial run in which p1, p2, and
p3become ready, p1and p2execute x12and become ready again, and then p2and p3execute x23. In addition to the definitions given in Part I, the following are used in this artical.
DEFINITION2.1. A fairness notionC1forIS is stronger than C2(or, alternatively,C2is weaker than
C1) ifC1(IS) ⊆ C2(IS). C1is strictly stronger thanC2ifC1(IS) ⊆ C2(IS). C1andC2are incomparable ifC1(IS) 6⊆ C2(IS) and C2(IS) 6⊆ C1(IS); they are equivalent if C1(IS) = C2(IS).
DEFINITION2.2. [1]. A fairness notionC is equivalence-robust for IS iff ∀π ∈ C(IS), eq(π) ⊆ C(IS). The following is a restatement of strongly feasibility.
DEFINITION2.3. A fairness notionC is strongly feasible for IS iff there exists a nonblocking scheduler S such that r (S, A) ∈ C(IS) for every adversary A.
An immediate consequence of these definitions is the following. LEMMA2.1. LetIS = (P, I, M).
1. IfI6= ∅, then for any strongly feasible fairness notion C, C(IS) 6= ∅.
2. IfC1is strongly feasible forIS and C1(IS) ⊆ C2(IS), then C2is also strongly feasible forIS. 3. It may be the case that bothC1andC2are strongly feasible forIS, but C1∩ C2is not, where the notionC1∩ C2is defined byC1(IS) ∩ C2(IS).
Proof. The first two follow directly from the definitions. For the third, let IS = ({p1, p2, p3},
{x12, x23},M∀), where Px12 = {p1, p2} and Px23 = {p2, p3}. Let C1be defined as follows: in a state
where both x12and x23are enabled, x12must be scheduled for execution (i.e., x12has a higher priority than x23) andC2be defined as “x23has a higher priority than x12.” Then, bothC1andC2are strongly
feasible, but C1∩ C2 is not because no scheduler can make a move if the adversary lets the three processes be ready simultaneously. j
We have shown in Part I that SIF is strongly feasible. Then by Lemma 2.1, any fairness notion that is weaker than SIF is also strongly feasible. Examples include SPF, WPF, and WIF
LEMMA2.2. The following four fairness notions are all strongly feasible: SIF, SPF, WPF, and WIF. On the other hand, as we have shown in Part I, both U-fairness and hyperfairness are not strongly feasible.
In general, to prove thatC is not strongly feasible for IS, we must show that for every nonblocking scheduler S, there is an adversary A such that r (S, A) 6∈ C(IS). However, for most systems there exists an adversary such that every scheduler versus it must generate the same run. So if the run is not included inC(IS), then obviously C cannot be strongly feasible. For example, if an adversary always lets at most one interaction be enabled, then any nonblocking scheduler versus the adversary must generate the same run: whichever interaction is enabled, it must be selected for execution. The resulting runs are called singular in Part I, and are inevitable to every strongly feasible fairness notion ofIS. We shall use SG(IS) to denote the set of singular runs of IS. An immediate consequence of the definition is the following.
LEMMA2.3. For every strongly feasible fairness notionC, SG(IS) ⊆ C(IS).
Note that for every IS, SG(IS) 6= ∅, unless IS contains more than one interaction and for every interaction x, there exists another interaction y such that y is contained in x. Moreover, if SG(IS) 6= ∅, then for every fairness notionC it is never the case that SG(IS) ⊆ C(IS) and SG(IS) ⊆ ¯C(IS), where ¯C is the complement ofC defined by ¯C(IS) = run(IS) − C(IS). Therefore, if C is strongly feasible for IS, then ¯C must not be strongly feasible. In other words, it is never the case that both C and its complement are implementable.
COROLLARY2.4. LetIS = (P, I, M∀). If∃ x ∈I, ∀ y ∈I, y 6= x ⇒ Py6⊆ Px. Then for every fairness
notionC, it is never the case that both C and ¯C are implementable for IS.
Recall from Lemma 4.1 of Part I that in the presence of equivalence-robustness, strong feasibility is sufficient and necessary to determine fairness implementability. As this result will be referenced several times in the paper, for ease of reference, we restate the lemma below.
LEMMA2.5. IfC is strongly feasible and equivalence-robust for IS, then C is implementable for IS. Moreover, since ifC is stronger than C0thenC(IS) ⊆ C0(IS), the fairness implementability criterion immediately implies the following lemma:
LEMMA2.6. SupposeC is stronger than C0. IfC is implementable for IS, then so is C0; and ifC0is not implementable, then neither isC.
3. STRONG FEASIBILITY OF COMPLETIONS
In this section we consider the implementability of equivalence-robust fairness notions. In particular, we shall focus on completions—equivalence-robust fairness notions derived from a non-eqivalence-robust one. We shall show that the process of completion may not preserve strong feasibility. Since in the presence of equivalence-robustness strong feasibility suffices to determine fairness implementability, completions are not necessarily implementable.
Furthermore, we shall also show that if no interaction ofIS contains an interaction, then there exists a fairness notion, denoted by SG+, such that SG+is the strongest implementable and equivalence-robust fairness notion ofIS. On the other hand, if IS contains two interactions x, y such that Px⊆ Pythen in
general there does not exist a strongest implementable and equivalence-robust fairness notion forIS. 3.1. Definitions
DEFINITION3.1 [3]. 1. An equivalence class eq(π) in run(IS) is purely C-fair iff eq(π) ⊆ C(IS), it is purelyC-unfair iff eq(π) ∩ C(IS) = ∅, and it is C-mixed otherwise.
2. A fairness notion ˆC is a comletion of C iff the following three conditions are satisfied: (i) for every purelyC-fair class eq(π), eq(π) ⊆ ˆC(IS)
(ii) for every purelyC-unfair class eq(π), eq(π) ∩ ˆC(IS) = ∅, and
(iii) for every classC-mixed class eq(π), either eq(π) ⊆ ˆC(IS) or eq(π) ∩ ˆC(IS) = ∅.
It follows directly that a completion ˆC must be equivalence-robust. Two extreme completions of C arise naturally: the maximal completionC+, which treats everyC-mixed class as fair, and the minimal completionC−, which treats everyC-mixed class as unfair [3]. Moreover, C−(IS) ⊆ C(IS) ⊆ C+(IS) for everyC. By Lemma 2.1, if C is strongly feasible then so is C+. SinceC+is equivalence-robust, by Lemma 2.5, ifC is strongly feasible then C+must be implementable.
LEMMA3.1. IfC is strongly feasible for IS, then C+must be implementable forIS.
On the other hand, since the process of minimal completion may exclude some runs that are inevitable toC−, C−may be unimplementable. In fact, ifC is not implementable then strong feasibility cannot be preserved byC−. Therefore, unlike maximal completions, minimal completions do not help us obtain an implementable fairness notion from an unimplementable one while pursuing equivalence-robustness.
LEMMA3.2. IfC is not implementable for IS, then neither is C−. Moreover, ifC is not implementable, thenC−must not be strongly feasible.
Proof. SinceC−(IS) ⊆ C(IS), by Lemma 2.6, if C is not implementable then neither is C−. Since
C−is equivalence-robust, by Lemma 2.5, it must not be strongly feasible. j 3.2. Strongly Feasible Completions
As it turns out, the weakest completion (i.e., the maximal completion) of a strongly feasible fairness notion is also strongly feasible, while the strongest completion (i.e., the minimal completion) may not be. Since strongly feasible completions are implementable, and since stronger completions induce more liveness properties, given a strongly feasible fairness notionC, one would wish to know what is the strongest, strongly feasible completion ofC, or does it even exist. To answer this, we first establish a more important theorem showing the existence of a strongest fiarness notion that is both strongly feasible and equivalence-robust. For this, we need the following lemma.
LEMMA3.3. LetIS = (P,I,M) and assume that∀x, y ∈ I, x 6= y ⇒ Px 6⊆ Py. The everyπ ∈ run(IS) satisfying SIF is equivalent to a singular run.
Proof. Letπ ∈ run(IS) be a run given by
π = p1,1.I1,1. . . p1,n1.I1,n1x1 p2,1.I2,1. . . p2,n2.I2,n2x2. . . ,
where x1, x2, . . . are the sequence of interactions executed in π. Assume that π satisfies SIF. Consider x1. Suppose that we transformπ into another run π1by the following procedure: For each p1, j.I1, j, 1 ≤ j ≤ n1, if (1) p1, j /∈ Px1and (2) at some point inπ (after the ready transition p1, j.I1, j) some interaction
y involving p1, jis enabled, then move the action p1, j.I1, jafter x1. Clearly,π ≡ π1. Due to the restriction imposed on the structure ofIS, no subset of Px1is involved in any other interaction. So inπ1at most
one interaction is enabled at any point up to x1.
Similarly, we can transform π1into another runπ2 by applying the above procedure to the ready transitions occurring between x1and x2so thatπ1≡ π2, and inπ2at most one interaction is enabled at any point up to x2. We claim that if we apply the procedure repeatedly for the rest of xi’s, then we will
obtain a runπ∞such thatπ ≡ π∞andπ∞is singular. To see this, observe that for any finite i , we have π ≡ π1≡ · · · ≡ πi, and inπi at most one interaction is enabled at any point up to xi So it suffices to
show that the equivalence relation betweenπ and πiis preserved when i → ∞.2
2Note that, in general, equivalence relation may not be preserved through an infinite number of such transformations. For
example, considerπ = p1( p2p3x)ω, and assume that Py= {p1, p2} and Px= {p2, p3}. Let πi = (p2p3x)ip1( p2p3x)ω. Then,
Suppose otherwise that the equivalence relation does not hold. Then, it must be the case that some ready transition pk, j.Ik, j in between xk−1and xkof runπk has to be moved during the transformation
from πl−1 toπl for every l ≥ k, resulting in the extinction of pk, j.Ik, j when the transformation is
performed an infinite number of times. However, recall that if pk, j.Ik, j has to be moved in the kth
transformation (i.e., fromπk−1) toπk, then (1) pk, j /∈ Pxk and (2) later at some point inπk−1(and thus
inπ) some interaction y involving pk, j is enabled. Since in the remaining transformations pk, j.Ik, j
is continually moved, none of the interactions xk, xk+1, . . . involves process pk, j, and there exists an
infinitely number of points inπ such that at each point some interaction involving pk, jis enabled, but
from xkonward pk, j never participates in any interaction. Soπ does not satisfy SPF, and thus π does
not satisfy SIF. This contradicts the assumption thatπ satisfies SIF. Therefore, the equivalence relation betweenπ and π∞is preserved during the transformations fromπ to π∞. j
Recall from Lemma 2.3 that for every strongly feasible fairness notionC, SG(IS) ⊆ C(IS), where SG(IS) is the set of singular runs of IS. Define fairness notion SG+ to be the maximal completion of SG, i.e.,
SG+(IS) = [
π∈SG(IS)
eq(π).
Then, for everyC that is both strongly feasible and equivalence-robust, SG+(IS) ⊆ C(IS). Moreover, by Lemma 3.3, SIF(IS) ⊆ SG+(IS). Since SIF is strongly feasible, by Lemma 2.1 SG+is also strongly feasible. Hence, by Lemma 2.5 SG+is implementable. The following theorem can thus be established. THEOREM3.4. LetIS = (P,I,M) and assume that∀x, y ∈ I, x /∈ y ⇒ Px 6⊆ Py. Then, SG+ is strongly feasible and equivalence-robust forIS, and for every other strongly feasible and equivalence-robust fairness notionC, SG+(IS) ⊆ C(IS).
To illustrate SG+, consider the following example taken from [1]: p1:: b1:= true; ∗[b 1; p2! 0→ b1:= false] p2:: b2:= true; ∗[b 2; p1? x→ b2 := false 2 b2; p3? x→ skip]; p3! 0 p3:: b3:= true; ∗[b 3; p2! 0→ skip 2 b3; p2? y→ b3 := false]
In this system, p1 and p2 may interact, and p2 and p3 may interact. In particular, p2 and p3 may establish two possible interactions, one to deliver a value from p3 to p2and the other in the opposite direction. Although the two interactions contain each other, the program does not allow them to be enabled simultaneously. So Theorem 3.4 can be applied to the system so that SG+ is the strongest implementable and equivalence-robust fairness notion for the system. From the program, it can be seen that the system may not terminate as p2and p3may repeatedly establish an interaction forever. However, any run of the system satisfying SG+must terminate.
From Theorem 3.4, we can derive the following corollary.
COROLLARY3.5. LetIS = (P,I,M) and assume that∀x, y ∈I, x 6= y ⇒ Px 6⊆ Py. Then for every
strongly feasible fairness notionC, the completion C∗defined by
C∗(IS) = SG+(IS) ∪ {π ∈ E | E is a purely C-fair equivalence class in run(IS)} is the strongest implementable completion ofC.
Proof. SinceC is strongly feasible, by Lemma 2.3, SG(IS) ⊆ C(IS). So every equivalence class in SG+(IS) must be purely C-fair or C-mixed. So by definition C∗is a completion ofC. Moreover, since SG+(IS) ⊆ C∗(IS) and since SG+is strongly feasible, by Lemma 2.1,C∗is also strongly feasible. By Lemma 2.5, therefore,C∗is an implementable completion ofC.
To show thatC∗is the strongest implementable completion ofC, let ˆC be any other implementable completion ofC. Then, by Theorem 3.4 and by the definition of completions, C∗(IS) ⊆ ˆC(IS). Hence,
C∗is the strongest strongly feasible completion ofC. j
Note that Theorem 3.4 does not depend on the arity of interactions, and so it holds as well if interactions are strictly bipartied. In particular, if every pair of processes share at most one interaction, then SG+is the strongest strongly feasible and equivalence-robust fairness notion one can get for biparty interaction systems.
COROLLARY3.6. For everyIS = (P,I,M) such that∀x ∈I, |Px| = 2 and ∀x, y ∈I, x 6= y ⇒ Px6=
Py, SG+is the strongest fairness notion forIS that is both strongly feasible and equivalence-robust.
3.3. Non-Strongly-Feasible Completions
On the other hand, if some interaction contains an interaction, then the strongest strongly feasible and equivalence-robust fairness notion may not exist. Before proving this, we first show that ifIS in addition contains at least two processes, then not all strongly feasible fairness notions ofIS have a strongest implementable completion. Note that for this we shall consider interaction systems with programs of typeM∀. It can be seen that even if interactions may contain interactions, if the associated program
M guarantees that at any time no enabled interaction x contains an interaction that is also enabled simultaneously, then SG+is still the strongest strongly feasible and equivalence-robust fairness notion for the system.
THEOREM3.7. LetIS = (P,I,M∀) be an interaction system satisfying the following conditions: 1. |P| > 1 and
2. ∃x, y ∈I, x 6= y, Px ⊆ Py, and∀z ∈I, Pz ⊆ Py⇒ Px ⊆ Pz.
Then, there exists a fairness notionC which is strongly feasible but does not have a strongest strongly feasible completion.
Proof. Let x, y ∈Ibe two interactions satisfying condition (2). Consider first that|Py| ≥ 2. let p1 and p2be two arbitrary processes in Py. Clearly, run(IS) contains runs of the form
p1p2(Py− {p1, p2})z1Pz1z2Pz2z3Pz3. . . . (1)
Let Exand E¯x be two subsets of run(IS) defined by
Ex = {π | π is equivalent to some run of form (1) where ∀i, zi= x}
E¯x = {π | πis equivalent to some run of form (1) where ∃i, zi 6= x}.
The two sets are obviously not empty and disjoint. Note that in the presence of p1and p2, each runπ in Exand E¯xhas at least one equivalent run different fromπ, i.e., |eq(π)| ≥ 2 (because the first ready transitions of the two processes can be arbitrarily permuted).
Let S be a nonblocking scheduler which selects an arbitrary enabled interaction for execution, except:
• If initially the adversary schedules the sequence of ready transitions p1p2(Py− {p1, p2}), then x will always be chosen for execution whenever it is enabled.
• If initially the adversary schedules the sequence of ready transitions p2p1(Py− {p1, p2}), then y will always be chosen for execution whenever it is enabled.
Define fairness notionC to be the following:
ThenC is strongly feasible because S generates only C-fair runs. Observe that every run of the form p1p2(Py− {p1, p2})(x Px)ω belongs toC(IS) but its equivalent run p2p1(Py− {p1, p2})(x Px)ωdoes
not. So every equivalence class eq(π) ⊆ Ex isC-mixed. (In fact, there is only one equivalence class
in Ex.) On the other hand, for every π of form (1) such that for some i, zi 6= x, π must not belong to
C(IS) because no adversary versus S can generate π. So every equivalence class eq(π) ⊆ E¯xis either
C-mixed or is purely C-unfair.
Recall from Lemma 2.1 that ifC1 is strongly feasible andC1(IS) ⊆ C2(IS), then C2 must also be strongly feasible. From the above description ofC, it can be seen that there exists a strongly feasible fairness notionC0forIS satisfying the following two conditions:
• ∀π ∈ run(IS) − (Ex∪ E¯x), π ∈ C0(IS), and
• ∀π ∈ Ex∪ E¯x, eq(π) ∩ C0(IS) 6= ∅ and eq(π) ∩ C0(IS) 6= ∅.
For example,C0can be obtained by extending the aboveC to include every run in run(IS)−(Ex∪ E¯x) and including one run from every purelyC-unfair class of E¯x.
Now, since each equivalence class eq(π) ⊆ Ex∪ E¯x isC0-mixed, every completion ˆC of C0must decide the fairness of eq(π). Moreover, if ˆC0is strongly feasible, then ˆC0cannot treat all the eq(π)’s in Ex∪ E¯xas unfair; otherwise, no nonblocking scheduler can generate a fair run if it faces the following adversary. Initially, the adversary schedules the sequence of partial run p1p2(Py− {p1, p2}); subse-quently, whichever interaction is chosen by the scheduler, the adversary in response simply schedules the processes of the interaction to be ready again.
We can define two completions ˆC0x which treats all equivalence classes in Ex as fair and those in
E¯x as unfair, and ˆC0¯x, which is defined in the other way. We argue that both are strongly feasible. To see this, consider first a nonblocking scheduler Sx which selects an arbitrary enabled interaction for
executioin, except that x must be chosen whenever it is enabled. Then for every runπ generated by Sx,
ifπ is equivalent to some run of form (1), then all of the zi’s must be instances of x. This is because at
any point inπ only the processes in Pycan be ready. So for every zi, Pzi ⊆ Py. By condition (2), x is
enabled whenever ziis. Since Sxprefers x to any other interaction containing x, zi = x. So Sxcannot
generate any run in E¯x. Therefore, ˆC0xis strongly feasible because Sxgenerates only runs in ˆC0x.
For the strong feasibility of ˆC0¯xconsider a nonblocking scheduler S¯xwhich selects an arbitrary enabled interaction for execution, except that y must be chosen whenever y is enabled. Since every run in Ex
contains a state in which y is enabled, no adversry versus S¯x can generate a run in Ex. So every run
generated by S¯xsatisfies ˆC0¯x. Hence, ˆC0¯xis also strongly feasible.
Observe that the two completions ˆC0x and ˆC0¯x are incomparable. So neither of them can be the strongest implementable completion ofC0. Moreover, recall that for every strongly feasible comp-letion ˆC0ofC0, ˆC0(IS) must contain some equivalence classes in Ex∪E¯x. So if ˆC0contains all equivalence classes in Ex∪ E¯x, then ˆC0must be weaker than ˆC0xand ˆC0¯x; and if ˆC0(IS) contains only part of them, then ˆC0must be incomparable with either ˆC0x or ˆC0¯x. Therefore,C0does not have a strongest strongly feasible completion.
In the above proof, we have assumed that|Py| ≥ 2. If |Py| = 1, then Px= Py. Since|P| > 1, either
there exists an interaction u involving more than one process, or there exists two interactions u1, u2 such that|Pu1| = |Pu2| = 1 and Pu16= Pu2. In the former case, we can modify form (1) to
p1p2(Pu− {p1, p2})v1· · · vkPyz1Pz1z2Pz2z3Pz3. . . ,
where p1and p2are two arbitrary process in Pu andv1, . . . , vk are instances of interactions such that
no interaction is enabled immediately aftervk. In the latter case, we instead consider the form
p1u01p2u02Pyz1Pz1z2Pz2z3Pz3. . . ,
where Pu1 = {p1} and Pu2 = {p2}. In either case, we can define Ex and E¯x analogously and show
that there exists a strongly feasible fairness notionC0such that all its strongly feasible completions intersect (a) both Ex and E¯x, (b) only Ex, or (c) only E¯x SoC0 does not have a strongest strongly feasible completion. j
Note that in Theorem 3.7, ifPconsists of only one process, then for anyπ ∈ run(IS), the equivalence class eq(π) consists of π itself. So for any fairness notion C, there is only one completion, i.e., C itself. Therefore, it holds trivially that ifC is strongly feasible for IS, then C is the strongest strongly feasible completion ofC.
We now show tht if some interaction contains an interaction, then there may not exist a strongest fairness notion forIS that is both strongly feasible and equivalence-robust.
THEOREM3.8. LetIS = (P,I,M∀) be an interaction system satisfying the following condition:
∃x, y ∈I, x 6= y, Px⊆ Py, and ∀z ∈I, Pz ⊆ Py⇒ Px ⊆ Pz.
Then, there does not exist a fairness notionC such that (1) C is strongly feasible and equivalence-robust and (2)C is the strongest fairness notion for IS that satisfies Condition (1).
Proof. The proof is similar to that of Theorem 3.7, except that we do not need processes p1and p2to make some equivalence classes of run(IS) consist of more than one run. Let Ex and E¯xbe two subsets of runIS defined by
Ex = {π | πis equivalent to some run of the form Py(x Px)ω},
E¯x = {π | πis equivalent to some run of the form Pyz1Pz1z2Pz2. . . where ∃i, zi 6= x}.
Then, using an argument similar to Theorem 3.7, we can show that any strongly feasible and equivalence-robust fairness notionC for IS must intersect either Exor E¯x. Furthermore, there are two incomparable fairness notions (which are strongly feasible and equivalence-robust)CxandC¯xsuch that the following two conditions are satisfied: (1) Ex ⊆ Cx(IS) and Cx(IS) ∩ E¯x = ∅ and (2) E¯x ⊆ C¯x(IS) and
C¯x(IS) ∩ Ex = ∅. All other strongly feasible and equivalence-robust fairness notions for IS must be
either weaker than Cx andC¯x or incomparable with one of them. Therefore, the strongest strongly feasible and equivalence-robust fairness notion forIS does not exist. j
Note that like Theorem 3.4, both Theorems 3.7 and 3.8 hold as well if interactions are strictly bipartied. To illustrate Theorem 3.8, letIS = ({p}, {x, y},M∀), where Px = Py = {p}. Let Fx = {(px)ω}
and Fx = {(py)ω}. Then both are strongly feasible and equivalence-robust (and so are implementable).
However, the two fairness notions are incomparable. Note that each fairness notion has only one completion, i.e., itself. So each has a strongest implementable completion.
3.4. A Patch
The readers may have noticed that Theorem 3.8 alone is not enough to determine whether there exists a strongest implementable and equivalence-robust fairness notion for allIS = (P,I,M∀) where some interaction contains an interaction. This is because Theorem 3.8 concerns only the case where some interaction y ∈ I contains a minimal interaction x (where an interaction u is minimal if for every interactionv contained in u, Pu = Pv) such that for all other minimal interactionsw contained in
y, Pw= Px. Clearly, y may contain two minimal interactions x and z such that neither of them contains
the other. As we shall see, these systems do have a strongest implementable and equivalence-robust fairness notion, which is, by no surprise, SG+.
LEMMA3.9. LetIS = (P,I,M∀) and assume that
∀x, y ∈I, x 6= y, Px⊆ Py⇒ ∃z, w ∈I, Pz ⊆ Py, Pw⊆ Py, Pz 6⊆ Pw, and Pw6⊆ Pz.
Then a runπ ∈ run(IS) is equivalent to a singular run if it satisfies the following conditions: 1. No interaction containing an interaction is ever executed inπ.
2. For every x not containing any interaction, if x is enabled infinitely often, then it is executed infinitely often.
Proof. Letπ ∈ run(IS) be a run given by
π = p1,1.I1,1. . . p1,n1.I1,n1x1 p2,1.I2,1. . . p2,n2.I2,n2x2. . . ,
where x1, x2, . . . are the sequence of interactions executed in π. Assume that π satisfies conditioins 1 and 2. We can use the method described in Lemma 3.3 to transform π into an equivalent run π1 by moving each p1, j.I1, j, 1 ≤ j ≤ n1, to the end of x1, where p1, j.I1, j satisfies the following two conditions: (a) p1, j /∈ Px1and (b) at some point inπ (after the ready transition p1, j.I1, j) some interaction
y involving p1, jis enabled. By condition 1 of the lemmaπ1is singular up to x1.
Like Lemma 3.3, the transformation can be done ad infinitum. Letπ∞denote the resulting run. Unlike Lemma 3.3, however, some ready transition pk, j.Ik, jin between xk−1and xkmay be kept moving forever
in the rest of the transformation fromπktoπ∞. (If no ready transition is moved indefinitely thenπ ≡ π∞
andπ∞is singular; hence we are done.) If this happens, then by the transformation some interaction y involving process pk, jis enabled infinitely often but from xkonward y is never executed. Note that by the
conditions of the lemma, y must contain two interactionsw and z such that Pw− Pz6= ∅, Pz− Pw6= ∅,
and neither of them contains an interaction. Since bothw and z are enabled whenever y is enabled, w and z are enabled infinitely often throughoutπ. Since they do not contain any interaction, by condition 2 they are executed infinitely often inπ.
We can then modify the transformation such that starting fromπkthe ready transition pk, j.Ik, j will
not be moved in the rest of the transformation. Without loss of generality assume that no other ready transition is kept moving forever in the new transformation. (If there is one, then we can use the same method to freeze that transition too.) Letπ∞0 be the resulting run. It is clear thatπ ≡ π∞0 because no ready transition is kept moving forever.
We claim thatπ∞0 is singular. By the transformation, it suffices to show that y will never be enabled even if we stop moving pk, j.Ik, jfrom xkonward. For this, suppose otherwise y is enabled in some state
s inπ∞0 . Sow and z are also enabled in s. Recall that w and z are executed infinitely often in π (and thus inπ∞0 ). Let u be the first interaction that is executed after s. By condition 1, Pucannot contain Pw
and Pz. So either Pw− Pu 6= ∅ (when u 6= w) or Pz− Pu 6= ∅ (when u 6= z). Since both w and z are
executed infinitely often, by the transformation either the ready transitions by the processes in Pw− Pu
or the ready transitions by the processes in Pz− Pu will be moved after s. Hence, y cannot be enabled
in s; contradiction. The lemma is thus proven. j
To illustrate Lemma 3.9, assume that IS = ({p1, p2, p3}, {x2, x3, x23, x123},M∀), where Px2 =
{p2}, Px3 = {p3}, Px23 = {p2, p3}, and Px123 = {p1, p2, p3} (see Fig. 3c). Then the run
π = p1p2p3(x2p2x2p2x3p3)ω can be transformed into
ρ = p1( p2x2p2x2p3x3)ω which is singular and is equivalent toπ.
THEOREM3.10. LetIS = (P,I,M∀) and assume that
∀x, y ∈I, x 6= y, Px⊆ Py⇒ ∃z, w ∈I, Pz ⊆ Py, Pw⊆ Py, Pz 6⊆ Pw, and Pw6⊆ Pz
Then, SG+is the strongest strongly feasible and equivalence-robust fairness notion forIS.
Proof. By Lemma 2.3, for every strongly feasible and equivalence-robust fairness notionC, SG+(IS)
⊆ C(IS). As by definition SG+is equivalence-robust, to prove the theorem it suffices to show that SG+ is strongly feasible forIS. Moreover, by Lemma 3.9, it suffices to show that there exists a nonblocking scheduler forIS satisfying conditions 1 and 2 of the lemma. Such a scheduler can be easily obtained by modifying the SIF-scheduler presented in Part I (Fig. 6) so that no interaction containing an interaction is ever selected for execution. j
FIG. 3. Instances of interaction systemsIS = (P, I, M∀) which permit some interactions to contain an interaction but have a strongest implementable and equivalence-robust fairness notion.
Figure 3 illustrates some instances ofIS that have a strongest implementable and equivalence-robust fairness notion. Theorem 3.10 implies the following corollary (cf. Corollary 3.5).
COROLLARY3.11. LetIS = (P,I,M∀) and assume that
∀x, y ∈I, x 6= y, Px⊆ Py⇒ ∃z, w ∈I, Pz ⊆ Py, Pw⊆ Py, Pz 6⊆ Pw, and Pw6⊆ Pz.
Then for every strongly feasible fairness notionC, the completion C∗defined by
C∗(IS) = SG+(IS) ∪ {π ∈ E | E is a purely C-fair equivalence class in run(IS)} is the strongest implementable completion ofC.
4. COMPARISONS OF SG+WITH OTHER FAIRNESS NOTIONS
In this section we compare SG+with the following well-known fairness notions and their completions: Strong interaction fairness (SIF): An interaction that is infinitely often enabled is executed infinitely often.
Strong process fairness (SPF): A process that is infinitely often ready for an enabled interaction engages in an interaction infinitely often.
Weak process fairness (WPF): A process that is continuously ready for an enabled interaction (not necessary the same interaction) will eventually engage in an interaction.
Weak interaction fairness (WIF): An interaction that is continuously enabled will eventually be executed.
The comparison is intended to be comprehensive so that we know how these fairness notions differ for various systems. In particular, we shall divide the comparison into two subsections—one for systems involving strictly biparty interactions (`a la CSP and Ada), and the other for those involving multiparty interactions of arbitrary arity. Recall that SG+is the strongest implementable and equivalence-robust fairness notion for systems where interactions cannot contain interactions. In the biparty case, an interaction x cannot be contained in another interaction y if Px 6= Py. This means that if interaction
names only serve to identify the participants, then SG+is the strongest implementable and equivalence-robust fairness notion for biparty interaction systems.3 We shall therefore useIB to denote a set of biparty interactions such that∀ x ∈IB, |Px| = 2 and ∀ y ∈IB− {x}, Px 6= Py.
Recall from Lemma 2.2 that the above four fairness notions are all strongly feasible. Their equivalence-robustness is summarized in Table 1. It is clear that for everyIS the following relation holds [1, 2]:
SIF(IS) ⊆ SPF(IS) ⊆ WPF(IS) ⊆ WIF(IS).
In particular, depending on the instances ofIS, the fairness notions may be identical or strictly different. To study the structure of interactions that distinguishes these fairness notions and their minimal and maximal completions, we shall associateIS with a program of typeM∀.
3In practice an interaction name usually identifies the set of participants, while the interaction body determines the content
of communication, which can vary dynamically, and in some cases can even involve nondeterministic choices among guarded commands.
TABLE I
Equivalence-Robustness of Various Fairness Notions [1] Biparty interactions Multiparty interactions
SIF − −
SPF + −
WPF − −
WIF + +
4.1. Biparty Interaction Systems
We will establish some lemmas that are useful in classifying the relationship between SG+and SIF, SPF, WPF, WIF, and their minimal and maximal completions. We begin with the comparison of SIF−, SIF, and SIF+. By definition of completions, for everyIS we have SIF−(IS) ⊆ SIF(IS) ⊆ SIF+(IS). Since SIF is not equivalence-robust, there exists someIS that distinguishes SIF−, SIF, and SIF+. The following lemma shows when they are distinct.
LEMMA4.1. For everyIS = (P, I, M∀), SIF−(IS) ⊆ SIF(IS) ⊆ SIF+(IS). In particular, SIF−(IS) ( SIF(IS) ( SIF+(IS) if ∃ x, y, z ∈I, Px∩ Py 6⊆ Pzand Px∩ Pz 6⊆ Py.
Proof. To see the proper subset relation, consider the run π = ((Px− Pz)∪ Py)( y Pzz Py)ω.
If only y and z are enabled infinitely often inπ, then π ∈ SIF(IS). If some other interaction w is enabled infinitely often, then due to the restriction imposed onIS, w 6= x because x is never enabled in π. So either Pw⊆ (Px− Pz)∪ Pyor Pw⊆ (Px− Py)∪ Pz. If Pw⊆ (Px− Pz)∪ Py, then let
π0= ((P
x− Pz)∪ Py)(w Pwy Pzz Py)ω;
otherwise let
π0= ((P
x− Pz)∪ Py)( y Pzw Pwz Py)ω.
In either case, ifπ0is still not in SIF(IS), then similarly there must be another interaction u such that either Pu ⊆ (Px− Pz)∪ Py or Pu ⊆ (Px− Py)∪ Pz and u is enabled infinitely often but is never
executed. Then we can use the above method to obtain another runπ00such that u is executed infinitely often inπ00. So without loss of generality assume thatπ ∈ SIF(IS).
Consider the run
ρ = ((Px− Pz)∪ Py)((Pz− Py) y (Pz∩ Py) z Py)ω.
It is easy to see thatρ ≡ π. However, ρ does not satisfy SIF because x is now enabled infinitely often inρ but it is never executed. By the definition of minimal completions, π ∈ SIF(IS) − SIF−(IS); and by the definition of maximal completionsρ ∈ SIF+(IS) − SIF(IS). j
Figures 4b and 4c illustrate some instances ofIS for which SIF−(IS) ( SIF(IS) ( SIF+(IS).4 LEMMA4.2. For everyIS = (P, I, M∀), SIF(IS) ⊆ SPF(IS). In particular, SIF(IS) ( SPF(IS) if
∃ x, y1, . . . , yn∈Isuch that∀i ≤ n, Pyi ∩ Px6= ∅ and
S
i(Pyi ∩ Px)= Px.
4It can also be shown that SIF−(IS) ( SIF(IS) ( SIF+(IS) only if ∃ x, y, z ∈I, P
x∩ Py6⊆ Pzand Px∩ Pz6⊆ Py. Since we
FIG. 4. Instances of interaction systemsIS = (P, I, M∀) for which SIF(IS) ( SPF(IS). Moreover, SIF is not equivalence-robust for (b) and (c).
Proof. It is easy to see that∀ IS, SIF(IS) ⊆ SPF(IS). To see the proper subset condition, consider the run
π =¡Py1∪ · · · ∪ Pyn
¢¡
y1Py1· · · ynPyn
¢ω.
Thenπ ∈ SPF(IS) − SIF(IS) because (1) x is enabled infinitely often (x is enabled because Px ⊆
Py1 ∪ · · · ∪ Pyn) but is never executed (so π 6∈ SIF(IS)) and (2) every process in π executes some
interaction yi infinitely often (soπ ∈ SPF(IS)). j
Figure 4 illustrates some instances ofIS for which SIF(IS) ( SPF(IS).
We have shown the structure of IS that makes SIF non-equivalence-robust; that is, SIF−(IS) ( SIF(IS) ( SIF+(IS). Given that SIF(IS) ( SPF(IS), it is interesting to compare SPF with SIF+. As we shall see shortly, SIF+, SPF+, and SG+are all equivalent when interactions cannot contain interactions. Moreover, since in the biparty case SPF is equivalence-robust, it follows that SPF, SPF+, SIF+, and SG+are all equivalent.
LEMMA4.3. For everyIS = (P, I, M), if∀x, y ∈I, x 6= y ⇒ Px 6⊆ Py, then SIF(IS) ⊆ SG+(IS),
and SPF(IS) ⊆ SG+(IS).
Proof. This follows directly from Lemma 3.3, and note that the proof of Lemma 3.3 can also be used to show that every runπ ∈ SPF(IS) is equivalent to a singular run. j
LEMMA 4.4. For every IS = (P, I, M), if ∀x, y ∈ I, x 6= y ⇒ Px 6⊆ Py, then SIF+(IS) =
SPF+(IS) = SG+(IS).
Proof. By Lemma 4.3 and the fact that SG+ is equivalence-robust, SIF+(IS) ⊆ SG+(IS) and SPF+(IS) ⊆ SG+(IS). On the other hand, by Lemmas 2.2 and 2.1, SIF+and SPF+are strongly feasible and equivalence-robust. By Theorem 3.4, SG+(IS) ⊆ SIF+(IS) and SG+(IS) ⊆ SPF+(IS). Hence SIF+(IS) = SPF+(IS) = SG+(IS). j
We now consider the notion of WPF and its completions.
LEMMA 4.5. For every IS = (P, I, M∀), SPF−(IS) ⊆ WPF−(IS). In particular, SPF−(IS) ( WPF−(IS) if ∃ x, y ∈ Isuch that (1) Px∩ Py 6= ∅, and (2) ∃ p ∈ Px− Py such that∀ z ∈ I, Pz ⊆
Px− Py⇒ p 6∈ Pz.
Proof. Since SPF(IS) ⊆ WPF(IS), SPF−(IS) ⊆ WPF−(IS). To see the proper subset condition, without loss of generality assume that x and y are two interactions satisfying conditions (1) and (2) of the lemma such that for all other interactions x0and y0satisfying the same conditions,|Px∪ Py| ≤
|Px0∪ Py0|.
Consider the run
π = (Px∪ Py)(y Py)ω.
Let p be the process satisfying condition (2) of the lemma. Since p ∈ Px− Pyand since x is enabled
z1is continuously enabled inπ, then Pz1⊆ Px− Py. By condition (2) of the lemma, p6∈ Pz1. Then in the run π0= (P x∪ Py) ¡ yz1PyPz1 ¢ω
z1is not continuously enabled. Still,π0does not satisfy SPF because p is ready for an enabled interaction (i.e., x) infinitely often but it never engages in any interaction. Soπ0does not satisfy SPF−either. If some other interaction z2is still continuously enabled inπ0, then Pz2 ⊆ Px− Py− Pz1 and p6∈ Pz2.
The above method can be used again to obtain a runπ00such thatπ00does not satisfy SPF and z2is not continuously enabled. As there are only a finite number of interactions inI, without loss of generality letρ = (Px∪ Py)(yz1z2. . . zkPyPz1Pz2. . . Pzk)ωbe a run that does not satisfy SPF and SPF
−and that does not have an interaction that is continuously enabled. Note that by the construction, for every two different interactions a, b executed in ρ, Pa∩ Pb= ∅.
We argue that all runs in eq(ρ) satisfy WPF. To see this, suppose otherwise some run ψ in eq(ρ) violates WPF. Then, given that no interaction is continuously enabled inρ (and thus in ψ), there must exist two interactions u1 andv1, where Pu1 ∪ Pv1 ⊆ Px∪ Py, such that (a) Pu1∩ Pv1 6= ∅, (b) v1 is
executed infinitely often inψ, and (c) some process q ∈ Pu1− Pv1is continuously ready for an enabled
interaction but it never executes any interaction. Moreover, immediately afterv1is executed q must still be ready for an enabled interaction. Let u2be the smallest such interaction so that there is no interaction a such that Pa( Pu2. Because no interaction is continuously enabled inρ, u2 will subsequently be
disabled due to the execution of some interactionv2. So Pv1∩ Pu2= ∅ and Pv2∩ Pu26= ∅. Since any two
different interactions executed inρ are disjoint, Pv1∩ Pv2= ∅. Given that Pu1, Pu2, Pv1, Pv2 ⊆ Px∪ Py,
we have Pu2∪ Pv2( Px∪ Py.
However, because q is not involved in an interaction a such that Pa( Pu2, it is not involved in any
interaction b such that Pb ⊆ Pu2− Pv2. Then u2andv2satisfy the lemma conditions onIS; but this
then contradicts our earlier assumption that|Px∪ Py| ≤ |Pu2∪ Pv2|. Therefore, all runs in eq(ρ) satisfy
WPF. Henceρ ∈ WPF−(IS) − SPF−(IS). j
Figure 5 depicts some instances ofIS for which SPF−(IS) ( WPF−(IS). The following lemma on the non-equivalence-robustness of WPF is somewhat complex.
LEMMA 4.6. For every IS = (P, I, M∀), WPF−(IS) ⊆ WPF(IS) ⊆ WPF+(IS). In particular, WPF−(IS) ( WPF(IS) ( WPF+(IS) if ∃ xi, yi ∈ I, where 0 ≤ i ≤ n − 1 and n > 1, and ∃ p ∈ P
such that (1) p ∈ TPxi, p 6∈ S Pyi, (2)∀ i, Pyi ∩ Pxi 6= ∅, Pyi ∩ Pxi+1 = ∅, and (3) ∀ u ∈ I, Pu ⊆ S Pxi − S
Pyi ⇒ ∃ v ∈ I, Pv∩ Pu 6= ∅, p 6∈ Pv, and∃ i, Pv∩ Pxi = ∅. (Note that in the lemma
additions and subtractions on indices of x and y are to be interpreted modulo n). Proof. To see the proper subset conditions, consider the run
π =³ [Pxi ∪ [ Pyi ´ ¡ y0Py0y1Py1. . . yn−1Pyn−1 ¢ω .
Observe that before each instance of yj process p is ready for all xi’s; and since Pyj ∩ Pxj+1= ∅, after the instance p is ready for at least xj+1 (which exists because n> 1). So p is continuously ready for
an enabled interaction (starting from the point the first interaction is to be executed). Since p never executes any interaction,π 6∈ WPF(IS). Now consider the run
ρ =³ [Pxi− [ Pyi ´ ¡ Py0y0Py1y1. . . Pyn−1yn−1 ¢ω
which is obtained fromπ by deferring for each j the readiness ofSPyi− Pyj before each instance of
yjuntil the instance is executed. Since the deferred actions are independent of the instance of yj, and
since no action is deferred indefinitely,ρ is equivalent to π. However, since ∀ i, Pyi ∩ Pxi 6= ∅, right
after each instance of yjnone of the xi’s is enabled. So the xi’s can no longer cause p to be continuously
ready for an enabled interaction.
Ifρ ∈ WPF(IS) then we are done because ρ ∈ WPF(IS) − WPF−(IS), while π ∈ WPF+(IS) − WPF(IS). If ρ 6∈ WPF(IS), then some process is still continuously ready for an enabled interaction but it never engages in any interaction. Observe that after each instance of yj only the set of processes
S
Pxi−
S
Pyiare ready for interaction. Moreover, the processes are continuously ready for interaction
throughoutρ. So if some process is continuously ready for an enabled interaction but never engages in any interaction, then the process must be continuously ready for the same interaction, say u, and
Pu⊆
S
Pxi −
S
Pyi. By condition (3) there exists somev (where v could be u) and some k such that
Pv∩ Pu 6= ∅, p 6∈ Pv, and Pv∩ Pxk = ∅.
Letπ0andρ0be two equivalent runs given by π0=³ [P xi ∪ [ Pyi∪ Pv ´ ¡ y0Py0y1Py1. . . yn−1Pyn−1v Pv ¢ω ρ0=³ [P xi − [ Pyi − Pv ´ ¡ Py0y0Py1y1. . . Pyn−1yn−1Pvv ¢ω.
Since Pv∩ Pxk = ∅, p is still continuously ready for an enabled interaction in π0even ifv is executed
infinitely often. Soπ06∈ WPF(IS). Moreover, since Pu∩ Pv6= ∅, u is not continuously enabled in ρ0. So
eitherρ0∈ WPF(IS), in which case we are done, or there exists another u0, Pu0 ⊆
S
Pxi−
S
Pyi− Pv,
such that u0is continuously enabled inρ0. In the latter case, we can apply the above method again to obtain two equivalent runsπ00 andρ00such thatπ00 6∈ WPF(IS) and u0(and u) are not continuously enabled inρ00. Given that there are only a finite number of interactions and a finite number of processes inIS, eventually we will establish the lemma. j
Figure 6 depicts some instances of IS for which WPF−(IS) ( WPF(IS) ( WPF+(IS). Note that the non-equivalence-robustness must be intrigued by at least four interactions. In Fig. 6c, all the six interactions are needed in making p1be continuously ready for an enabled interaction but never engage in any interaction.
LEMMA4.7. For everyIS, WPF+(IS) = WIF(IS).
Proof. We shall show that for everyπ ∈ run(IS) it is never the case that eq(π) ⊆ WIF(IS) − WPF(IS). Since both WPF+and WIF are equivalence-robust, and since WPF(IS) ⊆ WPF+(IS) ⊆ WIF(IS), we therefore have WPF+(IS) = WIF(IS).
Letψ be any run in WIF(IS)−WPF(IS). Then, there must exist a process p such that from some point onward (say t0) p is continuously ready for an enabled interaction, but p never executes any interaction thereafter. Moreover, sinceψ satisfies WIF, p cannot be ready for the same interaction continuously.
So there exists an infinite number of points t1, t2. . . such that (1) p is continuously ready for some interaction xiat the time between ti−1and ti (inclusive), (2) xibecomes enabled at some point between
ti−2and ti−1, and is disabled at ti, and (3) xi 6= xi+1for each i > 0. Suppose that xiis disabled due to
the execution of some interaction yi. Since xi+1remains enabled while yi is executed, Pxi+1∩ Pyi = ∅.
That is, the enabledness of xi+1(due to the readiness of some processes in Pxi+1) is independent of the execution of yi.
Consider the runψ0 obtained fromψ by deferring, for each i, the enabledness of xi+1 until yi is
executed. Then,ψ ≡ ψ0. Note that the transformation fromψ to ψ0does not cause any new interaction to be enabled, nor does it extend the duration of an interaction’s enabledness. So the transformation cannot cause any new process to be continuously ready for an enabled interaction. However, for each i , right after yi is executed inψ0, p is not ready for xi+1 (and not ready for xi either). If there exist
infinitely many i ’s such that p is not ready for any interaction immediately after each yi is executed,
then p is not continuously ready for an enabled interaction. Otherwise, there exists some i0 such that for all i≥ i0there still exists another interaction xi0+1which remains enabled right after yiis executed.
We can also use the above method again to break the overlap of the enabledness of xi and xi0+1. Since
there is only a finite number of interactions, we can obtain a run equivalent toψ such that p is not continuously ready for an enabled interaction.
Similarly, if there is some other process q inψ0 (and thus inψ) that is continuously ready for an enabled interaction, then we can use the same method again to transformψ0intoψ00so that q is not continuously ready for an enabled interaction. Since there are only a finite number of processes, we can transformψ into an equivalent run satisfying WPF. Therefore, for every run ψ ∈ WIF(IS) − WPF(IS), eq(ψ) ∩ WPF(IS) 6= ∅. j
We have finished the comparison of SG+with the four fairness notions SIF, SPF, WPF, and WIF, and their minimal/maximal completions. The following theorem summarizes the results.
THEOREM4.8. LetIS = (P, IB,M∀) be a given biparty interaction system. Then the following relation holds:
SIF−(IS) ⊆ SIF(IS) ⊆ SIF+(IS) = SG+(IS) = SPF−(IS) = SPF(IS) = SPF+(IS)
⊆ WPF−(IS) ⊆ WPF(IS) ⊆ WPF+(IS) = WIF(IS).
In particular, there exists anIS for which all the stronger-than relations “⊆” become strict.
Figure 7a depicts the relationship between these fairness notions. In this figure A→ B means A is stronger than B. The relation “→” is transitive. Note that since SG+is the strongest implementable and
FIG. 7. The hierarchy of various fairness notions when interactions cannot contain interactions. The fairness notions in boldface are implementable, while the others are not.
equivalence-robust fairness notion, all fairness notions weaker than SG+are also implementable, and all equivalence-robust fairness notions stronger than SG+, e.g., SIF−, are unimplementable. Moreover, although SIF is not equivalence-robust, as we have seen in Part I, it is also unimplementable.
EXAMPLE. Consider the Producers–Consumers problem, in which there are two producers producer1 and producer2and two consumers consumer1and consumer2. The data produced by a producer can be consumed by either of the consumers. The following is a CSP program for the problem, where i = 1, 2:
produceri :: compute(data);
* [ consumer1! data−→ compute(data) 2 consumer2! data−→ compute(data) ] consumeri :: * [ producer1? data−→ digest(data)
2 producer2? data−→ digest(data) ]
There are four biparty interactions in this program, each of which involves a producer and a consumer. They have the structure shown in Fig. 6a. So by our results in this section, the stronger-than relations (i.e., the arrow→) in Fig. 7a are all strict; that is, for this problem
SIF−(IS) ( SIF(IS) ( SG+(IS) ( WPF−(IS) ( WPF(IS) ( WIF(IS).
Therefore, any implementation of CSP’s input/output guards which guarantees only WIF cannot prevent the following behavior, which continuously blocks producer1from sending its data to either consumer and so does not satisfy WPF (although it does satisfy WIF):
all processes are ready (for communication/interaction), and then the repeat of the following forever producer2sends data to consumer1
producer2 and consumer1 ready producer2sends data to consumer2 producer2 and consumer2 ready . . .
Similarly, the following behavior which satisfies WIF and WPF but does not satisfy WPF−and SPF is also possible:
all processes are ready, and then the repeat of the following forever producer2sends data to consumer1
producer2ready
producer2sends data to consumer2 producer2ready
consumer1and consumer2ready . . .
In the absence of consumer1 (say, it terminates prematurely), the following scenario which satisfies WIF, WPF, and WPF−but not SPF is also possible:
all processes are ready, and then the repeat of the following forever producer2sends data to consumer2
producer2and consumer2ready . . .
Since in the biparty case SPF (which is equivalent to SG+) is implementable, a good implementation should be able to avoid all the above unfair scenarios. On the other hand, since SPF is also the strongest implementable and equivalence-robust fairness notion, the strongest equivalence-robust property one can observe from the program executing in any asynchronous environment is that no process is forever blocked from communicating with its partners if it has infinitely many such opportunities.
4.2. Multiparty Interaction Systems
We now consider multiparty interactions of arbitrary arity. Recall that in Theorem 4.8 the following relations hold as well even if interactions are multipartied (but cannot contain interactions):
1. SIF−(IS) ⊆ SIF(IS) ⊆ SIF+(IS) = SG+(IS) = SPF+(IS) 2. SIF(IS) ⊆ SPF(IS)
3. SPF−(IS) ⊆ WPF−(IS) ⊆ WPF(IS) ⊆ WPF+(IS) = WIF(IS) 4. SPF+(IS) ⊆ WPF+(IS).
Since SPF becomes non-equivalence-robust in the multiparty case, we need to resolve the relationship between its completions and the other fairness notions.
LEMMA4.9. For everyIS = (P, I, M∀), SPF−(IS) ⊆ SPF(IS) ⊆ SPF+(IS). In particular, SPF− (IS) ( SPF(IS) ( SPF+(IS) if ∃ x, y, z ∈I, ∃ p1, p2, p3∈ Pxsuch that (1) p1∈ Px− Py− Pz, p2∈ Pz− Pyand p3∈ Py− Pzand (2)∀u ∈I, p1∈ Pu ⇒ (Pu 6⊆ (Px− Pz)∪ Py) and (Pu6⊆ (Px− Py)∪ Pz).
Proof. To see the proper subset conditions, it suffices to find a runπ ∈ SPF(IS) such that some run equivalent toπ does not satisfy SPF. Consider the run
π = ((Px− Pz)∪ Py)(y Pzz Py)ω.
Due to the two conditions p2∈ Px∩ Pz− Pyand p3∈ Px∩ Py− Pz, x is never enabled inπ. So if no
other interaction is enabled infinitely often but is never executed, thenπ ∈ SPF(IS). Moreover, the run ρ = ((Px− Pz)∪ Py)((Pz− Py) y (Pz∩ Py) z Py)ω
is equivalent toπ but x is now enabled just before each instance of y is to be executed. So p1, which belongs to Px, is now ready for an enabled interaction infinitely often. Since p1 never executes any interaction,ρ 6∈ SPF(IS).
Ifπ 6∈ SPF(IS), then some interaction w is enabled infinitely often but some process q in Pwnever executes any interaction. Then either Pw⊆ (Px− Py)∪ Pzor Pw⊆ (Px− Pz)∪ Py. Due to condition (2)
imposed onIS, p16∈ Pw. Assume that Pw⊆ (Px− Py)∪ Pz. (The other case can be proved similarly.)
Then in the run
π0= ((P
x− Pz)∪ Py)(y PzwPwz Py)ω
q has executedw infinitely often. So either π0∈ SPF(IS), or similarly there exists another interaction u, u 6= w, such that u is enabled infinitely often but some process in Punever executes any interaction. In
the former case, we can find a runρ0similar toρ such that ρ0≡ π0butρ0does not satisfy SPF because p1 is infinitely often ready for an enabled interaction (i.e., x) but it never engages in any interaction. In the latter case, given thatIandPare finite, we can use the above method repeatedly to find two equivalent runs such that one satisfies SPF while the other does not. j
Figure 8 illustrates some instances ofIS for which SPF is not equivalence-robust. Note that all of them consists of a multiparty interaction involving more than two processes.
LEMMA4.10. For everyIS = (P, I, M∀), SIF−(IS) ⊆ SPF−(IS). In particular, SIF−(IS) ( SPF−(IS) if∃ x, y1, . . . , yn ∈Isuch that∀i ≤ n, Pyi∩ Px 6= ∅ and
S
i(Pyi ∩ Px)= Px.
Proof. Since SIF(IS) ⊆ SPF(IS), SIF−(IS) ⊆ SPF−(IS). To see the proper subset condition, recall the following run in Lemma 4.2,
π =¡Py1∪ · · · ∪ Pyn
¢¡
y1Py1· · · ynPyn
¢ω
,
which is in SPF(IS) − SIF(IS). So π 6∈ SIF−(IS) either. Since every process in π executes some interaction yi infinitely often, eq(π) ⊆ SPF−(IS). So π ∈ SPF−(IS) − SIF−(IS). j
Figure 4 also illustrates some instances ofIS for which SIF−(IS) ( SPF−(IS).
LEMMA4.11. There exists a systemIS = (P, I, M∀), where ∀x, y ∈I, x 6= y ⇒ Px 6⊆ Py, such that
SIF(IS) 6⊆ SPF−(IS) and SPF−(IS) 6⊆ SIF(IS).
Proof. LetIS be the interaction system withPandIshown in Fig. 9. Consider the run π1= p5( p1p3x13p2p4x24)ω.
Thenπ1∈ SIF(IS). However, π16∈ SPF−(IS) because its equivalent run π2= p5( p1p3p2p4x13x24)ω
does not satisfy SPF due to the fact that p5is now ready for an enabled interaction (i.e., x345) infinitely often but it never executes any interaction. So SIF(IS) 6⊆ SPF−(IS).
On the other hand, the run
ρ = (p1p3p2p4x13x24)ω
and all of its equivalent runs satisfy SPF, and so they also satisfy SPF−. However,ρ 6∈ SIF(IS) because x12is enabled infinitely often but is never executed. So SPF−(IS) 6⊆ SIF(IS). j
LEMMA4.12. There exists a systemIS = (P, I, M∀), where∀x, y ∈I, x6= y ⇒ Px6⊆ Py, such that
1. SG+(IS) 6⊆ WPF(IS) and WPF(IS) 6⊆ SG+(IS) and 2. SG+(IS) 6⊆ WPF−(IS) and WPF−(IS) 6⊆ SG+(IS).
Proof. LetIS be the interaction system withPandIshown in Fig. 10. Consider the two runs π1= p5( p1p3x13p2p4x24p6p8x68p7p9x79)ω
π2= p5p1p3p2p4p6p8p7p9(x13p1p3x24p2p4x68p6p8x79p7p9)ω.
![FIG. 2. The fairness-equivalence partitioning [3].](https://thumb-ap.123doks.com/thumbv2/9libinfo/8859269.244691/3.918.294.636.87.329/fig-the-fairness-equivalence-partitioning.webp)
