An Algo i hm o Ensu ing Fai ness
and Li eness in Non-de e minis ic Sys ems
Based on Mul ipa y In e ac ions
Da id Ruiz, Ra ael Co chuelo, Jos´eA.P´e ez, and Miguel To o
Uni e sidad de Se illa, E. T. S. Ingenie os In o m´a icos,
A . de la Reina Me cedes s/n, Se illa, E–41012, Spain
[email p o ec ed], h p:// dg.lsi.us.es
Abs ac . S ong ai ness is a no ion we can use o ensu e ha an ele-
men ha is enabled infini ely o en in a non–de e minis ic p og amme,
will e en ually be selec ed o execu ion so ha i can p og ess. Un o u-
na ely, “e en ually” is oo weak o induce he in ui i e idea o li eliness
and leads o anomalies ha a e no desi able, namely ai fini eness and
conspi acies. In his pape , we ocus on non–de e minis ic p og ammes
based on mul ipa y in e ac ions and we p esen a new c i e ia o selec -
ing in e ac ions called s ong k– ai ness ha imp o es on o he p oposals
in ha i add esses bo h anomalies simul aneously, and kmay be se a
p io i o con ol i s goodness. We also show ou no ion is easible, and
p esen an algo i hm o scheduling in e ac ions in a s ongly k– ai man-
ne using a heo e ical amewo k o suppo he mul ipa y in e ac ion
model. Ou algo i hm does no equi e o ans o m he sou ce code o
he p ocesses ha compose he sys em; u he mo e, i can deal wi h
bo h e mina ing and non– e mina ing p ocesses.
1 In oduc ion
Fai ness is an impo an li eliness concep ha becomes essen ial when he ex-
ecu ion o a p og amme is non–de e minis ic [8]. This may be a esul o he
inhe en ly non–de e minis ic cons uc s ha he language we used o code i
offe s, o a esul o he in e lea ing o a omic ac ions in a concu en and/o
dis ibu ed en i onmen .
In ui i ely, an execu ion o a p og amme is ai iff e e y elemen unde con-
side a ion ha is enabled sufficien ly o en is execu ed sufficien ly o en, which
p e en s undesi able execu ions in which an enabled elemen is neglec ed o -
e e . The elemen s unde conside a ion may ange om al e na i es in a non–
de e minis ic mul i–choice command o high–le el business ules, and combined
wi h a p ecise defini ion o “sufficien ly o en” lead o a ich la ice o ai ness
no ions ha do no collapse, i.e., a e no equi alen each o he [3].
This a icle was suppo ed by he Spanish In e minis e ial Commission on Science
and Technology unde g an TIC2000-1106-C02-01.
The e is no a p e ailing defini ion, bu many esea che s ag ee in ha so
called s ong ai ness dese es special a en ion [8] because i may induce e -
mina ion o e en ual esponse o an e en . Technically, an execu ion is said o
be s ongly ai iff e e y elemen ha is enabled indefini ely o en is execu ed
infini ely o en, i.e., i p e en s elemen s ha a e enabled infini ely o en, bu
no necessa ily pe manen ly, om being neglec ed o e e .
In his pape , we ocus on concu en and/o dis ibu ed p og ammes ha
use he mul ipa y in e ac ion model as he sole means o p ocess1synch oni-
sa ion and communica ion. This in e ac ion model is used in se e al academic
p og amming languages like Sc ip s [8], Raddle [7] o IP [9] and in comme cial
p og amming en i onmen s like Mic oso .NET O ches a ion [4] oo. In his
pape , we ocus on IP because i is in ended o ha e a dual ole: on he one hand,
i is in ended o be a dis ibu ed sys em specifica ion language equipped wi h
sound seman ics ha u n i in o a language amenable o o mal easoning, a
a he impo an p ope y; on he o he hand, i is in ended o be an assemble
language suppo ing mo e sophis ica ed high–le el specifica ion languages such
as LOTOS, ESTELLE, SDL [10] o CAL [5]. Nex , we epo on hose issues,
p esen some app oaches o add ess hem and gi e he eade a bi d’s–eye iew
o he es o he pape .
1.1 Known Issues
Figu e 1 shows a solu ion o he well–known dining philosophe s p oblem in IP.
This classic mul i-p ocess synch onisa ion p oblem consis s o fi e philosophe s
si ing a a able who do no hing bu hink and ea . The e is a single o k
be ween each philosophe , and hey need o pick bo h o ks up in o de o ea .
In addi ion, each philosophe should be able o ea as much as he es , i.e., he
whole p ocess should be ai . This p oblem is he co e o a la ge class o p oblems
whe e a p ocess needs o acqui e a se o esou ces in mu ual exclusion.
Ge iand Relideno e a numbe o h ee–pa y in e ac ions ha allow each
philosophe Pi o ge i s co esponding o ks Fiand Fi+1 mod Nin mu ual exclu-
sion wi h i s neighbou s (i=1,2,...,N). Fo an in e ac ion o become enabled,
he se o p ocesses ha may e en ually eady i , i.e., may e en ually be willing
o pa icipa e in he join ac ion i ep esen s, need o be eadying i simul ane-
ously.
The only way o ensu e ha e e y philosophe ha is hung y will e en ually
ea is by in oducing a no ion o ai ness in he implemen a ion o he language.
Howe e , s ong ai ness is no p ac ical enough because o he ollowing inhe en
p oblems:
Fai Fini eness: E e y fini e execu ion is s ongly ai by defini ion. Figu e
2.a shows a simple execu ion ace o an ins an ia ion o he p eceding p o-
g amme in which N= 5. The no a ion p.χ means ha p ocess p eadies he
1The e m p ocess e e s o any au onomous, single– h eaded compu ing a e ac . I
may be a p ocess in an ope a ing sys em, a h ead, o e en a ha dwa e de ice.
ge
2
el
2
ge
3
el
3
ge
4
el
4
ge
5
el
5
ge
1
el
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:: *[Ge i[] →ea ; Reli[]; hink]
Fi::
*[ Ge i[] →Reli[]
[] Ge (i+1 mod N)[] →Rel(i+1 mod N)[]
]
(a) (b)
Fig. 1. A solu ion o he dining philosophe s p oblem in IP.
se o in e ac ions χ. No ice ha o any fini e n, his execu ion is echni-
cally s ongly ai , despi e Ge 2being enabled n imes bu ne e selec ed.
I n= 10, his execu ion may be conside ed ai om an in ui i e poin o
iew, bu i n= 1000 i is no so in ui i e o conside his beha iou ai .
Conspi acies: I does no ake in o accoun conspi acies in which an in e ac-
ion ne e ge s enabled because o an un o una e in e lea ing o independen
a omic ac ions. Fo ins ance, he execu ion shown in Figu e 2.b is s ongly
ai o any n≥0, bu no ice ha due o an un o una e in e lea ing, in e -
ac ion Ge 2is ne e eadied by all o i s pa icipan s a he same ime and
hus ne e ge s enabled.
The abo e p oblems show ha s ong ai ness (and o he no ions ha ely
on infini eness and e en uali y) ails o cap u e he in ui i e idea o inducing
li eliness. Al hough i may be he only way o p oo e mina ion o e en ual
esponse o an e en du ing an infini e execu ion, “e en ual” is usually oo weak
o p ac ical pu poses because any p ac ical unning p og amme mus necessa ily
s op o be s opped a day.
1.2 Rela ed Wo k
These issues mo i a ed se e al au ho s o esea ch s onge no ions. He e we
ocus on wo app oaches called s ong fini a y ai ness [1] and hype ai ness [2].
An execu ion is s ongly fini a ily ai iff he e exis s a na u al numbe k
(no known a p io i) such ha e e y in e ac ion ha is enabled infini ely o en
is execu ed a leas e e y ks eps. Al hough his no ion in oduces addi ional
li eliness because i bounds he numbe o imes an enabled in e ac ion may
be neglec ed, i has se e al d awbacks: (i) kis no known a p io i, and hus
i canno be used o fine- une a po en ial schedule depending on he na u e
o he sys em i is scheduling; (ii) i does no p e en un ai fini eness; (iii) i
does no p e en conspi acies; and, o he bes o ou knowledge, (i ) no gene al
algo i hm implemen ing i has been p oduced. (The au ho s do only p esen a
P1.{Ge 1},P
2.{Ge 2},
(P5.{Ge 5, Ge 1},P
2.{Ge 2, Ge 3},P
1.{Ge 1, Ge 2}, Ge 1[],
P1.{Rel1},P
1.{Rel1,Rel
2},P
5.{Rel5,Rel
1},Rel
1[],P
1.{Ge 1})n
(a)
P1.{Ge 1},P
2.{Ge 2}P3.{Ge 3},
(P5.{Ge 5, Ge 1},P
3.{Ge 3, Ge 4},
P1.{Ge 1, Ge 2}, Ge 1[],P
2.{Ge 2, Ge 3}, Ge 3[],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.{Ge 1},P
3.{Ge 3})n
(b)
Fig. 2. S ong ai ness anomalies.
ans o ma ional app oach sui able o be used in he con ex o B¨uchi au oma a
[12,11].)
Hype ai ness also dese es a en ion because i alle ia es he second p ob-
lem. Technically, an execu ion is hype ai iff i is fini e o e e y in e ac ion ha
may ge enabled infini ely o en, becomes enabled infini ely o en. I is impo -
an o no ice ha his defini ion di e ges om classical no ions in ha he
la e imply e en ual execu ion o an in e ac ion i i ge s enabled sufficien ly
o en, whe eas hype ai ness does only imply e en ual enablemen . Subsequen
execu ion is unde he c i e ion o an implied unde lying classical ai ness no-
ion. Thus, his no ion p e en s conspi acies due o un o una e in e lea ing o
independen a omic ac ions bu combined wi h fini a y o s ong ai ness suffe s
om ai fini eness. To he bes o ou knowledge, no gene al algo i hm able
o implemen hype ai ness has been p oduced. Howe e , he au ho s p esen ed
a ans o ma ional app oach by means o which we can ans o m an IP p o-
g amme in o an equi alen s ongly hype ai o m, which implies modifica ion
o he sou ce code and c ea ion o explici schedule s o each p og amme. This
may be accep able in he con ex o esea ch languages, bu i is no p ac ical
enough in eal–wo ld languages in which p ocesses o componen s a e a ailable
only in bina y o m and need o be scheduled wi hou any knowledge o hei
in e nal de ails. Fu he mo e, i does no add ess he issue o ai fini eness.
1.3 O e iew
In his pape , we p esen a new no ion called s ong k– ai ness ha sol es ai
fini eness and conspi acies. In ui i ely, an execu ion is s ongly k– ai iff no in-
e ac ion is execu ed mo e han k imes unless he se o in e ac ions ha sha e
p ocesses wi h i is s able, i.e., he p ocesses ha pa icipa e in hem a e wai ing
o in e ac ion o finished, and i is he oldes in he g oup, i.e., he one ha has
no been execu ed o a longe pe iod o ime.
We p esen a heo e ical in e ac ion amewo k o o malize he mul ipa y
in e ac ion model. Fu he mo e, we p esen an algo i hm ha uses his ame-
wo k o scheduling in e ac ions in a s ongly k– ai manne , and i is no de-
penden on he in e nal de ails o he p ocesses ha compose he sys em, i.e., i
is no a ans o ma ional app oach.
The succeeding sec ions a e o ganised as ollows: Sec ion 2 p esen s ou he-
o e ical in e ac ion amewo k; Sec ion 3 p esen s a o mal defini ion o s ong
k– ai ness; Sec ion 4 desc ibes a schedule we can use o implemen his no ion;
finally, Sec ion 5 epo s on ou main conclusions.
2 A Theo e ical F amewo k
o Suppo he Mul ipa y In e ac ion Model
Nex , we p esen a o mal defini ion o ou abs ac in e ac ion amewo k.
Defini ion 1 (S a ic Cha ac e isa ion o a Sys em) A sys em Σisa2–
uple (PΣ,I
Σ)in which PΣ=∅is a fini e se o au onomous p ocesses and IΣ=
∅is a fini e se o in e ac ions. We deno e he se o p ocesses ha may e en ually
eady in e ac ion xas P(x)(pa icipan s o in e ac ion x). A configu a ion is a
ma hema ical objec ha may be iewed as a snapsho o a sys em a un ime.
We deno e hem as C, C,C
1,C
2...
An e en is a happening ha induces a sys em o ansi om a configu a ion
o ano he . In ou model, we ake in o accoun he ollowing kinds o e en s: p.ι,
which indica es ha p ocess pexecu es an a omic ac ion ha does only in ol e
i s local da a; p.χ, which indica es ha p ocess pis eadying he in e ac ions in
se χ(no ice ha when χ=∅, p ocess pa i es a a fixed poin ha we may
in e p e as i s e mina ion); and x, which indica es ha in e ac ion xhas been
selec ed and he p ocesses pa icipa ing in i can execu e he co esponding join
ac ion a omically.
Defini ion 2 (Dynamic Cha ac e isa ion o a Sys em) An execu ion o a
sys em Σis a 3– uple (C0,α,β)in which C0deno es i s ini ial configu a ion,
α=[C1,C
2,C
3,...]is a maximal (fini e o infini e) sequence o configu a ions
h ough which i p oceeds, and β=[e1,e
2,e
3,...]is a maximal (fini e o infini e)
sequence o e en s esponsible o he ansi ion be ween e e y wo consecu i e
configu a ions. Ob iously |α|=|β|. Finally, le λ=(C0,α,β)be an execu ion o
sys em Σ.Wecallαi s configu a ion ace and deno e i as λα, and βi s e en
ace and deno e i as λβ.
We deno e he ule ha cap u es he unde lying seman ics ha con ol
he ansi ion be ween configu a ions as L. Fo ins ance, CeLCin-
dica es ha he sys em may ansi om configu a ion C o configu a ion C
on occu ence o e en e. Thus, gi en an execu ion λ=(C0,[C1,C
2,C
3,...],
[e1,e
2,e
3,...]), we usually w i e i as2:C0e1LC1e2LC2e3L···
2No ice ha he exac o mula ion o Ldepends comple ely on he language in
which he sys em unde conside a ion was w i en.

Defini ion 3 (S a ic Cha ac e isa ion o a P ocess) P ocess pis wai ing
a in e ac ion se Υa he i– h configu a ion in execu ion λiff i has a i ed
a a poin in i s execu ion in which execu ing any x∈Υis one o i s possible
con inua ions. P ocess pis finished a he i– h configu a ion in execu ion λiff i
can nei he execu e any local compu a ion no any in e ac ion.
Wai ing(λ, p, Υ, i)⇐⇒ ∃ k∈[1..i]·β(k)=p.χ ∧Υ⊆χ∧j∈[k+1..i]·β(j)=x∧x∈χ
Finished(λ, p, i)⇐⇒ ∃ k∈[1..i]·β(k)=p.∅
(1)
Defini ion 4 (S a ic Cha ac e isa ion o an In e ac ion) In e ac ion x
is enabled a he i– h configu a ion in execu ion λiff all o he p ocesses in
P(x)a e eadying xa ha configu a ion. In e ac ion xis s able a he i– h con-
figu a ion in execu ion λiff i is ei he enabled o disabled a ha configu a ion.
Enabled(λ, x, i)⇐⇒ ∀ p∈P(x)·Wai ing(λ, p, {x},i)
S able(λ, x, i)⇐⇒ ∀ p∈P(x)·∃Υ⊆IΣ·Wai ing(λ, p, Υ, i)
(2)
Defini ion 5 (Dynamic Cha ac e isa ion o an In e ac ion) The se o
in e ac ions linked o in e ac ion xa he i– h configu a ion in execu ion λis
he se o in e ac ions such ha he e exis s a p ocess ha is eadying xand any
o hose in e ac ions simul aneously. We define he execu ion se o in e ac ion
xa he i– h configu a ion in execu ion λas he se o indices up o i ha deno e
he configu a ions a which in e ac ion xhas been execu ed.
Linked(λ, x, i)= {y∈IΣ·∃p∈PΣ·Wai ing(λ, p, {x, y},i)}
ExeSe (λ, x, i)= {k≤i·β(k)=x}
(3)
3 S ong k–Fai ness
In ui i ely, an execu ion is s ongly k– ai iff no in e ac ion is execu ed mo e han
k imes unless all o he in e ac ions ha a e linked o i when i is execu ed a e
s able and i is he oldes amongs hem.
Defini ion 6 (S ongly k–Fai Execu ion) Le λ=(C0,α,β)be an execu-
ion o a sys em, and ka non–null na u al numbe . λis s ongly k– ai iff p ed-
ica e SKF(λ, k)holds.
SKF(λ, k)⇐⇒ ∀ x∈IΣ,i∈ExeSe (λ, x, ∞)·Enabled(λ, x, i)∧
(LS able(λ, x, i)∧LOldes (λ, x, i)∨
¬LS able(λ, x, i)∧∆(λ, x, i)≤k)
(4)
This defini ion elies on a numbe o auxilia y p edica es and unc ions we
ha e in oduced o he sake o simplici y. LS able is a p edica e we use o
de e mine i an in e ac ion and hose ha a e linked o i a e s able a a gi en
configu a ion in an execu ion. I s o mal defini ion ollows:
LS able(λ, x, i)⇐⇒ ∀ y∈Linked(λ, x, i)∪{x}·S able(λ, y, i)(5)
LOldes is a p edica e we use o de e mine i an in e ac ion is olde han any
o he in e ac ions o which i is linked o , in he wo s case, is he same age. I s
defini ion ollows:
LOldes (λ, x, i)⇐⇒ ∀ y∈Linked(λ, x, i)·Age(λ, x, i)≥Age(λ, y, i) (6)
The age o an in e ac ion is he numbe o configu a ions ha ha e elapsed
since i was execu ed o he las ime, o ∞i i has ne e been execu ed so a .
Age(λ, x, i)=i−max ExeSe (λ, x, i) i ExeSe (λ, x, i)=∅
∞o he wise (7)
∆is a unc ion ha maps an e en ace, an in e ac ion and an index in o
he numbe o imes i has execu ed in he p esence o a non–emp y se o linked
in e ac ions ha was no s able. I s defini ion ollows:
∆(λ, x, i)= 
φ≤k<i
(λβ(k)=x∧Linked(λ, x, k)=∅∧¬LS able(λ, x, k)) (8)
whe e deno es he coun e quan ifie (
a∈A
P(a)|{a∈A·P(a)}|), and φis
defined as ollows (no ice ha we deno e he maximum o an emp y se as ⊥):
φji j= max{k∈ExeSe (λ, x, i)·LS able(λ, x, k)}∧j=⊥
1 o he wise (9)
4 A S ongly k–Fai Schedule
Ou algo i hm is based on p e ious p oposals which wan o esol e ano he
p oblems in he con ex o he mul ipa y in e ac ions [6,14,13].
The idea behind ou algo i hm o scheduling in e ac ions in a s ongly k– ai
manne consis s o a anging he se o in e ac ions in o a queue τso ha he
close an in e ac ion is o he ea , he less ime has elapsed since i was execu ed
o he las ime. Fu he mo e, each in e ac ion has an associa ed coun e δwe
use o coun how many imes i has been semi–enabled in p esence o linked
in e ac ions.
To know he s a e in which a p ocess o an in e ac ion is, we use a map ϕ
om he se o in e ac ions in o he se o p ocesses ha a e eadying i . We
upda e i each ime he selec ion module de ec s a ansi ion p.χLoccu s, o
an in e ac ion is execu ed. Ou algo i hm selec s o execu ion in e ac ion xas
long as i is he fi s enabled one in queue τ, and he se o in e ac ions linked
o i is s able.
We desc ibe he ope a ional seman ics o ou s ong k– ai ness algo i hm
using ansi ion ule SKF on configu a ions D,D,D
1,.... These configu-
a ions a e composed o he configu a ion Co he p og amme and he da a
s uc u es we need o selec in e ac ions. Nex , we define heses da a s uc u es
and he unc ions ha allows us o upda e i .
The ex ended configu a ions on which ou algo i hm wo ks a e o he o m
(τ, ϕ, δ, ϑ), whe e τis an in e ac ion queue, ϕis a eadiness map, δis a semi–
enablemen map, and ϑdeno es he se o p ocesses ha a e finished.
Defini ion 7 (Da a S uc u es) ϕdeno es a map om in e ac ions in o se s
o p ocesses. ϕ(x)deno es he se o p ocesses ha a e eadying x.ϑ⊆PΣ
deno es he se o p ocesses ha a e finished, i.e., can nei he execu e local com-
pu a ions no eady any in e ac ion. δis a map om he se o in e ac ions in o
he se o na u al numbe s. δ(x)deno es he numbe o imes any in e ac ion
linked o xhas been execu ed while xwas semi–enabled. The highe δ(x)is, he
highe he p obabili y o conspi acy is. τdeno es a queue in which he se o in-
e ac ions has been a anged so ha he close hey a e o he ea , he less ime
has elapsed since hey we e execu ed o he las ime. As usual, we conside a
queue o in e ac ions is a map om a subse o na u al numbe s in o he se o
in e ac ions.
The ini ial ex ended configu a ion o ou algo i hm is o he o m (τ0,ϕ
0,
δ0,ϑ
0). I does no ma e he o de in which in e ac ions a e ini ially a anged
in o τ,bu ϕ0mus sa is y ha ∀x∈dom ϕ0·ϕ0(x)=∅,δ0mus sa is y ha
∀x∈dom δ0·δ0(x)=0,andϑ0=∅.
Defini ion 8 (Func ions) When p ocess p eadies a se o in e ac ions χ,we
use unc ion AddOffe (ϕ, p, χ) o upda e map ϕ, and when in e ac ion xis exe-
cu ed, we use unc ion Remo eOffe (ϕ, x). By defini ion, p ocess pfinishes when
i eadies an emp y se o in e ac ions, and unc ion AddFinished(ϑ, p)upda es
map ϑ. When in e ac ion xis selec ed o execu ion, we use unc ion O de o
mo e i o he ea o τ, no necessa ily o he las posi ion. When in e ac ion x
is selec ed o execu ion, we use unc ion Upda e(ϕ, δ, x) o c ea e a new semi–
enablemen . P edica e S abilised(Υ, ϕ, ϑ)holds iff all o he p ocesses ha may
e en ually eady an in e ac ion in Υhas eadied i o a e finished. EnblDisj(τ,ϕ)
deno es he se o in e ac ions ha a e enabled and i does no exis s any p e-
ceding in e ac ion in τ ha is enabled and linked o hem.
AddOffe (ϕ, p, χ)={x→ ϕ(x)·x∈dom ϕ∧x∈ χ}∪
{x→ ϕ(x)∪{p}·x∈dom ϕ∧x∈χ}
Remo eOffe (ϕ, x)={x→ ϕ(x) P(x)·x∈dom ϕ}
AddFinished(ϑ, p)=
ϑ∪{p}i χ=∅
ϑi χ=∅
O de (τ, δ)=τ⇔dom τ= dom τ∧ an τ= an τ∧
∀x1,x
2∈ an τ·(τ−1(x1)≤τ−1(x2)⇒δ(x1)≥δ(x2))
Upda e(ϕ, δ, x)=δ⊗{x→ 0}⊗{y→ δ(y)+1·y∈S {x}∧¬S abilised(S,ϕ,ϑ)}
S abilised(Υ, ϕ, ϑ)⇔∀x∈Υ·∀p∈P(x)·p∈ an ϕ∨p∈ϑ
EnblDisj(τ, ϕ)={x∈dom ϕ·P(x)=ϕ(x)∧y∈S·P(y)=ϕ(y)∧τ−1(y)<τ
−1(x)}
(10)
whe e S{z∈dom ϕ·ϕ(z)∩ϕ(x)=∅}.
Ou algo i hm is o mally defined by means o he in e ence ules p esen ed in
Figu e 3. Rule 11 is s aigh o wa d because i desc ibes how he da a s uc u es
a e upda ed each ime p ocess p eadies a se o in e ac ions χ. Rule 12 desc ibes
which in e ac ion mus be selec ed so ha he execu ion is s ongly k– ai . The
an eceden is complex, bu he easoning behind i is qui e simple. Assume xis
an enabled in e ac ion and he e is no a conflic ing enabled in e ac ion be o e
xin queue τ, i.e., x∈EnblDisj(τ,ϕ); in his con ex xis selec ed o execu ion
iff any o he ollowing h ee condi ions hold:
Cp.χLC∧
ϕ= AddOffe (ϕ, p, χ)∧ϑ= AddFinished(ϑ, p)
(C, τ, ϕ, δ, ϑ)p.χSKF (C,τ,ϕ
δ, ϑ)(11)
x∈EnblDisj(τ, ϕ)∧S={z∈dom ϕ·(ϕ(z)∩ϕ(x)=∅)}∧
τ= O de (τ, δ)∧ϕ= Remo eOffe (ϕ, x)∧δ= Upda e(ϕ, δ, x)∧
(S={x}∨S abilised(S,ϕ,ϑ)∨(S ={x}∧ max
y∈S {x}δ(y)<k))
(C, τ, ϕ, δ, ϑ)xSKF (C,τ,ϕ
,δ
,ϑ)∧CxLC(12)
Fig. 3. Algo i hm o s ongly k– ai schedule .
1. I is no conflic ing wi h o he in e ac ions (S={x}).
2. The in e ac ions which i is conflic ing wi h a e s abilised, i.e., all o hei
pa icipan s a e eadying i o finished (S abilised(S,ϕ,ϑ)).
3. The semi–enablemen coun e associa ed wi h each conflic ing in e ac ion is
less han k(S ={x}∧ max
y∈S {x}δ(y)<k).
5 Conclusions and Fu u e Wo k
In his pape , we ha e p esen ed s ong k– ai ness in he con ex o concu en
and/o dis ibu ed p og ammes in which mul ipa y in e ac ion models a e he
sole mean o p ocess synch onisa ion and communica ion. An impo an con-
ibu ion is he concep o semi–enablemen ha we use o o ecas conspi acies
and sol e hem. kcan hus be iewed as a semi–enablemen h eshold ha cha -
ac e ises he goodness o ou no ion because i makes ou selec ion c i e ion mo e
o less demanding. I kis minimum, he pace a which conflic ing in e ac ions
a e execu ed depends hen on he pa icipan ha spends mo e ime a doing
local compu a ions because, in his case, no in e ac ion can be selec ed o exe-
cu ion unless he se o po en ially conflic ing in e ac ions is consolida ed. I k
is e y dis an om i s minimum, he algo i hm in oduces li le delay because
in e ac ions may be scheduled as soon as hey a e enabled. The exac choice o
kdepends on he ea u es o he p og amme unde conside a ion and can only
be uned by means o expe imen a ion.