An Algorithm for Ensuring Fairness and Liveness in Non-deterministic Systems Based on Multiparty Interactions

An Algorithm for Ensuring Fairness and Liveness in Non-deterministic Systems Based on Multiparty Interactions David Ruiz, Rafael Corchuelo, Jos´eA.P´erez, and Miguel Toro Universidad de Sevilla, E. T. S. Ingenieros Inform´aticos, Av. de la Reina Mercedes s/n, Sevilla, E–41012, Spain [email protected], http://tdg.lsi.us.es Abstract. Strong fairness is a notion we can use to ensure that an element that is enabled infinitely often in a non–deterministic programme, will eventually be selected for execution so that it can progress. Unfortunately, “eventually” is too weak to induce the intuitive idea of liveliness and leads to anomalies that are not desirable, namely fair finiteness and conspiracies. In this paper, we focus on non–deterministic programmes based on multiparty interactions and we present a new criteria for selecting interactions called strong k–fairness that improves on other proposals in that it addresses both anomalies simultaneously, and kmay be set a priori to control its goodness. We also show our notion is feasible, and present an algorithm for scheduling interactions in a strongly k–fair manner using a theoretical framework to support the multiparty interaction model. Our algorithm does not require to transform the source code to the processes that compose the system; furthermore, it can deal with both terminating and non–terminating processes. 1 Introduction Fairness is an important liveliness concept that becomes essential when the execution of a programme is non–deterministic [8]. This may be a result of the inherently non–deterministic constructs that the language we used to code it offers, or a result of the interleaving of atomic actions in a concurrent and/or distributed environment. Intuitively, an execution of a programme is fair iff every element under consideration that is enabled sufficiently often is executed sufficiently often, which prevents undesirable executions in which an enabled element is neglected forever. The elements under consideration may range from alternatives in a non– deterministic multi–choice command to high–level business rules, and combined with a precise definition of “sufficiently often” lead to a rich lattice of fairness notions that do not collapse, i.e., are not equivalent each other [3]. This article was supported by the Spanish Interministerial Commission on Science and Technology under grant TIC2000-1106-C02-01. There is not a prevailing definition, but many researchers agree in that so called strong fairness deserves special attention [8] because it may induce termination or eventual response to an event. Technically, an execution is said to be strongly fair iff every element that is enabled indefinitely often is executed infinitely often, i.e., it prevents elements that are enabled infinitely often, but not necessarily permanently, from being neglected forever. In this paper, we focus on concurrent and/or distributed programmes that use the multiparty interaction model as the sole means for process1synchroni- sation and communication. This interaction model is used in several academic programming languages like Scripts [8], Raddle [7] or IP [9] and in commercial programming environments like Microsoft .NET Orchestration [4] too. In this paper, we focus on IP because it is intended to have a dual role: on the one hand, it is intended to be a distributed system specification language equipped with sound semantics that turn it into a language amenable to formal reasoning, a rather important property; on the other hand, it is intended to be an assembler language supporting more sophisticated high–level specification languages such as LOTOS, ESTELLE, SDL [10] or CAL [5]. Next, we report on those issues, present some approaches to address them and give the reader a bird’s–eye view of the rest of the paper. 1.1 Known Issues Figure 1 shows a solution to the well–known dining philosophers problem in IP. This classic multi-process synchronisation problem consists of five philosophers sitting at a table who do nothing but think and eat. There is a single fork between each philosopher, and they need to pick both forks up in order to eat. In addition, each philosopher should be able to eat as much as the rest, i.e., the whole process should be fair. This problem is the core of a large class of problems where a process needs to acquire a set of resources in mutual exclusion. Getiand Relidenote a number of three–party interactions that allow each philosopher Pito get its corresponding forks Fiand Fi+1 mod Nin mutual exclusion with its neighbours (i=1,2,...,N). For an interaction to become enabled, the set of processes that may eventually ready it, i.e., may eventually be willing to participate in the joint action it represents, need to be readying it simultaneously. The only way to ensure that every philosopher that is hungry will eventually eat is by introducing a notion of fairness in the implementation of the language. However, strong fairness is not practical enough because of the following inherent problems: Fair Finiteness: Every finite execution is strongly fair by definition. Figure 2.a shows a simple execution trace of an instantiation of the preceding programme in which N= 5. The notation p.χ means that process preadies the 1The term process refers to any autonomous, single–threaded computing artefact. It may be a process in an operating system, a thread, or even a hardware device. get 2 rel 2 get 3 rel 3 get 4 rel 4 get 5 rel 5 get 1 rel 1 P 1 P 2 P 3 P 4 P 5 F 1 F 5 F 4 F 3 F 2 N=5 S::[N i=1FiN i=1Ti] Pi:: *[Geti[] →eat; Reli[]; think] Fi:: *[ Geti[] →Reli[] [] Get(i+1 mod N)[] →Rel(i+1 mod N)[] ] (a) (b) Fig. 1. A solution to the dining philosophers problem in IP. set of interactions χ. Notice that for any finite n, this execution is technically strongly fair, despite Get2being enabled ntimes but never selected. If n= 10, this execution may be considered fair from an intuitive point of view, but if n= 1000 it is not so intuitive to consider this behaviour fair. Conspiracies: It does not take into account conspiracies in which an interaction never gets enabled because of an unfortunate interleaving of independent atomic actions. For instance, the execution shown in Figure 2.b is strongly fair for any n≥0, but notice that due to an unfortunate interleaving, interaction Get2is never readied by all of its participants at the same time and thus never gets enabled. The above problems show that strong fairness (and other notions that rely on infiniteness and eventuality) fails to capture the intuitive idea of inducing liveliness. Although it may be the only way to proof termination or eventual response to an event during an infinite execution, “eventual” is usually too weak for practical purposes because any practical running programme must necessarily stop or be stopped a day. 1.2 Related Work These issues motivated several authors to research stronger notions. Here we focus on two approaches called strong finitary fairness [1] and hyperfairness [2]. An execution is strongly finitarily fair iff there exists a natural number k (not known a priori) such that every interaction that is enabled infinitely often is executed at least every ksteps. Although this notion introduces additional liveliness because it bounds the number of times an enabled interaction may be neglected, it has several drawbacks: (i) kis not known a priori, and thus it cannot be used to fine-tune a potential scheduler depending on the nature of the system it is scheduling; (ii) it does not prevent unfair finiteness; (iii) it does not prevent conspiracies; and, to the best of our knowledge, (iv) no general algorithm implementing it has been produced. (The authors do only present a P1.{Get1},P 2.{Get2}, (P5.{Get5, Get1},P 2.{Get2, Get3},P 1.{Get1, Get2}, Get1[], P1.{Rel1},P 1.{Rel1,Rel 2},P 5.{Rel5,Rel 1},Rel 1[],P 1.{Get1})n (a) P1.{Get1},P 2.{Get2}P3.{Get3}, (P5.{Get5, Get1},P 3.{Get3, Get4}, P1.{Get1, Get2}, Get1[],P 2.{Get2, Get3}, Get3[],P 1.{Rel1}, P1.{Rel1,Rel2},P 5.{Rel5,Rel 1},Rel 1[],P 3.{Rel3}, P2.{Rel2,Rel 3},P 3.{Rel3,Rel 4},Rel 3[],P 1.{Get1},P 3.{Get3})n (b) Fig. 2. Strong fairness anomalies. transformational approach suitable to be used in the context of B¨uchi automata [12,11].) Hyperfairness also deserves attention because it alleviates the second problem. Technically, an execution is hyperfair iff it is finite or every interaction that may get enabled infinitely often, becomes enabled infinitely often. It is important to notice that this definition diverges from classical notions in that the latter imply eventual execution of an interaction if it gets enabled sufficiently often, whereas hyperfairness does only imply eventual enablement. Subsequent execution is under the criterion of an implied underlying classical fairness notion. Thus, this notion prevents conspiracies due to unfortunate interleaving of independent atomic actions but combined with finitary or strong fairness suffers from fair finiteness. To the best of our knowledge, no general algorithm able to implement hyperfairness has been produced. However, the authors presented a transformational approach by means of which we can transform an IP programme into an equivalent strongly hyperfair form, which implies modification of the source code and creation of explicit schedulers for each programme. This may be acceptable in the context of research languages, but it is not practical enough in real–world languages in which processes or components are available only in binary form and need to be scheduled without any knowledge of their internal details. Furthermore, it does not address the issue of fair finiteness. 1.3 Overview In this paper, we present a new notion called strong k–fairness that solves fair finiteness and conspiracies. Intuitively, an execution is strongly k–fair iff no interaction is executed more than ktimes unless the set of interactions that share processes with it is stable, i.e., the processes that participate in them are waiting for interaction or finished, and it is the oldest in the group, i.e., the one that has not been executed for a longer period of time. We present a theoretical interaction framework to formalize the multiparty interaction model. Furthermore, we present an algorithm that uses this frame- work for scheduling interactions in a strongly k–fair manner, and it is not dependent on the internal details of the processes that compose the system, i.e., it is not a transformational approach. The succeeding sections are organised as follows: Section 2 presents our theoretical interaction framework; Section 3 presents a formal definition of strong k–fairness; Section 4 describes a scheduler we can use to implement this notion; finally, Section 5 reports on our main conclusions. 2 A Theoretical Framework to Support the Multiparty Interaction Model Next, we present a formal definition of our abstract interaction framework. Definition 1 (Static Characterisation of a System) A system Σisa2– tuple (PΣ,I Σ)in which PΣ=∅is a finite set of autonomous processes and IΣ= ∅is a finite set of interactions. We denote the set of processes that may eventually ready interaction xas P(x)(participants of interaction x). A configuration is a mathematical object that may be viewed as a snapshot of a system at run time. We denote them as C, C,C 1,C 2... An event is a happening that induces a system to transit from a configuration to another. In our model, we take into account the following kinds of events: p.ι, which indicates that process pexecutes an atomic action that does only involve its local data; p.χ, which indicates that process pis readying the interactions in set χ(notice that when χ=∅, process parrives at a fixed point that we may interpret as its termination); and x, which indicates that interaction xhas been selected and the processes participating in it can execute the corresponding joint action atomically. Definition 2 (Dynamic Characterisation of a System) An execution of a system Σis a 3–tuple (C0,α,β)in which C0denotes its initial configuration, α=[C1,C 2,C 3,...]is a maximal (finite or infinite) sequence of configurations through which it proceeds, and β=[e1,e 2,e 3,...]is a maximal (finite or infinite) sequence of events responsible for the transition between every two consecutive configurations. Obviously |α|=|β|. Finally, let λ=(C0,α,β)be an execution of system Σ.Wecallαits configuration trace and denote it as λα, and βits event trace and denote it as λβ. We denote the rule that captures the underlying semantics that control the transition between configurations as L. For instance, CeLCindicates that the system may transit from configuration Cto configuration C on occurrence of event e. Thus, given an execution λ=(C0,[C1,C 2,C 3,...], [e1,e 2,e 3,...]), we usually write it as2:C0e1LC1e2LC2e3L··· 2Notice that the exact formulation of Ldepends completely on the language in which the system under consideration was written. Definition 3 (Static Characterisation of a Process) Process pis waiting a interaction set Υat the i–th configuration in execution λiff it has arrived at a point in its execution in which executing any x∈Υis one of its possible continuations. Process pis finished at the i–th configuration in execution λiff it can neither execute any local computation nor any interaction. Waiting(λ, p, Υ, i)⇐⇒ ∃ k∈[1..i]·β(k)=p.χ ∧Υ⊆χ∧j∈[k+1..i]·β(j)=x∧x∈χ Finished(λ, p, i)⇐⇒ ∃ k∈[1..i]·β(k)=p.∅ (1) Definition 4 (Static Characterisation of an Interaction) Interaction x is enabled at the i–th configuration in execution λiff all of the processes in P(x)are readying xat that configuration. Interaction xis stable at the i–th configuration in execution λiff it is either enabled or disabled at that configuration. Enabled(λ, x, i)⇐⇒ ∀ p∈P(x)·Waiting(λ, p, {x},i) Stable(λ, x, i)⇐⇒ ∀ p∈P(x)·∃Υ⊆IΣ·Waiting(λ, p, Υ, i) (2) Definition 5 (Dynamic Characterisation of an Interaction) The set of interactions linked to interaction xat the i–th configuration in execution λis the set of interactions such that there exists a process that is readying xand any of those interactions simultaneously. We define the execution set of interaction xat the i–th configuration in execution λas the set of indices up to ithat denote the configurations at which interaction xhas been executed. Linked(λ, x, i)= {y∈IΣ·∃p∈PΣ·Waiting(λ, p, {x, y},i)} ExeSet(λ, x, i)= {k≤i·β(k)=x} (3) 3 Strong k–Fairness Intuitively, an execution is strongly k–fair iff no interaction is executed more than ktimes unless all of the interactions that are linked to it when it is executed are stable and it is the oldest amongst them. Definition 6 (Strongly k–Fair Execution) Let λ=(C0,α,β)be an execution of a system, and ka non–null natural number. λis strongly k–fair iff predicate SKF(λ, k)holds. SKF(λ, k)⇐⇒ ∀ x∈IΣ,i∈ExeSet(λ, x, ∞)·Enabled(λ, x, i)∧ (LStable(λ, x, i)∧LOldest(λ, x, i)∨ ¬LStable(λ, x, i)∧∆(λ, x, i)≤k) (4) This definition relies on a number of auxiliary predicates and functions we have introduced for the sake of simplicity. LStable is a predicate we use to determine if an interaction and those that are linked to it are stable at a given configuration in an execution. Its formal definition follows: LStable(λ, x, i)⇐⇒ ∀ y∈Linked(λ, x, i)∪{x}·Stable(λ, y, i)(5) LOldest is a predicate we use to determine if an interaction is older than any of the interactions to which it is linked or, in the worst case, is the same age. Its definition follows: LOldest(λ, x, i)⇐⇒ ∀ y∈Linked(λ, x, i)·Age(λ, x, i)≥Age(λ, y, i) (6) The age of an interaction is the number of configurations that have elapsed since it was executed for the last time, or ∞if it has never been executed so far. Age(λ, x, i)=i−max ExeSet(λ, x, i) if ExeSet(λ, x, i)=∅ ∞otherwise (7) ∆is a function that maps an event trace, an interaction and an index into the number of times it has executed in the presence of a non–empty set of linked interactions that was not stable. Its definition follows: ∆(λ, x, i)=  φ≤k<i (λβ(k)=x∧Linked(λ, x, k)=∅∧¬LStable(λ, x, k)) (8) where denotes the counter quantifier ( a∈A P(a)|{a∈A·P(a)}|), and φis defined as follows (notice that we denote the maximum of an empty set as ⊥): φjif j= max{k∈ExeSet(λ, x, i)·LStable(λ, x, k)}∧j=⊥ 1 otherwise (9) 4 A Strongly k–Fair Scheduler Our algorithm is based on previous proposals which want to resolve another problems in the context of the multiparty interactions [6,14,13]. The idea behind our algorithm for scheduling interactions in a strongly k–fair manner consists of arranging the set of interactions into a queue τso that the closer an interaction is to the rear, the less time has elapsed since it was executed for the last time. Furthermore, each interaction has an associated counter δwe use to count how many times it has been semi–enabled in presence of linked interactions. To know the state in which a process or an interaction is, we use a map ϕ from the set of interactions into the set of processes that are readying it. We update it each time the selection module detects a transition p.χLoccurs, or an interaction is executed. Our algorithm selects for execution interaction xas long as it is the first enabled one in queue τ, and the set of interactions linked to it is stable. We describe the operational semantics of our strong k–fairness algorithm using transition rule SKF on configurations D,D,D 1,.... These configurations are composed of the configuration Cof the programme and the data structures we need to select interactions. Next, we define theses data structures and the functions that allows us to update it. The extended configurations on which our algorithm works are of the form (τ, ϕ, δ, ϑ), where τis an interaction queue, ϕis a readiness map, δis a semi– enablement map, and ϑdenotes the set of processes that are finished. Definition 7 (Data Structures) ϕdenotes a map from interactions into sets of processes. ϕ(x)denotes the set of processes that are readying x.ϑ⊆PΣ denotes the set of processes that are finished, i.e., can neither execute local computations nor ready any interaction. δis a map from the set of interactions into the set of natural numbers. δ(x)denotes the number of times any interaction linked to xhas been executed while xwas semi–enabled. The higher δ(x)is, the higher the probability of conspiracy is. τdenotes a queue in which the set of interactions has been arranged so that the closer they are to the rear, the less time has elapsed since they were executed for the last time. As usual, we consider a queue of interactions is a map from a subset of natural numbers into the set of interactions. The initial extended configuration of our algorithm is of the form (τ0,ϕ 0, δ0,ϑ 0). It does not matter the order in which interactions are initially arranged into τ,butϕ0must satisfy that ∀x∈dom ϕ0·ϕ0(x)=∅,δ0must satisfy that ∀x∈dom δ0·δ0(x)=0,andϑ0=∅. Definition 8 (Functions) When process preadies a set of interactions χ,we use function AddOffer(ϕ, p, χ)to update map ϕ, and when interaction xis executed, we use function RemoveOffer(ϕ, x). By definition, process pfinishes when it readies an empty set of interactions, and function AddFinished(ϑ, p)updates map ϑ. When interaction xis selected for execution, we use function Order to move it to the rear of τ, not necessarily to the last position. When interaction x is selected for execution, we use function Update(ϕ, δ, x)to create a new semi– enablement. Predicate Stabilised(Υ, ϕ, ϑ)holds iff all of the processes that may eventually ready an interaction in Υhas readied it or are finished. EnblDisj(τ,ϕ) denotes the set of interactions that are enabled and it does not exists any preceding interaction in τthat is enabled and linked to them. AddOffer(ϕ, p, χ)={x→ ϕ(x)·x∈dom ϕ∧x∈ χ}∪ {x→ ϕ(x)∪{p}·x∈dom ϕ∧x∈χ} RemoveOffer(ϕ, x)={x→ ϕ(x)\P(x)·x∈dom ϕ} AddFinished(ϑ, p)= ϑ∪{p}if χ=∅ ϑif χ=∅ Order(τ, δ)=τ⇔dom τ= dom τ∧ran τ= ran τ∧ ∀x1,x 2∈ran τ·(τ−1(x1)≤τ−1(x2)⇒δ(x1)≥δ(x2)) Update(ϕ, δ, x)=δ⊗{x→ 0}⊗{y→ δ(y)+1·y∈S\{x}∧¬Stabilised(S,ϕ,ϑ)} Stabilised(Υ, ϕ, ϑ)⇔∀x∈Υ·∀p∈P(x)·p∈ran ϕ∨p∈ϑ EnblDisj(τ, ϕ)={x∈dom ϕ·P(x)=ϕ(x)∧y∈S·P(y)=ϕ(y)∧τ−1(y)<τ −1(x)} (10) where S{z∈dom ϕ·ϕ(z)∩ϕ(x)=∅}. Our algorithm is formally defined by means of the inference rules presented in Figure 3. Rule 11 is straightforward because it describes how the data structures are updated each time process preadies a set of interactions χ. Rule 12 describes which interaction must be selected so that the execution is strongly k–fair. The antecedent is complex, but the reasoning behind it is quite simple. Assume xis an enabled interaction and there is not a conflicting enabled interaction before xin queue τ, i.e., x∈EnblDisj(τ,ϕ); in this context xis selected for execution iff any of the following three conditions hold: Cp.χLC∧ ϕ= AddOffer(ϕ, p, χ)∧ϑ= AddFinished(ϑ, p) (C, τ, ϕ, δ, ϑ)p.χSKF (C,τ,ϕ δ, ϑ)(11) x∈EnblDisj(τ, ϕ)∧S={z∈dom ϕ·(ϕ(z)∩ϕ(x)=∅)}∧ τ= Order(τ, δ)∧ϕ= RemoveOffer(ϕ, x)∧δ= Update(ϕ, δ, x)∧ (S={x}∨Stabilised(S,ϕ,ϑ)∨(S ={x}∧ max y∈S\{x}δ(y)<k)) (C, τ, ϕ, δ, ϑ)xSKF (C,τ,ϕ ,δ ,ϑ)∧CxLC(12) Fig. 3. Algorithm for strongly k–fair scheduler. 1. It is not conflicting with other interactions (S={x}). 2. The interactions which it is conflicting with are stabilised, i.e., all of their participants are readying it or finished (Stabilised(S,ϕ,ϑ)). 3. The semi–enablement counter associated with each conflicting interaction is less than k(S ={x}∧ max y∈S\{x}δ(y)<k). 5 Conclusions and Future Work In this paper, we have presented strong k–fairness in the context of concurrent and/or distributed programmes in which multiparty interaction models are the sole mean for process synchronisation and communication. An important contribution is the concept of semi–enablement that we use to forecast conspiracies and solve them. kcan thus be viewed as a semi–enablement threshold that characterises the goodness of our notion because it makes our selection criterion more or less demanding. If kis minimum, the pace at which conflicting interactions are executed depends then on the participant that spends more time at doing local computations because, in this case, no interaction can be selected for execution unless the set of potentially conflicting interactions is consolidated. If k is very distant from its minimum, the algorithm introduces little delay because interactions may be scheduled as soon as they are enabled. The exact choice of kdepends on the features of the programme under consideration and can only be tuned by means of experimentation.