÷ƒ’Ą;č TeX output 2000.06.01:2033‹’’’’ o#f ż¬Üš 5#f żäܚ‘eFÆóĀÖN ff cmbx12ŗPŒĢartially–ffOrdered“Runs:“a“Case“StudyŽŸ#!Œ’—Ų«óKń`y cmr10²Y‘’*Ŗuri–UUGurevicšøćhŸü^’óŁ“ Rcmr7±1Ž‘ŃȲand“Dean“Rosenzw˜eigŸü^’±2ŽŽŸõi’¹­™óo“‹Ē cmr9¾Microsoft–TResearc¾9h,“USAޤ ‘r£¦óߤN cmtt9ægurevich@microsoft.com–T¾and“Univ•¾9ersit“y–Tof“Zagreb,“CroatiaŽ”’Š6Lædean@math.hrŽŸ+融‘[sēót ‰: cmbx9ĄAbstract.ŽŽ’Œ&„¾W‘’:«e–ploAĒok“at“some“sources“of“insecuritš¾9y“and“dicult˜y“in“rea-Ž”‘[sēsoning–Ó,abšAĒout“partially“ordered“runs“of“distributed“ASMs,“and“prop˜oseŽ”‘[sēsome–ntecš¾9hniques“to“facilitate“suc˜h“reasoning.“As“a“case“study‘’:«,“w˜e“pro˜v˜eŽ”‘[sēin–‡detail“correctness“and“deadloAĒc¾9k{freedom“for“general“partially“orderedŽ”‘[sēruns–Tof“distributed“ASM“mošAĒdels“of“Lamp˜ort's“Bak¾9ery“Algorithm.ŽŸ#o‘?óĀÖN  cmbx12ĀIn tro`ductionŽŸŲ‘?²Distributed– æASMs“[Gur95Ž‘QĖ]“is“a“general“concurrenšøćt“moGdel“of“m˜ulti{agen˜t“compu-ޤ ‘?tation.–8ćIt“wšøćas“in˜tended,“in“generalization“of“its“more“limited“precursors“[GM90Ž‘’,GR93Ž‘5X],Ž”‘?to–…rallošøćw“as“m˜uc˜h“concurrency“as“logically“pGossible.“Although“the“de nition“hasŽ”‘?bGeen–"±in“prinšøćt“for“sev˜eral“y˜ears,“its“notion“of“partially“ordered“runs“has“remainedŽ”‘?largely–Junexploited“in“its“generalitšøćy|most“of“its“uses“in“the“literature“ha˜v˜e“re-Ž”‘?coursed–“«to“some“kind“of“spGecialization“to“linear“time,“discrete“or“con•øćtin“uous.Ž”‘?The–™¼general“partially“ordered“runs“seem“to“bGe“somehoøćw“dicult“to“handle“andŽ”‘?to–UUreason“abGout“Ÿü^’±1ŽŽ‘ŃȲ.Ž© ^g‘NApart–Ų2from“deeply“engrained“inšøćtuitions“of“linear“time,“w˜e“feel“that“someŽ”‘?rather–UUtecšøćhnical“sources“of“this“dicult˜y“can“bGe“detected.ަ‘NSequenšøćtial–~\runs“[Gur95Ž‘QĖ]“ha˜v˜e“t˜w˜o“propGerties“whic˜h“greatly“facilitate“reason-Ž”‘?ing.ŽŸy›‘C8ā1.ŽŽŽ‘PEv•øćery›UUmo“v“e˜is˜executed˜in˜a˜w“ell{de ned˜state.ަ‘C8ā2.ŽŽŽ‘P`External'–"(or“`monitored',“cf.“bGelošøćw)“c˜hanges“can“bšGe“lo˜cated“in“time,“andŽ”‘Pthoughšøćt– Bof“as“actions“b˜y“the“en˜vironmen˜t.“The“en˜vironmen˜t“th˜us“bGecomesŽ”‘Pjust–‹®another“(tšøćypically“implicit)“agen˜t,“whose“bGeha˜viour“can“bšGe“sp˜eci ed“inŽ”‘Pdeclarativšøće–ģ²terms.“The“judicious“splitting“of“dynamics“to“a“part“giv˜en“b˜y“theŽ”‘Pprogram–Ą;and“a“part“that“can“bšGe“sp˜eci ed“declarativšøćely“is“a“natural“w˜a˜y“toŽ”‘Pseparate–UUconcerns“and“to“abstract“in“ASMs.ŽŸ4‘?In–u–a“partially“ordered“run“neither“of“the“abšGo•øćv“e–u–prop˜erties“hold“in“general|aŽ”‘?(global)–/Ņstate“in“whicšøćh“a“mo˜v˜e“is“executed“is“in“general“not“uniquely“de ned,Ž”‘?and–¾it“is“not“at“all“clear“hošøćw“to“loGcate“external“c˜hanges“in“a“partial“order.“TheseŽ‘?Ÿą‰ff8ēϟ LĶ‘ĄŸü-=ó¹AaØcmr6Ć1ŽŽŽŽ‘ ¾This–ęMremark“is“not“limited“to“the“ASM‘ęcon¾9text|most“formal“methošAĒds“mo˜dellingޤ ‘ concurrency–-mtend“to“fall“bacš¾9k,“one“w˜a˜y“or“another,“to“some“kind“of“in˜terlea˜ving,Ž”‘ sequen•¾9tial‘Tseman“ticsŽŽŽŒ‹* o#f ż¬Üš 5#f żäܚ‘?²seem–ŗtto“bšGe“imp˜ortanšøćt“sources“of“insecurit˜y“and“dicult˜y“in“reasoning“abGoutޤ ‘?partially–UUordered“runs.Ž© 5‘NW‘’*Ŗe–H®address“bGoth“issues“here,“bšøćy“dev˜eloping“some“tec˜hniques“to“salv‘’qĒage“asŽ”‘?m•øćuc“h–žof“propGerties“1.“and“2.“as“needed“for“partially“ordered“runs.“In“order“toŽ”‘?conšøćvince–Rthe“reader“that,“with“suc˜h“means,“non˜trivial“reasoning“abGout“partiallyŽ”‘?ordered–x¢runs“is“feasible,“wšøće“do“it:“as“a“case“study‘’*Ŗ,“w˜e“apply“the“tec˜hniques“to“aŽ”‘?nonøćtrivial–§jcorrectness“prošGof.“The“case“study“also“demonstrates“that“the“prop˜erŽ”‘?setting–g for“analysis“of“concurrenšøćt“algorithms“in˜v˜olv˜es“truly“concurren˜t“runs|Ž”‘?mapping–UUto“linear“time“mašøćy“w˜ell“miss“some“impGortan˜t“pGoin˜ts.ަ‘NIn–2section“2“wøće“deduce“some“simple“consequences“of“the“coherence“conditionŽ”‘?of–üż[Gur95Ž‘QĖ],“prošøćviding“sucien˜t“conditions“for“mo˜v˜es“in“a“distributed“run“to“ha˜v˜eŽ”‘?at–f-least“a“signi canšøćt“pGortion“of“state“w˜ell{de ned“when“they“execute.“This“largelyŽ”‘?reconstructs–|propGertšøćy“1.“for“partially“ordered“runs“of“man˜y“distributed“programs.ަ‘NIn–Ppthe“same“section“wšøće“in˜troGduce“`external“c˜hange'“in“form“of“`monitored'Ž”‘?mo•øćv“es,›9Ļb“y˜unkno“wn˜agen“ts˜with˜unkno“wn˜programs,˜loGcated˜exactly˜in˜the˜par-Ž”‘?tial–Mčorder.“This“is“an“extension“of“the“standard“practice“(of“hašøćving“`the“en˜vi-Ž”‘?ronmenšøćt'–ŲŌas“a“single,“t˜ypically“implicit,“unkno˜wn“agen˜t)“reconstructing“largelyŽ”‘?propGertøćy–UU2.“for“partially“ordered“runs.ަ‘NIn–Ķčthe“rest“of“the“papGer“wšøće“explain“a“non˜trivial“correctness“proGof“for“partiallyŽ”‘?ordered–N†runs:“wšøće“pro˜v˜e“in“detail“correctness“and“deadloGc˜k{freedom“of“(distributedŽ”‘?ASM‘Q#mošGdels–Qdof‘Ē)“Lamp˜ort's“Bakøćery“Algorithm“[Lam74Ž‘•[].“W‘’*Ŗe“pro˜ceed“on“threeŽ”‘?di erenšøćt–%żabstraction“lev˜els“there.“The“abstraction“lev˜el“of“our“primary“moGdel,Ž”‘?ó !",š cmsy10øBŸ’±1Ž‘|s²,–¶äcorrespšGonds“precisely“to“that“of“Lamp˜ort's“algorithm|the“part“sp˜eci edŽ”‘?declarativøćely–vis“exactly“what“LampšGort's“algorithm“do˜esn't“de ne.“A‘hhigher“levøćelŽ”‘?description,–Āåof“the“mošGdel“øBŸ’±2Ž‘|s²,“alloøćws“us“to“deduce“correctness“and“deadlo˜cøćk{Ž”‘?freedom–½Tfrom“abstract“propGerties,“shošøćwn“to“hold“of“øBŸ’±1Ž‘|s².“A‘½.lo˜w˜er“lev˜el“description,Ž”‘?of–sDthe“moGdel“øBŸ’±0Ž‘|s²,“is“an“ASM‘rśshošøćwn“to“implemen˜t“programatically“exactly“allŽ”‘?bGeha•øćviours›UUallo“w“ed˜b“y˜øBŸ’±1Ž‘|s².ަ‘NEgon–Ą™B‘ś’’orger“and“wšøće“wrote“abGout“the“Bak˜ery“Algoirithm“earlier;“see“[BGR95Ž‘ JÆ]Ž”‘?where–ĆŃa“correctness“proGof“wšøćas“giv˜en“for“ASM‘Ć“moGdels“of“the“Bak˜ery“AlgorithmŽ”‘?with–€Ųruns“emšøćbGedded“in“con˜tin˜uous“linear“time.“Our“new“mošGdels“and“pro˜ofs“areŽ”‘?similar–emto“those“of“[BGR95Ž› JÆ],“but“they“are“also“di erenøćt.“The“proGofs“of“[BGR95Ž˜]Ž”‘?rely– ‰essenšøćtially“on“con˜tin˜uous“linear“time.“As“w˜e“will“see“later“(see“section“7),Ž”‘?certain–rinformation“abGout“partially“ordered“runs“is“obfuscated“in“linear“runs.Ž”‘?Here–šėwšøće“remo˜v˜e“the“linear“time“crutc˜hes“and“w˜ork“directly“with“partially“orderedŽ”‘?runs.–ąĒAs“in“[BGR95Ž‘ JÆ],“wšøće“bGorro˜w“ideas“from“[Lam74Ž‘•[]“and“[Abr93Ž‘ųč].“In“order“forŽ”‘?the–ķJpapšGer“to“b˜e“reasonably“self{conšøćtained“w˜e“spGell“the“en˜tire“construction“out“inŽ”‘?full.ŽŸ! Ģ‘?Ā1Ž‘S@PreliminariesŽŸ Ģ‘?²W‘’*Ŗe–>.presume“that“the“reader“is“familiar“with“[Gur95Ž‘QĖ].“Consider“a“one-agenøćt“pro-Ž”‘?gram–Ūó  b> cmmi10µ›\“²and“let“µf‘j²bGe“a“basic“function“of“µ˜²whicøćh“is“dynamic“so“that“the“v‘’qĒalues“ofŽ”‘?µf‘:²can–’«cšøćhange“in“runs“of“µ[ٲ.“Egon“B‘ś’’orger“suggested“to“use“for“ASMs“the“follo˜wingŽ”‘?terminology›‘SbGorro•øćw“ed˜from˜P“arnas.˜µf‘¤ā²is˜óż': cmti10Źc–’}'ontr“ol‘‚Ųle“d˜²if˜only˜µ‘ķ,²can˜cøćhange˜it.˜µf‘¤ā²isŽŽŽŒ‹ „ o#f ż¬Üš 5#f żäܚ‘?Źmonitor–’}'e“d–«3²if“only“the“en•øćvironmen“t–«3can“cøćhange“it.“µf‘¾Ā²is“Źshar–’}'e“d–«3²if“bGoth“µ‘ ²and“theޤ ‘?en•øćvironmen“t–šBcan“cšøćhange“it.“(In“[Gur95Ž‘QĖ],“con˜trolled“functions“w˜ere“called“in˜ternal,Ž”‘?and–UUmonitored“functions“wøćere“called“external.)Ž”‘NThe–÷9terminology“extends“naturally“to“a“m•øćulti-agen“t–÷9program“µ‘Ļž².“Let“µX‘Ą²bGeŽ”‘?a–†ąset“of“agenšøćts“of“µ‘Ļž².“A‘†‘dynamic“basic“function“µf‘šo²is“con˜trolled“b˜y“µX‘O²if“onlyŽ”‘?agenšøćts–•in“µX‘]ž²can“c˜hange“it.“µf‘Ø«²is“monitored“b˜y“X‘• if“none“of“the“agen˜ts“in“µX‘]ž²canŽ”‘?cøćhange–pit.“The“terminology“also“extends“to“particular“loGcations“rather“than“wholeŽ”‘?functions.ŽŸ`\‘?Ā2Ž‘S@P artially–€Ordered“RunsŽŸ`\‘?²W‘’*Ŗe–UUrely“on“the“notion“of“partially“ordered“run“of“[Gur95Ž‘QĖ].Ž”‘NThis–ÖĘmeans“that“wšøće“shall“consider“partially“ordered“sets“of“mo˜v˜es“with“theŽ”‘?` nite–xhistory'“propGertøćy:“øfµy–…²:›«¬µy“<˜xøg–x²is“ nite“for“all“µx“²(wøće“shall“refer“to“theŽ”‘?ordering–ķ¢relation“bšøćy“µ<²,“using“also“øµ;–ŖØ>;“ø²).–ķ¢Eac˜h“mo˜v˜e“is“pGerformed“b˜y“an“agen˜tŽ”‘?and,–¬‹since“agenšøćts“are“sequen˜tial,“mo˜v˜es“b˜y“one“agen˜t“form“a“sequence;“since“thereŽ”‘?are–UU nitely“manšøćy“agen˜ts,“all“an˜tic˜hains“are“ nite.Ž”‘NA‘ūš(global)–ü]state“µ[ٲ(µI‘Čā²)“is“assoGciated“with“evšøćery“ nite“initial“segmen˜t“µI‘Å?²(aŽ”‘?do•øćwn“w“ards–$closed“ nite“subset)“of“a“run,“resulting“from“pGerforming“all“mo•øćv“es‘$inŽ”‘?µI›ž0²so–ÕNthat“if“µs–Ē<“t–ÕN²then“µs“²is“executed“earlier“than“µt².“In“particular,“if“µI˜²is“the“emptøćyŽ”‘?segmenøćt–UUthen“µ[ٲ(µI‘Čā²)“is“the“initial“state“of“the“run.Ž”‘NUsing–ˆ³a“partial“order“implies“that“mo•øćv“es–ˆ³µs;‘ŖØt“²mašøćy“bGe“concurren˜t,“i.e.“incom-Ž”‘?parable:–vÕneither“µs–žķø“µt–vÕ²nor“µt–žķø“µs–vÕ²holds.“The“global“state“`resulting'“from“a“mo•øćv“eŽ”‘?is–jZthen“in“general“not“uniquely“determined.“It“depGends“on“what“global“state“wøćeŽ”‘?see–q‚as“the“one“in“whicšøćh“the“mo˜v˜e“is“pGerformed.“Th˜us“states“are“sub‘Ž8ject“to“aŽ”‘?coherence–UUcondition“[Gur95Ž‘QĖ],“whicšøćh“allo˜ws“us“to“giv˜e“the“follo˜wing“de nitions.Ž”‘NLet‘įŻPøćostŽ‘>Q(µt²)–įŻbGe“the“set“of“all“ nite“initial“segmenšøćts“in“whic˜h“a“mo˜v˜e“µt“²isŽ”‘?maximal,–ę(and“let“µa“²bšGe“the“agenøćt“p˜erforming“µt².“F‘’*Ŗor“eacšøćh“µI‘Xø2‘øv²P˜ostŽ‘ź(µt²),“the“stateŽ”‘?µš[ٲ(µI‘Čā²)–UUis“the“state“obtained“when“µa“²executes“its“program“in“the“state“µ˜²(µI‘Āøn‘8ąfµtøg²)Ž”‘N`The–‚Įglobal“state'“in“whicšøćh“a“mo˜v˜e“is“pGerformed“is“also“not“in“general“uniquelyŽ”‘?de ned.–mĘLet“PreŽ‘˜r(µt²)–ļŌ=“øfµI‘ øn‘I+fµtøg“²:“µI‘ø¶ø2“²PøćostŽ‘LH(µt²)øg².–mĘSevšøćeral“di eren˜t“states“are“th˜us“inŽ”‘?general–ŁžassoGciated“with“PreŽ‘J(µt²),“whicšøćh“mak˜es“reasoning“abGout“partially“orderedŽ”‘?runs–‘»somewhat“dicult.“The“coherence“condition“mašøćy“ho˜w˜ev˜er,“as“w˜e“shall“seeŽ”‘?b•Geloøćw,›UUimp“ose˜that˜some˜term˜has˜a˜unique˜v‘’qĒalue˜at˜all˜states˜µI‘śø2‘DzPreŽ‘ńÄ(µt²).Ž”‘NIn–Ējorder“to“express“sucšøćh“requiremen˜ts“succinctly‘’*Ŗ,“w˜e“extend“term“v‘’qĒaluationŽ”‘?from–UUstates“to“some“statesets,“saøćying“thatŽŸź:‘rĢV‘’*ŖalŽ’=ڟĪ:±PreŽ’LŸĪ:(ó 0e—rcmmi7“t±)Ž’—n²(µu²)ŽŽ’§^Ö=ŽŽ’±ņĄŸōę`óś±u cmex10«nŽŸū@’ŗHµcŽ’ÜrIJifŽ’čņÅø8µI‘śø2‘DzPreŽ‘ńÄ(µt²)‘8ą(µc–Dz=“V‘’*ŖalŽ‘8įŸĪ:“@L±(“I‘‹J±)Ž‘ ņ²(µu²))ŽŽ”’ŗHundefŽŽ’ÜrÄif–UUno“sucøćh“v‘’qĒalue“existsŽŽŽŽŽŽŽŽŸxs‘?where–1µt“²is“a“mo•øćv“e–1in“a“distributed“run,“V‘’*ŖalŽ‘xśŸ’“SŽ‘D²(µu²)“is“the“v‘’qĒalue“of“term“µu“²in“state“µS‘“²,Ž”‘?[Gur95Ž‘QĖ].– ŗW›’*Ŗe“shall“often“shorten“V˜alŽ‘{ƒŸĪ:±PreŽ‘‰æŸĪ:(“t±)Ž‘'O²(µu²)“to“µuŸĪ:±PreŽ‘ <ŸĪ:(“t±)Ž‘Ӕ².“When“the“v‘’qĒalue“of“µuŸĪ:±PreŽ‘ <ŸĪ:(“t±)ŽŽ”‘?²is–Dgivšøćen“b˜y“the“ rst“clause,“i.e.“when“there“is“a“µc“²suc˜h“that“ø8µI‘ķø2‘U ²PreŽ‘·(µt²)‘Ų(µc‘U ²=Ž”‘?V‘’*ŖalŽ‘MqɟĪ:“@L±(“I‘‹J±)Ž‘]*ö²(µu²)),–ųwšøće“shall“sa˜y“that“µuŸĪ:±PreŽ‘ <ŸĪ:(“t±)Ž‘،²is“Źindisputable“²(or“that“its“v‘’qĒalue“is“indis-Ž”‘?putable).–ErNotice“that“an“indisputable“v‘’qĒalue“mašøćy“also“bGe“undef,“but“whenev˜erŽ”‘?µuŸĪ:±PreŽ‘ <ŸĪ:(“t±)Ž‘š¬ø6²=‘ĒundefŽ‘Gthen–UUits“v‘’qĒalue“is“indisputable.Ž”‘NF‘’*Ŗor–UUfuture“reference,“let“us“note“some“immediate“propGerties“of“PreŽ‘€(µt²).ŽŽŽŒ‹Ø o#f ż¬Üš 5#f żäܚ‘?ó ņ"V cmbx10ĖF‘’ «act‘ÕT1.ŽŽ‘f:ŹL›’}'et–ܵt“Źb˜e“a“move“in“a“p˜artial‘‚Ųly“or˜der˜e˜d“run.“The“set“Pr˜eŽ‘ņ¹²(µt²)“Źhas“the“fol-ޤ ‘?lowing‘“ēpr–’}'op“erties.ŽŸ„؍‘BŅ€1.ŽŽŽ‘PPr‘’}'eŽ‘_¹²(µt²)–ńTŹhas“a“minimal“element“²minŽ‘FŖŹPr‘’}'eŽ‘&]c²(µt²)–@=“øfµs“²:“µs“<“tøg–ńTŹand“a“maximalŽ”‘Pelement‘“ē²maxŽ‘ŪŹPr‘’}'eŽ‘&ń¾²(µt²)–Ē=“øfµs“²:“µs“ø6“µtøgŹ.Ž© €ī‘BŅ€2.ŽŽŽ‘PPr‘’}'eŽ‘_¹²(µt²)–Ž8Źis“the“set“of“al‘‚Ųl“initial“se›’}'gments“µI‘WŹsuch“that“²minŽ‘掬Pr˜eŽ‘#śG²(µt²)–Ēø“µI‘śø“²maxŽ‘6ŹPr˜eŽ‘&$ļ²(µt²)Ź,Ž”‘Pand–“ēis“henc›’}'e“close˜d“under“unions“and“interse˜ctions.ަ‘BŅ€3.ŽŽŽ‘PL›’}'et–“ēµs“Źb˜e“another“move.“The“fol‘‚Ųlowing“ar˜e“e˜quivalent:ŽŸ Ż‘N¶(a)ŽŽŽ‘aµs–“ēŹis“c–’}'oncurr“ent–“ēwith“µtŹ.ަ‘O8é(b)ŽŽŽ‘a²minŽ‘sUVŹPr‘’}'eŽ’‚l²(µs²)–2ø[“²minŽ‘jˆŹPr‘’}'eŽ‘$A²(µt²)–ĆōŹis“an“initial“se›’}'gment“that“b˜elongs“to“Pr˜eޑڭ²(µs²)‘2ø\Ž”‘aŹPr‘’}'eŽ‘p¹²(µt²)Ź.ަ‘O8é(c)ŽŽŽ‘aPr‘’}'eŽ‘p¹²(µs²)–8ąø\“ŹPr‘’}'eŽ‘O™²(µt²)–Ēø6²=“ø;Ź.ަ‘N¶(d)ŽŽŽ‘aTher›’}'e–“ēexist“µI‘Čā;‘ŖØJ‘½Qø2‘ĒŹPr˜eŽ‘ŻŃ²(µt²)“Źwith“µs–Ēø2“µI‘Āøn‘8ąµJ‘ö9Ź.ŽŸ–‘N²Statemenšøćt–×ō3“ma˜y“need“an“argumen˜t.“W‘’*Ŗe“pro˜v˜e“that“(a)“implies“(b)“impliesŽ”‘?(c)–UUimplies“(d)“implies“(a).Ž”‘N(a)–DIimplies“(b).“Assume“that“µs“²is“concurrenøćt“with“µt“²and“let“µI‘ś²=‘ĒminŽ‘nPreŽ‘$G(µs²)‘Čø[Ž”‘?²minŽ‘QUVPreŽ‘`€(µt²).–8ćClearly“µI‘Ųis“an“initial“segmenšøćt.“Chec˜k“that“minŽ‘Ž9PreŽ‘#øå(µt²)–Ēø“µI‘śø“²maxŽ‘6PreŽ‘&8ā(µt²),Ž”‘?so–UUthat“µI›śø2‘DzPreŽ‘ńÄ(µt²).“By“symmetry‘’*Ŗ,“µI˜ø2‘DzPreŽ‘ńÄ(µs²).Ž”‘N(b)–UUimplies“(c).“T‘’*Ŗrivial.Ž”‘N(c)–»4implies“(d).“Assume“that“PreŽ‘åą(µs²)–|Źø\“²PreŽ‘§v(µt²)–pįø6²=“ø;–»4²and“let“µJ‘±m²bGe“anšøćy“mem˜bGerŽ”‘?of‘UUPreŽ‘€(µs²)–8ąø\“²PreŽ‘cŒ(µt²).–UUSet“µI›ś²=‘ǵJ‘/ø[‘8ąfµsøg².“Clearly‘’*Ŗ,“µI˜ø2‘DzPreŽ‘ńÄ(µt²).Ž”‘N(d)–‡'implies“(a).“SuppGose“that“µI‘Čā;‘ŖØJ‘»ø2‘ÄɲPreŽ‘ļu(µt²)“and“µs–ÄÉø2“µI‘Ķ¢øn‘ĄµJ‘ö9².–‡'If“µs–ÄÉ<“t‘‡'²thenŽ”‘?µs–Ēø2“²minŽ‘nPreŽ‘$G(µt²)“ø“µJ›!ź²so–+±that“µs–Ēø2“µJ˜²whicšøćh–+±is“impGossible.“The“dual“argumen˜t“sho˜wsŽ”‘?that›UUµs–Ē>“t˜²is˜impGossible˜as˜wøćell.ŽŸ€ī‘NW‘’*Ŗe–&eshall“sašøćy“that“a“mo˜v˜e“µt“²(in“a“giv˜en“partially“ordered“run)“Źmay‘T>changeŽ”‘?²the–vHv‘’qĒalue“of“term“µu“²if,“for“some“µI‘Ęäø2‘ž²PreŽ‘(®(µt²),“wšøće“ha˜v˜e“V‘’*ŖalŽ‘čŸĪ:“@L±(“I‘‹J±)Ž‘!”>²(µu²)–žø6²=“V‘’*ŖalŽ‘o˟Ī:“@L±(“I‘‹Jó O!ā…cmsy7·[f“t·g±)Ž‘1Ć„²(µu²)Ž”‘?(equiv‘’qĒalenšøćtly‘’*Ŗ,–,¹if“µt“²c˜hanges“the“v‘’qĒalue“of“µu“²in“some“linearization“of“the“run).“If“theŽ”‘?abGo•øćv“e–@Yholds“for“all“µI‘©ø2‘NDzPreŽ‘ys(µt²)“(equiv‘’qĒalenšøćtly‘’*Ŗ,“if“µt“²c˜hanges“the“v‘’qĒalue“of“µu“²in“allŽ”‘?linearizations),–UUwšøće“shall“sa˜y“that“µt“Źmust‘“ēchange‘°²the“v‘’qĒalue“of“µu².Ž”‘NRecall–tˆthat“a“linearization“of“a“partially“ordered“run“is“a“run“with“the“sameŽ”‘?mo•øćv“es,––and“a“linear“order“extending“the“givšøćen“partial“order.“It“w˜as“noted“inŽ”‘?[Gur95Ž‘QĖ]–ü­that,“in“view“of“the“coherence“condition,“all“linearizations“of“a“ nite“runŽ”‘?ha•øćv“e–UUthe“same“ nal“state.ޤ„؍‘?ŹExample‘“ē1.ŽŽ‘t»©²T‘’*Ŗakšøće–2ffor“instance“t˜w˜o“agen˜ts“µa;‘ŖØb²,“suc˜h“that“µa“²executes“the“programŽ”‘Næ÷ó!ßźĢn[i]“or“(n[j]=n[i]“and“jµ>Ģi)ŽŽ”‘?ĪCritical‘UUSectionŽŸ#Ս‘?FinaleŽ”‘Næ÷ĢRŸ’“iŽ‘”IĢ:=‘?ż0ŽŽ”‘N²The–̰Bakšøćery“Algorithm“is“divided“in˜to“six“consecutiv˜e“phases:“Źstart‘ņŲ²,“Źdo‘’}'orway‘ā}²,ަ‘?Źticket‘H-²assignmenøćt,–UUŹwait“²section,“Źcritic–’}'al‘“ēse“ction–UU²and“Ź nale‘Ą[².ަ‘NT‘’*Ŗo–{ßdeclare“its“inøćterest“in“accessing“the“critical“session,“a“proGcess“µPŸ’“iŽ‘Š+²writes“1ަ‘?in•øćto›UUarra“y˜v–’qĒariable˜µnŸ’“iŽ‘©”²and˜then˜pGosts˜the˜written˜v“alue˜in˜its˜register.ަ‘NIn–¢µthe“doGorw•øća“y–¢µsection,“µPŸ’“iŽ‘÷²copies“all“the“other“registers“inšøćto“its“arra˜y‘’*Ŗ.“Itަ‘?then–2¼computes“a“Źticket‘ņŲ²,“whicšøćh“is“the“least“in˜teger“greater“than“all“in˜tegers“in“itsަ‘?priv‘’qĒate–ē\arrašøćy‘’*Ŗ,“writes“the“tic˜k˜et“in˜to“µnŸ’“iŽ‘;زand“pGosts“the“written“v‘’qĒalue“in“its“register.ަ‘NDuring–OĪthe“subsequenšøćt“w˜ait“section,“proGcess“µPŸ’“iŽ‘¤²k˜eeps“reading,“in˜to“its“arra˜y‘’*Ŗ,ަ‘?the–)ńregisters“of“eacšøćh“other“proGcess“µPŸ’“jŽ‘6¬²,“un˜til“the“resulting“arra˜y“v‘’qĒalue“µn²[µj‘’‹²]–Ē=“0‘)ńorަ‘?µn²[µj›’‹²]–ǵ>“n²[µi²]–UUor“µn²[µj˜²]–Ē=“µn²[µi²]–8ąø^“µj‘Y£>‘Ēi².ަ‘NThe–K.meaning“of“the“condition“is“the“folloøćwing:“if“µn²[µj‘’‹²]–`Õ=“0,–K.then“µPŸ’“jŽ‘Ś²is“notަ‘?inšøćterested–˜in“en˜tering“the“critical“section,“and“it“has“no“righ˜t“to“bloGc˜k“µPŸ’“iŽ‘TL².“Ifަ‘?µn²[µj‘’‹²]–×~µ>“n²[µi²]“µ>“²0,–_,then“µPŸ’“iŽ‘³x²has“a“smaller“`tic•øćk“et'–_,and“has“the“righøćt“to“go“bGefore“µPŸ’“jŽ‘6¬².ަ‘?The–ā last“clause“resolvšøćes“the“case“of“t˜w˜o“customers“obtaining“the“same“`tic˜k˜et':ަ‘?then–Įßone“with“smaller“idenšøćti er“goGes“ rst.“Note“that“b˜y“ordering“pairs“of“pGositiv˜eަ‘?inøćtegers‘UUlexicographically:ޤ³(’Š¹(µi;›ŖØj‘’‹²)–ǵ<“²(µkP—;˜lš2`²)“ø ‘žUX!“²[µi“<“k‘„ģ²orŽ‘åķ(µi“²=“µk‘„ģ²andŽ‘¶µj‘Y£<“l˜²)]Ž”‘?one–UUcan“write“the“unšøćtil“condition“as“follo˜ws:“n[j]=0“or“(n[j],j)µ>²(n[i],i).ަ‘NOnce–{†pšGermitted“to“go,“µPŸ’“iŽ‘ĻҲenøćters“the“critical“section.“Up˜on“leaøćving“CS,“asަ‘? nale,–UUµPŸ’“iŽ‘©”²sets“its“register“to“0.ަ‘NNote–„malso“that“the“for-all“commands“in“the“doGorw•øća“y–„mand“the“wšøćait“section“ma˜yަ‘?bGe–UUexecuted“in“manšøćy“w˜a˜ys,“in“v‘’qĒarious“sequences,“all“at“once,“concurren˜tly“etc.ަ‘NIt–‡Mmašøćy“bGe“w˜orth“men˜tioning“the“follo˜wing.“The“proGcess“ rst“writes“in˜to“µn²[µi²]ަ‘?and– |then“pGosts“the“written“v‘’qĒalue“at“µRŸ’“iŽ‘TL².“Obšøćviously“it“could“do“the“t˜w˜o“actions“inަ‘?the–Åsrevšøćerse“order.“In˜tuitiv˜ely‘’*Ŗ,“the“order“bGet˜w˜een“the“t˜w˜o“actions“is“immaterial,ަ‘?but–UUthe“sequenšøćtial“c˜haracter“of“the“pseudo-cošGde“imp˜oses“one.ŽŽŽŒ‹[Õ o#f ż¬Üš 5#f żäܚ‘?Ā4Ž‘S@The–€Primary“Mo`del:“ASM“ó)ąÉŒ cmbsy10ŌBŸĢĢó$2Ē@Écmbx8Ļ1ŽŽŸ8y‘?²The›ōdoGorw•øća“y˜section˜in˜Lamp•Gort's˜program˜do“es˜not˜giv•øće˜us˜an“y˜indication˜ho“wޤ ‘?customer–]µi“²is“suppšGosed“to“p˜erform“reading.“Should“it“read“the“registers“µRŸ’“jŽ‘P ²inŽ”‘?the–#Horder“givšøćen“b˜y“the“indices,“in“the“rev˜ersed“order?“Should“it“get“help“and“useŽ”‘?v‘’qĒassal–Œdagenšøćts,“one“pGer“eac˜h“µRŸ’“jޑò?“There“are“man˜y“other“pGossibilities.“T‘’*Ŗo“re ect“theŽ”‘?situation–§æin“propšGer“generalitøćy‘’*Ŗ,“our“primary“ASM‘§Ŗmo˜del“øBŸ’±1Ž‘$2²includes“no“readingŽ”‘?instructions–t¬whatsoGevšøćer.“Instead,“w˜e“will“require“that“runs“of“øBŸ’±1Ž‘ń²satisfy“certainŽ”‘?prošøćvisos–UUthat“guaran˜tee“that“reading“is“pGerformed.ŽŸ 8y‘?Ė4.1Ž‘Y1¾The–ÕTProgram“of“ó3ąÉŒ cmbsy10ŽBŸ’ó.f$Ųcmbx7Ł1ŽŽŸ8y‘?²The–³ASM‘²Ühas“only“one“program,“used“bšøćy“all“customers,“whic˜h“has“ v˜e“rules.“TheŽ”‘?arrašøćy–žmµA²(µX:©;‘ŖØY‘8ä²)“represen˜ts“the“arra˜y“µn²[µY‘8ä²]“of“the“program,“priv‘’qĒate“to“customer“µX‘Čā².Ž”‘?W‘’*Ŗe–%nassume“that“initially“all“registers“ha•øćv“e–%nv‘’qĒalue“0,“all“customers“are“in“moGdeŽ”‘?satis ed,–_and“all“elemenšøćts“of“the“arra˜y“µA²(µX:©;‘ŖØY‘8ä²)“are“undef.“W‘’*Ŗe“assume“that“theŽ”‘?idenšøćti ers–ŽWof“the“µN‘õr²customers“are“distinct“natural“n˜um˜bGers“µ<‘ĒN‘².“V‘’*Ŗariables“µX:©;‘ŖØYŽ”‘?²will–UUrange“o•øćv“er‘UUcustomers.ŽŸ8y‘?ĪStaøćrtŽŽ”‘Næ÷Ģif–?żmode(me)“=“satisfied“thenŽŽ”‘^īA(me,me)–?ż:=“1,“R(me)“:=“1,“mode(me)“:=“doorwayŽŽŸĘĒ‘?ĪTickøćetŽ©ĘĒ‘Næ÷Ģif–?żmode(me)“=“doorway“and“ø8µY‘’üø6²=“Ģme“(A(me,Y)“ø6²=“Ģundef)“thenŽŽ”‘^īA(me,me)–?ż:=“²1–8ą+“maxŽ‘ÕVŸ’“YŽ›ĮĢA(me,Y),–?żR(me)“:=“²1–8ą+“maxŽ‘ÕVŸ’“YŽ˜ĢA(me,Y)ŽŽ”‘^īmode(me)–?ż:=“waitŽŽŸU‘?ĪEntryަ‘Næ÷Ģif–?żmode(me)“=“wait“andŽŽ”‘Næ÷ø8–?żĢY“ø6²=“Ģme“(A(me,Y)=0“or“(A(me,Y),id(Y))“µ>“Ģ(A(me,me),id(me)))“thenŽŽ”‘^īmode(me)–?ż:=“CSŽŽŸU‘?ĪExitަ‘Næ÷Ģif–?żmode(me)“=“CS“thenŽŽ”‘^īmode(me)–?ż:=“doneŽŽŸU‘?ĪFinaleަ‘Næ÷Ģif–?żmode(me)“=“done“thenŽŽ”‘^īR(me)–?ż:=“0,“mode(me)“:=“satisfiedŽŽ”‘^īø8–?żĢY“ø6²=“Ģme“A(me,Y)“:=“undefŽŽŽŽŒ‹ h o#f ż¬Üš 5#f żäܚ‘?Ė4.2Ž‘Y1¾Seman®9tics–ÕTof“ŽBŸ’Ł1ŽŽŸ_l‘?²W‘’*Ŗe–ówšøćould“lik˜e“to“assume“that,“in“an˜y“moGde“di eren˜t“from“ŹSatis e‘’}'d²,“no“customerޤ ‘?stalls–’Ÿforevšøćer;“ev˜en˜tually“it“mak˜es“a“mo˜v˜e“(pro˜vided“a“mo˜v˜e“is“con˜tin˜uously“en-Ž”‘?abled–UUfrom“some“time“on).Ž© FI‘NSince–®ŗin“ASMs“wšøće“ha˜v˜e“no“explicit“notion“of“a“mo˜v˜e“(or“program)“bGeingŽ”‘?enabled,–†Ėand“in“partially“ordered“runs“wšøće“ha˜v˜e“no“explicit“notion“of“time,“bGothŽ”‘?`enabled'–UUand“`con•øćtin“uously–UUfrom“some“time“on'“need“de nitions.ަ‘NThere–0@are“t•øćw“o›0@ob“vious˜candidates˜for˜the˜notion˜of˜a˜program˜bGeing˜enabledŽ”‘?in–#¾a“state.“One“is“based“on“the“inøćtuition“that“a“program“is“enabled“if“it“`getsŽ”‘?došøćwn–‚’to“upGdates',“i.e.“if“in“the“giv˜en“state“it“generates“a“nonempt˜y“set“of“upGdates.Ž”‘?The–ļöother“pGossibilitšøćy“is“that“it“really“c˜hanges“the“state,“i.e.“that“the“upGdateset“isŽ”‘?nonemptšøćy–tand“also“non˜trivial.“W‘’*Ŗe“are“happ˜y“to“sidestep“the“issue“here,“since“forŽ”‘?all–Sprograms“of“this“papGer“the“t•øćw“o–Snotions“will“coincide|whenevšøćer“a“nonem˜tp˜yŽ”‘?set–_of“upšGdates“is“generated,“it“will“also“b˜e“nonšøćtrivial.“Th˜us“w˜e“can“sa˜y“that“aŽ”‘?program–UUis“enabled“in“state“µ‘±.²if“it“prošGduces“a“nonemptøćy“set“of“up˜dates“in“µ[ٲ.ަ‘NW‘’*Ŗe–XŖsašøćy“that“an“agen˜t“µX‘!Œ²stalls“forev˜er“in“a“run“if“(a)“µX‘!Œ²has“a“last“mo˜v˜e,“sa˜yŽ”‘?µt²,–9and“(b)“after“µt“²a“mo•øćv“e›9b“y˜µX‘ö²(the˜program˜of˜µX‘Čā²)˜is˜ev“en“tually˜alw“a“ys˜enabledŽ”‘?(in–UUall“µ[ٲ(µJ‘ö9²)“for“µJ‘½Qø›ĒµI‘Čā²,“for“some“initial“segmenøćt“µI‘śø3˜µt²).ަ‘NW‘’*Ŗe–UUthøćus“assumeޤŅŪ‘?ĖProgress‘ÕTPro®9viso.–UU²No“customer,“in“moGde“other“than“ŹSatis e‘’}'d²,“stalls“forevøćer.Ž”‘NW‘’*Ŗe–½¹consider“the“runs“of“øBŸ’±1Ž‘:,²conšøćtaining“enabled“mo˜v˜es“b˜y“customers“executingޤ ‘?their–•›programs,“sub‘Ž8ject“to“the“Progress“Prošøćviso,“and“also“some“monitored“mo˜v˜es.Ž”‘?Our–*Benšøćtire“kno˜wledge“abGout“monitored“mo˜v˜es“will“bGe“encapsulated“in“explicitŽ”‘?requiremenšøćts–UUD,“W1,“W2“bGelo˜w.ަ‘NW‘’*Ŗe–ūTnošøćw“de ne“in˜terv‘’qĒals“c˜haracterized“b˜y“the“successiv˜e“executions,“b˜y“aŽ”‘?proGcess– ·µX‘Čā²,“of“its“rules“ĪStašøćrt,“Tick˜et,“Entry‘’*Ŗ,“Exit,“Finale“²(also“in“a“partial“order“w˜eŽ”‘?refer–UUto“opGen“inøćterv‘’qĒals“(µa;‘ŖØb²)–Ē=“øfµx“²:“µa“<“x“<“bøg²).ŽŸ_l‘?ĖDe nition‘ÕT1.ŽŽ’‚„@ŹSupp›’}'ose–Š µa“Źis“the“move“of“µX‘RķŹexe˜cuting“ĪStaøćrt“Źrule,“and“µb“Źis“theŽ”‘?next–“ēmove“by“µX‘\ÉŹ(which“has“to“exe‘’}'cute“the“ĪTickøćet“Źrule).ަ‘NThen–"the“interval“µx–˜F²=“(µa;›ŖØb²)–"Źis“a“²doGorw•øća“y–"Źof“µX‘ČāŹ,“and“µa–˜F²=“ĪStaøćrtŽ‘Q-²(µx²)µ;˜b“²=Ž”‘?ĪTickøćetŽ‘YN;²(µx²)Ź.–ĪcIf“µb“Źis“the“last“exe‘’}'cution“of“µX‘—EŹthen“the“²w•øćait‘~£in“terv‘’qĒal‘ĪcµW‘c²(µx²)–Ē=“øfµt“²:“µt“>“bøgŽ”‘?Źis–j2inc›’}'omplete“and“the“²CS‘'ōinøćterv‘’qĒal“ŹCSŽ‘1I²(µx²)“Źis“unde ne˜d.“Supp˜ose“that“µc“Źis“the“nextŽ”‘?move–”žof“µX‘j€Źafter“µb“Ź(ne–’}'c“essarily›”žexe“cuting˜ĪEntry˜Źrule),˜µd˜Źis˜the˜next˜move˜of˜µX‘j€ŹafterŽ”‘?µc›óŹ(ne–’}'c“essarily˜exe“cuting˜ĪExit˜Źrule),˜and˜µe˜Źis˜the˜next˜move˜of˜µX‘»ēŹafter˜µd˜Ź(ne“c“essar-Ž”‘?ily– £exe‘’}'cuting“ĪFinale“Źrule).“Then“µW‘c²(µx²)–Ž*=“(µb;›ŖØc²)– £Źand“CSŽ‘gŗ²(µx²)–Ž*=“(µc;˜d²)Ź,‘ £µc“²=“ĪEntryŽ‘Čײ(µx²)Ź,Ž”‘?µd–Dz=“ĪExitŽ‘\o²(µx²)Ź,‘“ēµe“²=“ĪFinaleŽ‘Ŗ©²(µx²)Ź.ŽŸ$‘N²By–Ö\Progress“Prošøćviso“and“requiremen˜t“D‘Ö;bGelo˜w,“ev˜ery“doGorw˜a˜y“is“complete,Ž”‘?i.e.–ń}eacšøćh“execution“of“ĪSta˜rt“²is“follo˜w˜ed“b˜y“execution“of“ĪTick˜et².“So“is“ev˜ery“crit-Ž”‘?ical–üsection,“i.e.“eacšøćh“execution“of“ĪEntry‘,‰²is“follo˜w˜ed“b˜y“executions“of“ĪExit“²(andŽ”‘?subsequenøćtly‘UUĪFinale²).ŽŽŽŒ‹ q¦ o#f ż¬Üš 5#f żäܚ‘N²The–ĢFprogram“of“customer“µX‘•(²writes“to“lošGcations“mo˜deŽ‘h¼(µX–Čā²)µ;›ŖØRDz(µX“²)µ;˜A²(µX:©;˜Y‘8ä²)Ÿü^’±2ŽŽ‘|s²,ޤ ‘?where–DloGcations“µA²(µX:©;‘ŖØY‘8ä²)“with“µY‘’üø6²=‘ǵX‘ ²are“only“cleaned“up“(that“is“set“to“undef‘Ē)Ž”‘?bšøćy–N,µX‘²(in“ĪFinale²)“and“someb•Go“dy–N,else“writes“more“meaningful“information“in˜toŽ”‘?these‘UUloGcations.Ž”‘NOur–F-program“co•øćv“ers–F-all“but“the“reading“actions.“Since“our“de nitions“do“notŽ”‘?allošøćw–Ų`partially“kno˜wn“programs',“i.e.“a“con˜trolled“agen˜t“can“do“no“more“thanŽ”‘?what–‡Whis“program“instructs“him“to“do,“more“meaningful“v‘’qĒalues“ha•øćv“e–‡Wto“bGe“writtenŽ”‘?there–UUbšøćy“the“en˜vironmen˜t,“i.e.“b˜y“someb•Go“dy‘UUelse.Ž”‘NW‘’*Ŗe–Āassume“that“lošGcations“mo˜deŽ‘_(µX–Čā²)µ;›ŖØRDz(µX“²)µ;˜A²(µX:©;˜X“²)–Āare“also“conšøćtrolled“b˜y“X,Ž”‘?i.e.–°^that“no“other“(knošøćwn“or“unkno˜wn)“agen˜t“ma˜y“write“there.“This“is“justi edŽ”‘?bšøćy–ĒbLampGort's“algorithm:“other“customers,“as“w˜ell“as“the“en˜vironmen˜t,“ha˜v˜e“noŽ”‘?business–UUwriting“to“moGdeŽ‘ńĖ(µX–Čā²)µ;›ŖØRDz(µX“²)µ;˜A²(µX:©;˜X“²).Ž”‘NThis–7assumption“implies“that“µRDz(µY›8ä²)“is“foGcused,“for“all“customers“µY˜²,“and,“bøćyŽ”‘?the–UUprogram“and“fact“2,“for“all“mo•øćv“es–UUµt“²in“a“run“of“øBŸ’±1Ž‘|s²,Ž©ļƒ‘?ĖCorollary‘ÕT1.ŽŽ’€–µRDz(µY‘8ä²)ŸĪ:ĶPr–ĮeŽ‘ t©ŸĪ:±(“t±)Ž‘ˆ–Źis–N•indisputable“i “µt“Źc–’}'omp“ar“es–N•to“al‘‚Ųl“ĪSta•øćrtµ;‘ŖØĪTick“et‘N•ŹandŽ”‘?ĪFinale–“ēŹmoves“of“Y.ަ‘N²T‘’*Ŗo›īa•øćv“oid˜repGetitiv“e˜case˜distinctions˜for˜customers˜whic“h˜(bGeing˜satis ed)Ž”‘?ha•øćv“e–Ū register“0,“and“of“customers“whicšøćh“happGen“to“receiv˜e“the“same“tic˜k˜et,“w˜eŽ”‘?inšøćtroGduce–»the“follo˜wing“notation.“If“µf‘-J²is“a“function“from“customers“to“naturalŽ”‘?n•øćum“bGers,‘UUletŽŸńǟoŠ’Œ­[µf‘ŸūŽ’·0Ž‘įȲ(µX›Čā²)–Ē=“Ÿńę^«ŽŸśG‘ ńĮµN‘Oūø–8ąµf‘²(µX˜²)“+“idŽ‘ Ž7(µX˜²)µ;Ž‘eJ²if‘UUµf‘²(µX˜²)“µ>“²0;ŽŽ”‘ ńĮø1µ;Ž‘eJ²otherwise.ŽŽŽŽŽŸaR‘NLet–#»µX:©;›ŖØY‘\Ÿ²range“o•øćv“er–#»customers,“and“µx;˜y‘”²o•øćv“er›#»doGorw“a“ys˜of˜customers˜µX:©;‘ŖØYŽ”‘?²respGectivøćely‘’*Ŗ.Ž”‘NW‘’*Ŗe–UUabbreviate“1–8ą+“maxŽ‘ÕVŸ’“YŽ‘lEµA²(µX:©;‘ŖØY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(ó7Ęs6‘cmss8āTickĖetŽ‘”±(“x±))Ž‘4€Š²as‘UUµT‘c²(µx²).Ž”‘NThe–v”declarativšøće“requiremen˜ts,“sa˜ying“what“reads“need“bGe“done,“are“then“(withŽ”‘?µx–UU²bšGeing“an“arbitrary“do˜orw•øća“y–UUof“customer“µX‘Čā²)ŽŸģ7‘?ĖDŽŽ‘LŃIJEacšøćh–iexecution“of“ĪSta˜rt“²b˜y“µX‘åK²completes“to“a“doGorw˜a˜y“µx².“F‘’*Ŗor“eac˜h“µx²,“for“eac˜hŽ”‘PµY‘ßuø6²=›¦‘µX‘¤M²there–Ūkis“a“mo•øćv“e–Ūkµb˜ø2˜µx²,“sucøćh“that“µA²(µX:©;‘ŖØY–8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(āTickĖetŽ‘”±(“x±))Ž‘4ŃƲ=˜µRDz(µY“²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)ŽŽ”‘P²(thøćus‘UUµT‘c²(µx²)–ǵ>“RDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘šø6²=“undefŽ‘ńĒ).Ž© ü“‘?ĖW1ŽŽ‘U£ˆ²If–hµW‘c²(µx²)“is“complete,“then“for“eacšøćh“µY‘Jø6²=‘ęfµX‘1²there“is“a“mo˜v˜e“µb–ęfø2“µW‘c²(µx²),‘hsuc˜hŽ”‘Pthat›UUµRDz(µY–8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘š²=‘ǵA²(µX:©;‘ŖØY“²)ŸĪ:±PreŽ‘ <ŸĪ:(āEntryq±(āx±))Ž‘0ßk²(thøćus˜µT‘cŸü^’·0Ž‘1Ȳ(µx²)–ǵ<“Rǟü^’·0Ž‘ā²(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘šø6²=“undefŽ‘ńĒ).ަ‘?ĖW2ŽŽ‘U£ˆ²If–¤CµW‘c²(µx²)“is“incomplete,“then“for“some“µY‘.1ø6²=‘õMµX‘m%²there“is“an“in nite“cøćhainŽ”‘PµbŸ’±1Ž–Jɵ<›ĪVbŸ’±2Ž“µ<˜ø–ŖØ“ޑҪ²of›Y­mo•øćv“es˜in˜µW‘c²(µx²),˜suc“h˜that,˜for˜eac“h˜µn²,˜µRǟü^’·0Ž‘ā²(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“bŸóO Ś\cmmi5³nŽ‘ēl±)Ž‘Dµ<‘ĪVT‘cŸü^’·0Ž‘1Ȳ(µx²)Ž”‘P(thøćus–UUalso“µRDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“bŸ³nŽ‘ēl±)Ž‘ø6²=‘ĒundefŽ‘ńĒ).ŽŸļƒ‘ND‘i¬tells–ióus“that“the“v‘’qĒalue“of“µRDz(µY‘8ä²),“appGearing“in“the“arrašøćy“at“ĪTick˜etŽ‘ø.²(µx²),“isŽ”‘?read–š­in“µx².“W1“sašøćys“that“a“pGermission“to“go“is“obtained“b˜y“executing,“for“eac˜hŽ”‘?µY‘8ä²,–_Ła“successful“read“in“µW‘c²(µx²),“while“W2“tells“us“that“µX‘(»²mašøćy“bGe“prev˜en˜ted“fromŽ‘?Ÿ_Ήff8ēϟ LĶ‘ĄŸü-=Ć2ŽŽŽŽ‘ ¾b¾9y–ņ[Gur95Ž‘CŽ]“the“ocial“notation“for“these“lošAĒcations“is“(mo˜deŽ‘×öó5łž" cmmi9Ä;–ŠŖX›“[¾)Ä;“¾(ÄR>;“X˜¾)Ä;“¾(ÄA;“¾(ÄX0Ķ;“Y‘8¾));ޤ ‘ since–kin“the“simple“cases“ošAĒccurring“in“this“pap˜er,“no“am•¾9biguit“y›kma“y˜arise,˜w“e˜shallŽ”‘ use–Tthe“applicativš¾9e“term“notation“as“abAĒo˜v˜e“also“for“loAĒcations.ŽŽŽŒ‹  o#f ż¬Üš 5#f żäܚ‘?²going–Ēhonly“bøćy“executing,“for“some“µY‘¾ø6²=‘…7µX‘Čā²,“an“in nite“sequence“of“unsuccessfulޤ ‘?reads– in“µW›c²(µx²),“where“a“read“µb–>Ÿø2“µW˜²(µx²)– from“µRDz(µY‘8ä²)“on“bGehalf“of“µX‘eļ²is“successfulŽ”‘?if–¶$µRǟü^’·0Ž‘ā²(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘ŗņµ>‘hpT‘cŸü^’·0Ž‘1Ȳ(µx²).“It“turns“out“that“D,“W1“and“W2“is“all“that“wøće“need“toŽ”‘?knošøćw–ØabGout“reading“actions“in“order“to“pro˜v˜e“correctness“and“deadloGc˜k{freedomŽ”‘?of‘UUøBŸ’±1Ž‘|s².Ž© ¼N‘NRequiremenšøćts–3ĘD‘3and“W1“sa˜y“that,“for“eac˜h“µY‘8ä²,“there“is“a“mo˜v˜e“µb²(µY‘8ä²)“in“µx²,Ž”‘?respGectivšøćely–XµW‘c²(µx²),“ha˜ving“some“propGert˜y‘’*Ŗ.“Remark“that,“without“loss“of“general-Ž”‘?it•øćy‘’*Ŗ,›$w“e˜can˜assume˜that˜these˜mo“v“es˜µb²(µY‘8ä²)˜are˜all˜distinct.˜SuppGose˜namely˜that,Ž”‘?in–ŗD‘Šor“W1,“wšøće“ha˜v˜e“µb–’j²=“µb²(µYŸ’±1Ž‘|s²)“=“ø–ŖØ“Ž‘©{²=“µb²(µYŸ’“kŽ‘됲).–ŗThen“w˜e“can“replace“µb“²with“µkŽ”‘?²distinct–’ monitored“mo•øćv“es›’ whic“h,˜in˜the˜partial˜order,˜follo“w˜and˜precede˜exactlyŽ”‘?the–^£same“mo•øćv“es–^£as“µb“²doGes.“It“is“easy“to“see“that“this“replacemenšøćt“lea˜v˜es“us“withŽ”‘?a–V-legitimate“run,“with“exactly“the“same“partial“order“of“customers'“mo•øćv“es.‘V-AŽ”‘?remark–(Śof“the“same“kind“applies“also“to“sequences“of“mo•øćv“es–(Śclaimed“bøćy“W3,“butŽ”‘?wøće–UUshall“not“need“that“case.ަ‘NThe–ŠĀreader“familiar“with“[BGR95Ž‘ JÆ]“mighøćt“notice“that,“what“in“similar“re-Ž”‘?quiremenšøćts–­_there“w˜ere“tempšGoral“conditions“on“some“monitored“lo˜cations,“takøćesŽ”‘?here–(µ(and“in“the“next“section)“the“shapšGe“of“conditions“on“b˜ehašøćviour“of“unkno˜wnŽ”‘?agenšøćts.–‚€The“role“of“some“time“momen˜ts“in“proGofs“of“[BGR95Ž‘ JÆ]“th˜us“turns“out“toŽ”‘?bGe–UUthat“of“place“holders“for“monitored“mo•øćv“es.ŽŸ#­‡‘?Ā5Ž‘S@Correctness–€and“Deadlo`c k{F‘žąreedom:“The“ASM“ŌBŸĢĢĻ2ŽŽŸ­‡‘?²W‘’*Ŗe–gśde ne“an“ASM‘g“expressing“a“`higher“levšøćel'“view“of“the“Bak˜ery“Algorithm,Ž”‘?similar–vöto“øBŸ’±1Ž‘ói²but“with“the“arrašøćy“abstracted“a˜w˜a˜y‘’*Ŗ.“The“relev‘’qĒan˜t“datum“to“bGeŽ”‘?describGed–@éabstractly“is“the“Źticket“²assigned“to“a“customer“µX‘ ˲(and“written“inøćtoŽ”‘?its–˜Čregister“µRDz(µX‘Čā²))“when“µX‘aŖ²lea•øćv“es–˜Čthe“doGorw•øća“y–˜Čand“enšøćters“the“w˜ait“section.“W‘’*ŖeŽ”‘?inøćtrošGduce–ˆfor“this“purp˜ose“t•øćw“o–ˆmonitored“functions,“b˜o˜olean“v‘’qĒalued“Ready“andŽ”‘?inšøćteger–UUv‘’qĒalued“µT‘c²,“expressing,“respGectiv˜ely‘’*Ŗ,“readiness“of“the“tic˜k˜et“and“its“v‘’qĒalue.ަ‘NThe–9relev‘’qĒanšøćt“momen˜t“to“bGe“analyzed“is“the“momen˜t“at“whic˜h“a“proGcess“withŽ”‘?a›ytic•øćk“et˜is˜allo“w“ed˜to˜en“ter˜the˜critical˜section.˜This˜`pGermission˜to˜go'˜will˜alsoŽ”‘?bGe–UUrepresenšøćted“b˜y“a“monitored“function,“Go.ަ‘NW‘’*Ŗe–™1will“impGose“requiremenšøćts“on“the“en˜vironmen˜t“and“monitored“mo˜v˜es,“re-Ž”‘?spšGonsible–};for“the“v‘’qĒalues“of“Ready‘’*Ŗ,“µT‘ąŹ²and“Go,“whicøćh“will“b˜e“shošøćwn“to“guaran˜teeŽ”‘?the–&6correctness“and“deadloGcšøćk{freedom“of“the“higher“lev˜el“ASM‘&*øBŸ’±2Ž‘|s².“W‘’*Ŗe“will“thenŽ”‘?shošøćw–UUthat“these“requiremen˜ts“are“correctly“implemen˜ted“in“øBŸ’±1Ž‘|s².ŽŸ!­‡‘?Ė5.1Ž‘Y1¾The–ÕTProgram“of“ŽBŸ’Ł2ŽŽŸ&$‘?ĪStaøćrtŽŸń9‘Næ÷Ģif–?żmode(me)“=“satisfied“thenŽŽ”‘^īR(me)–?ż:=“1,“mode(me)“:=“doorwayŽŽŽŽŒ‹ ’ņ o#f ż¬Üš 5#f żäܚ‘?ĪTickøćetޤ†Ó‘Næ÷Ģif–?żmode(me)“=“doorway“and“Ready(me)“thenŽŽ© ‘^īR(me)–?ż:=“T(me),“mode(me)“:=“waitŽŽ”‘?ĪEntryŽ”‘Næ÷Ģif–?żmode(me)“=“wait“and“Go(me)“thenŽŽ¦‘^īmode(me)–?ż:=“CSŽŽ”‘?ĪExitŽ”‘Næ÷Ģif–?żmode(me)“=“CS“thenŽŽ¦‘^īmode(me)–?ż:=“doneŽŽ”‘?ĪFinaleŽ”‘Næ÷Ģif–?żmode(me)“=“done“thenŽŽ¦‘^īmode(me)–?ż:=“satisfied,“R(me)“:=“0ŽŽŸ†Ó‘?Ė5.2Ž‘Y1¾Seman®9tics–ÕTof“ŽBŸ’Ł2ŽŽ”‘?²The–{3ASM‘{*øBŸ’±2Ž›÷¦²is“similar“to“that“of“øBŸ’±1Ž˜²except“for“the“fact“that“the“arraøćy“is“gone.ަ‘?In–ć/particular“wšøće“assume“the“Progress“Pro˜viso“(for“kno˜wn“agen˜ts,“i.e.“customers).ަ‘?The–å9role“of“the“arrašøćy“is“tak˜en“o˜v˜er“b˜y“three“monitored“functions,“Ready‘’*Ŗ,“µTަ‘?²and–Go.“LoGoking“at“øBŸ’±1Ž‘|s²,“ReadyŽ‘·Æ(µX›Čā²)“and“µT‘c²(µX˜²)“can“bGe“seen“as“standing“for“theަ‘?abbreviations–žused“there,“while“GoŽ‘Żć(µX‘Čā²)“can“bGe“inøćterpreted“as“the“guard“of“theަ‘?ĪEntry‘xā²rule,›UUø8µY‘’üø6²=–ǵX‘Čā²(µA²(µX:©;‘ŖØY‘8ä²)“=“0˜or˜(µA²(µX:©;–ŖØY›8ä²)µ;“id²(µY˜²))–ǵ>“²(µA²(µX:©;–ŖØX›Čā²)µ;“id²(µX˜²))).ަ‘NThe–UUASM“øBŸ’±2Ž‘ŃȲprošøćvides“ho˜w˜ev˜er“no“means“to“compute“Ready‘’*Ŗ,“µT‘øä²and“Go.ަ‘NOur– rst“requiremenšøćt“sa˜ys“that“ev˜ery“in˜terested“customer“ev˜en˜tually“obtainsަ‘?his‘UUtic•øćk“et:ŽŸhˆ‘?ĖC0ŽŽ‘R4²Eacšøćh–Ūsexecution“of“ĪSta˜rt²,“b˜y“a“customer“µX‘Čā²,“completes“to“a“doGorw˜a˜y“µx².“F‘’*Ŗorަ‘Peacøćh–UUµx“²the“v‘’qĒalue“µT‘c²(µX‘Čā²)ŸĪ:±PreŽ‘ <ŸĪ:(āTickĖet±(āx±))Ž‘3dž²is“indisputable.Ž”‘NThe–½indisputable“v‘’qĒalue“of“µT‘c²(µX‘Čā²)ŸĪ:±PreŽ‘ <ŸĪ:(āTickĖet±(āx±))Ž‘4"f²will“bšGe,“likøće“b˜efore,“denoted“bøćyަ‘?µT‘c²(µx²).–Ŗ¢In“order“to“express“the“rest“of“our“conditions“on“the“arraøćy“in“terms“of“µTަ‘?²and–UUGo,“wøće“need“some“additional“notation“and“terminology‘’*Ŗ.ަ‘NF‘’*Ŗor–°ÖopGen“inšøćterv‘’qĒals“in“a“partial“order“w˜e“also“use“(µa;›ŖØb²)– Bµ<“²(µc;˜d²)–°Öif“µb– Bø“µc²,ަ‘?and–Ģsašøćy“that“the“t˜w˜o“in˜terv‘’qĒals“are“concurren˜t“if“neither“µb– ø“µc–̲nor“µd– ø“µa².‘ĢNoteަ‘?that– Bconcurrency“doGes“not“necessarily“imply“o•øćv“erlap,– Bi.e.“existence“of“commonަ‘?elemenšøćts;–UUit“in“general“just“allo˜ws“it.Ÿü^’±3ŽŽŽ¦‘N²Sometimes–L£wšøće“shall“also“compare“elemen˜ts“with“in˜terv‘’qĒals:“µc–Ē<“²(µa;‘ŖØb²)–L£if“µc–Ēø“µa²,ަ‘?likøćewise–UUfor“µ>².ަ‘NThis–ųŒordering“will“help“us“to“formalize“the“idea“that“tic•øćk“ets–ųŒincrease“togetherަ‘?with›ČdoGorw•øća“ys˜(see˜C2˜bGelo“w).˜This˜should˜also˜apply˜in˜a˜w“a“y˜to˜concurren“tŽ‘?Ÿ)Љff8ēϟ LĶ‘ĄŸü-=Ć3ŽŽŽŽ‘ ¾Note›Īpho•¾9w“ev“er˜that,˜if˜in“terv‘’|rals˜are˜in“terpreted˜as˜in“terv‘’|rals˜on˜the˜partial˜order˜ofޤ ‘ initial–(tsegmenš¾9ts,“with“(Äa;‘ŠŖb¾)“con˜taining“all“segmen˜ts“con˜taining“Äa“¾but“not“Äb¾,“thenŽ”‘ concurren•¾9t›Tin“terv‘’|rals˜indeed˜o“v“erlap.ŽŽŽŒ‹  Æ o#f ż¬Üš 5#f żäܚ‘?²doGorw•øća“ys;–°@these“are“ordered“bšøćy“the“follo˜wing“relation“ø²,“bGorro˜w˜ed“from“its“linearޤ ‘?order–UUanalog“of“[Abr93Ž‘ųč].Ž© %4‘NLet–UUµX‘śø6²=‘ǵY‘8ä²,“and“let“µx;‘ŖØy‘±.²range“o•øćv“er›UUdoGorw“a“ys˜of˜µX:©;‘ŖØY‘Ž9²respGectiv“ely‘’*Ŗ.ŽŸŗ‘?ĖDe nition‘ÕT2.ŽŽ’‚„@µx–3óTqŌ lasy10»“µy›,fŹif–Šµx“Źand“µy˜Źar›’}'e“c˜oncurr˜ent“and“µT‘cŸü^’·0Ž›1Ȳ(µx²)–ǵ<“T‘cŸü^’·0Ž˜²(µy[ٲ)Ź.–ŠF‘’;¼urther,“µx–Ēø“µyŽ”‘?Źif›“ēµx–8໓µy‘ļĄŹor˜µx–Ē<“y[ŁŹ.ޤ”Š‘?ĖLemma‘ÕT4.ŽŽ‘uøŃµx–Ēø“µy‘ļĄŹor‘“ēµy‘"ńø“µxŹ.Ž”‘?Pr–’}'o“of.ŽŽ‘^UI²Note–CŚthat“µT‘cŸü^’·0Ž›1Ȳ(µy[ٲ)–TŸø6²=“µT‘cŸü^’·0Ž˜²(µx²)–CŚfor“µX‘ø6²=‘TŸµY‘8ä²,“while“t•øćw“o›CŚdoGorw“a“ys˜of˜the˜sameŽŸ ‘?customer–UUcan“nevšøćer“bGe“concurren˜t.’½¼øuŽ’½¼tŽŽ”‘?²Our–UUother“conditions“are“thenŽŸ”Š‘?ĖC1ŽŽ‘R4µT‘c²(µx²)–UUis“a“pGositivšøće“in˜teger“µ>‘Dz1.ަ‘?ĖC2ŽŽ‘R4²If–UUµy‘"ń<›Ēx“²then“either“ĪFinaleŽ‘8ę²(µy[ٲ)˜µ<˜ĪTickøćetŽ‘S²(µx²)“or“µT‘cŸü^’·0Ž–1Ȳ(µy[ٲ)˜µ<˜T‘cŸü^’·0Ž“²(µx²).ަ‘?ĖC3ŽŽ‘R4²If–\īµW‘c²(µx²)“is“complete,“then,“for“evšøćery“µY‘ ¦ø6²=‘ÓµX‘Čā²,“there“exists“a“mo˜v˜e“µb–ÓĀø2“µW‘c²(µx²),ޤ ‘Psucšøćh–UUthat“µT‘cŸü^’·0Ž‘1Ȳ(µx²)–ǵ<“Rǟü^’·0Ž‘ā²(µY–8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘§×²(th˜us‘UUµRDz(µY“²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘šø6²=‘ĒundefŽ‘ńĒ).ަ‘?ĖC4ŽŽ‘R4²If–UUµW›c²(µx²)“is“incomplete,“then“there“is“a“µy‘"ńø‘ǵx“²with“µW˜²(µy[ٲ)“incomplete.ŽŸoœ‘NIn•øćtuitiv“ely‘’*Ŗ,–×C2“sašøćys“that“tic˜k˜ets“respšGect“the“temp˜oral“precedence“of“do˜orw•øća“ysŽ”‘?with–lNLemma“5,“if“one“of“the“w˜aiting“sections“is“complete“then“so“are“the“otherŽ”‘?t•øćw“o,–Ŗand“wšøće“ha˜v˜e“CSŽ‘q#(µx²)–T=µ<“²CSŽ›[(µy[ٲ)“µ<“²CSŽ˜(µzp—²)“µ<“²CSŽ˜(µx²)–Ŗwhicøćh“is“impGossible.“So“allŽ”‘?three–Ēwšøćaiting“sections“m˜ust“bGe“incomplete.“Th˜us“w˜e“can“apply“C2“to“obtain“alsoŽ”‘?µT‘cŸü^’·0Ž›1Ȳ(µzp—²)–ǵ<“T‘cŸü^’·0Ž˜²(µx²),–UUwhicøćh“is“impGossible.’»½ĻøuŽ’»½ĻtŽŽ¤¶½‘?ĖLemma‘ÕT7.ŽŽ‘uøŃ(DeadloQĒc®9k‘ÕTfreedom)–“ēŹEvery“µW‘c²(µx²)“Źis“c‘’}'omplete.Ž”‘?Pr–’}'o“of.ŽŽ‘^UI²By–Œ³corollary“2“(and“ nite“history)“ø“²is“wøćell{founded.“Then“C4“is“preciselyŽ© ‘?the–UUinduction“principle“required“to“establish“the“claim.‘e¦ŸøuŽ‘e¦ŸtŽŽ”‘N²This–UUsection“is“summarized“in“the“folloøćwingŽŸ¶½‘?ĖTheorem‘ÕT1.ŽŽ‘}Ē ŹDo–’}'orways›“ĪTickøćetŽ‘S²(µy[ٲ)‘Ŗ©(ii)˜if˜µy‘"ńø“µx˜²then˜µb“>“ĪFinaleŽ‘Ŗ©²(µy[ٲ).ŽŸ)HŁ‘NFirst–—]wšøće“deriv˜e“the“desired“con˜tradiction“from“the“claim,“and“second“w˜e“pro˜v˜eŽ”‘?the‘UUclaim.Ž©’6‘NSo–xśsuppšGose“that“the“claim“is“true“and“let“µb“²b˜e“as“in“the“claim.“Then“µRDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)ŽŽ”‘?²has–ÕKan“indisputable“v‘’qĒalue,“and“µb“²thšøćus“compares“to“all“mo˜v˜es“of“µY‘/²that“c˜hangeŽ”‘?µRšDz(µY‘8ä²).–N What“is“the“v‘’qĒalue“of“µR˜²(µY‘8ä²)“in“PreŽ‘xø(µb²)?“W‘’*Ŗe“ha•øćv“e›N t“w“o˜pGossible˜scenarios.Ž”‘?Scenario–{lA:“all“µy‘blø‘“µx²;“then“µb“²succeeds“evšøćery“ĪFinaleŽ‘^ż²(µy[ٲ)“and“th˜us“µRDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘Y²=‘“0.Ž”‘?Scenario–ŠĪB:“there“is“some“µy‘,§²with“ĪTickøćetŽ‘ ²(µyš[ٲ)–”įµ<“b“ø“ĪFinaleŽ‘xr²(µy˜²);–ŠĪthen“µRDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘ēc²=Ž”‘?µT›c²(µy[ٲ).–q*T‘’*Ŗo“summarize,“if“µb“²is“as“in“the“claim,“then“µRDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘Ƭ²is“either“0“or“µT˜²(µy[ٲ),Ž”‘?so–UUthat“µRǟü^’·0Ž‘ā²(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘šø‘ǵT‘cŸü^’·0Ž‘1Ȳ(µy[ٲ).ަ‘NThe–wŅv‘’qĒalues“of“µRšDz(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘ŹT²and“of“µR˜²(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“bŸ³nŽ‘ēl±)Ž‘±Ą²for“evøćery“µn“²are“indisputable.Ž”‘?Mo•øćv“es–µb“²and“µbŸ’“nŽ‘ Œ–²thšøćus“all“compare“with“ev˜ery“mo˜v˜e“of“µY‘Sü²whic˜h“c˜hanges“µRDz(µY‘8ä²).Ž”‘?It–•&is“easy“to“see“that“anøćy“µbŸ’“nŽ‘¢ņø6µ<‘1tb“²satis es“(i)“and“(ii)“in“the“claim.“But“then,“asŽ”‘?sho•øćwn›”abGo“v“e,˜µRǟü^’·0Ž‘ā²(µY‘8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(“bŸ³nŽ‘ēl±)Ž‘ø‘ǵT‘cŸü^’·0Ž‘1Ȳ(µy[ٲ),˜whic“h˜con“tradicts˜the˜propGert“y˜of˜µbŸ’“nŽ‘²in˜W2.Ž”‘?Th•øćus›UUev“ery˜µbŸ’“nŽ‘8–µ<‘Ēb²,˜whic“h˜con“tradicts˜ nite˜history‘’*Ŗ.ަ‘NIt–UUremains“to“pro•øćv“e–UUthe“claim.ަ‘NT‘’*Ŗo›ļpro•øćv“e˜the˜claim,˜note˜that,˜for˜µy‘ińø‘µx²,˜CSŽ‘G (µy[ٲ)˜is˜de ned˜and˜complete,˜b“yŽ”‘?the–ā`assumption“that“µW‘c²(µy[ٲ)“is“complete“and“the“Progress“Proøćviso.“It“suces“toŽ”‘?pro•øćv“e–ĮØthat“there“is“at“most“one“µy‘×z>‘{”x².“The“sequence“of“doGorw•øća“ys–ĮØof“µY‘śŒ²is“thenŽ”‘? nite:–*}bšøćy“ nite“history‘’*Ŗ,“it“has“ nitely“man˜y“elemen˜ts“µ<‘Ēx²,“b˜y“corollary“2“ nitelyŽ”‘?man•øćy›×Éelemen“ts˜concurren“t˜to˜µx².˜Th“us˜µY‘­²has˜a˜last˜mo“v“e,˜sa“y˜µeŸ’“YŽ‘ģG².˜By˜ProgressŽ”‘?Prošøćviso,–¬ µeŸ’“YŽ‘ ˜T²can“only“bGe“a“ĪTick˜et“²or“a“ĪFinale“²mo˜v˜e.“Since“all“µbŸ’“nŽ‘q~²,“b˜y“corollary“1,Ž”‘?compare–łüto“µeŸ’“YŽ‘ģG²,“bšøćy“ nite“history‘’*Ŗ,“for“sucien˜tly“large“µn“²w˜e“ha˜v˜e“µbŸ’“nŽ‘ Kµ>‘كeŸ’“YŽ‘ģG².“W‘’*ŖeŽ”‘?can–UUthen,“for“claimed“µb²,“takšøće“an˜y“µbŸ’“nŽ‘8–µ>‘ĒeŸ’“YŽ‘ģG².ަ‘NIt–å¼remains“to“pro•øćv“e–å¼that“µY‘ ²has“at“most“one“došGorw•øća“y–å¼µ>‘·Ćx².“Supp˜ose“µx–·Ć<“y[ٲ.Ž”‘?Then,–C÷bšøćy“C2“(with“µx;‘ŖØy‘ŸŠ²pla˜ying“µy[Ł;‘ŖØx“²respGectiv˜ely),“µT‘cŸü^’·0Ž›1Ȳ(µx²)–Tϵ<“T‘cŸü^’·0Ž˜²(µy[ٲ)–C÷(since“µW‘c²(µx²)Ž”‘?is–Ŗ•incomplete).“If“µW‘c²(µy[ٲ)“wšøćere“complete,“b˜y“C3“there“w˜ould“bGe“a“µc–U-ø2“µW‘c²(µy[ٲ)‘Ŗ•suc˜hŽ”‘?that–X̵Rǟü^’·0Ž‘ā²(µX‘Čā²)ŸĪ:±PreŽ‘ <ŸĪ:(“c±)ޑئµ>›w‡T‘cŸü^’·0Ž‘1Ȳ(µy[ٲ).“But“since“µx˜<˜y‘Ó`<˜c²,“wšøće“also“ha˜v˜e“µc–w‡ø2“µW‘c²(µx²)‘XĢandŽ”‘?µRDz(µX‘Čā²)ŸĪ:±PreŽ‘ <ŸĪ:(“c±)Ž‘(7²=‘ǵT›c²(µx²),–G©so“µT˜Ÿü^’·0Ž‘1Ȳ(µx²)–ǵ>“T˜Ÿü^’·0Ž‘1Ȳ(µy[ٲ),–G©whicšøćh“is“impGossible.“Th˜us“µW‘c²(µy[ٲ)“is“incom-Ž”‘?plete,–UUand“µy‘±.²is“the“last“doGorw•øća“y–UUof“µY‘8ä².ަ‘NW‘’*Ŗe›¶—ha•øćv“e˜th“us˜v“eri ed˜that˜C0{C4˜hold˜of˜arbitrary˜runs˜of˜øBŸ’±1Ž‘|s².˜It˜follo“ws˜thatŽ”‘?the–fresults“of“the“previous“subsection,“summarized“in“Theorem“1,“hold“of“øBŸ’±1Ž‘āt²asŽ”‘?wøćell.ŽŽŽŒ‹ĖĖ o#f ż¬Üš 5#f żäܚ‘?Ā6Ž‘S@Realizing–.zthe“Mo`del“with“Reading“Agen ts:“the“ASM‘.fŌBŸĢĢĻ0ŽŽŸ’-‘?Ė6.1Ž‘Y1¾The–ÕTProgram“of“ŽBŸ’Ł0ŽŽŸ’-‘?²Un•øćtil›;Ono“w˜the˜univ“erse˜of˜kno“wn˜agen“ts˜w“as˜pGopulated˜b“y˜customers˜only‘’*Ŗ.˜No“w˜w“eޤ ‘?also›Åha•øćv“e˜another˜kind˜of˜agen“ts.˜They˜presen“t˜one˜w“a“y˜of˜making˜the˜unkno“wnŽ”‘?agenšøćts–UUof“øBŸ’±1Ž‘ŃȲkno˜wn.Ž© ¶Ö‘NF‘’*Ŗormally––Ythe“univšøćerse“of“agen˜ts“splits“in˜to“t˜w˜o“disjoin˜t“univ˜erses:“CustomerŽ”‘?and–ÖzReader.“Customers“and“readers“are“related“bšøćy“sev˜eral“functions.“If“µX‘Ÿ\²andŽ”‘?µY‘öd²are–½€distinct“customers,“then“in“eacšøćh“state“there“is“at“most“one“reader{agen˜tŽ”‘?µrG²(µX:©;‘ŖØY‘8ä²),–UUand“there“are“no“other“readers.ަ‘NIf–ӈµr‘„²is“the“reader“µršG²(µX:©;‘ŖØY‘8ä²),“then“Lord(µr˜²)–D=“µX‘œj²and‘ӈSub‘Ž8ject(µr˜²)“=“µY‘8ä².‘ӈTheŽ”‘?readers–‘will“bGe“created“on“the“ y‘’*Ŗ,“when“needed“(at“ĪStašøćrt“²and“ĪTick˜et“²mo˜v˜es),“andŽ”‘?will–UUself{destruct“when“their“task“is“completed.ŽŸ!’-‘?ĖCustomer‘ĪStaøćrtŽ©ŪW‘Næ÷Ģif–?żmode(me)“=“satisfied“thenŽŽ”‘^īA(me,me)–?ż:=“1,“R(me)“:=“1,“mode(me)“:=“doorwayŽŽ”‘^īø8–?żĢY“ø6²=“Ģme“create-reader(me,“Y,“doorway)ŽŽŸ$‘?ĪTickøćetަ‘Næ÷Ģif–?żmode(me)“=“doorway“and“²(ø8µY‘’üø6²=Ģme)“A(me,Y)“ø6²=“Ģundef“thenŽŽ”‘^īA(me,me)–?ż:=“²1–8ą+“maxŽ‘ÕVŸ’“YŽ›ĮĢA(me,Y),–?żR(me)“:=“²1–8ą+“maxŽ‘ÕVŸ’“YŽ˜ĢA(me,Y)ŽŽ”‘^īmode(me)–?ż:=“waitŽŽ”‘^īø8–?żĢY“ø6²=“Ģme“create-reader(me,“Y,“wait)ŽŽŸ$‘?ĪEntryަ‘Næ÷Ģif–?żmode(me)“=“wait“andŽŽ”‘Næ÷ø8–?żĢY“ø6²=“Ģme“(A(me,Y)=0“or“(A(me,Y),id(Y))“µ>“Ģ(A(me,me),id(me)))“thenŽŽ”‘^īmode(me)–?ż:=“CSŽŽŸ$‘?ĪExitަ‘Næ÷Ģif–?żmode(me)“=“CS“thenŽŽ”‘^īmode(me)–?ż:=“doneŽŽŸ$‘?ĪFinaleަ‘Næ÷Ģif–?żmode(me)“=“done“thenŽŽ”‘^īR(me)–?ż:=“0,“mode(me)“:=“satisfiedŽŽ”‘^ī(ø8–?żĢY“ø6²=“Ģme)“A(me,Y)“:=“undefŽŽŸ$‘N²where‘UUcreate-readerŽ‘<Y(µX:©;–ŖØY‘Ž9;“m²)–UUabbreviates“the“ruleŽŽŽŒ‹Ż\ o#f ż¬Üš 5#f żäܚ‘Næ÷Ģcreate‘?żrŽŽ¤ ‘n?åagent(r)–?ż:=“true,“Reader(r)“:=“trueŽŽ”‘n?åprogram(r)–?ż:=“reader-programŽŽ”‘n?åLord(r)–?ż:=“X,“Subject(r)“:=“YŽŽ”‘n?åmode(r)–?ż:=“mŽŽ”‘Næ÷endcreateŽŽŸ,ČŁ‘?ĖReaderŽ©ŽŪ‘Næ÷ĢA(Lord(me),Subject(me))–?ż:=“R(Subject(me))ŽŽ”‘Næ÷if–?żmode(me)“=“doorway“thenŽŽ”‘^īdestroy-reader(me)ŽŽ”‘Næ÷if–?żmode(me)“=“wait“thenŽŽ”‘^īif–?żR(Subject(me))“=“0ŽŽ”‘n?åor‘?ż(R(Subject(me)),id(Subject(me)))ŽŽ”‘}’ܵ>–?żĢ(A(Lord(me),Lord(me)),id(Lord(me)))“thenŽŽ”‘^īdestroy-reader(me)ŽŽ¦‘N²where‘UUdestroøćy-readerŽ‘A±Ķ(µa²)–UUabbreviates“the“ruleŽŸr‘‘Næ÷Ģagent(a)–?ż:=“false,“Reader(a)“:=“falseŽŽ”‘Næ÷program(a)–?ż:=“undef,“Lord(a)“:=“undef,“Subject(a)“:=“undefŽŽŸŽŪ‘?Ė6.2Ž‘Y1¾Seman®9tics–ÕTof“ŽBŸ’Ł0ŽŽ¦‘?²Semanšøćtics–µäof“øBŸ’±0Ž‘2W²is“lik˜e“that“of“øBŸ’±1Ž‘|s²,“but“considerably“simpler,“since“all“loGcationsŽ”‘?are–×5conšøćtrolled“b˜y“the“kno˜wn“agen˜ts,“and“there“are“no“mo˜v˜es“monitored“b˜y“theŽ”‘?kno•øćwn›Ķragen“ts,˜to˜put˜constrain“ts˜on|it˜is˜all˜in˜the˜programs˜for˜øBŸ’±0Ž‘|s².˜The˜readerŽ”‘?agenšøćts–ģ²are“one“w˜a˜y“to“realize“the“requiremen˜t“that“those“`for-all“commands“inŽ”‘?the›QodoGorw•øća“y˜and˜the˜w“ait˜section˜of˜Lamp•Gort's˜pseudo“co“de˜maøćy˜b“e˜executed˜inŽ”‘?man•øćy›¢²w“a“ys,˜in˜v‘’qĒarious˜sequences,˜all˜at˜once,˜concurren“tly˜etc.'˜In˜fact˜the˜readerŽ”‘?agenšøćts–UUcapture“all“w˜a˜ys“to“realize“that“requiremen˜t,“see“bGelo˜w.Ž”‘NThe–b%only“assumption“wšøće“ha˜v˜e“to“mak˜e,“outside“of“the“program,“is“the“ProgressŽ”‘?Prošøćviso,–UUapplying“here“to“all“agen˜ts,“bGoth“customers“and“readers:Ž©Ēm‘?ĖProgress‘6ōPro®9viso.–Ŗ9²No“reader,“and“no“customer“in“moGde“other“than“ŹSatis e‘’}'d²,Ž”‘?stalls‘UUforevøćer.ަ‘NThe–greader{agenšøćts“are“created“on“the“ y‘’*Ŗ,“and“destro˜y˜ed“upGon“completion“ofŽ”‘?their–·task:“the“e ect“of“destroøćy-readerŽ‘B(µa²),“if“µa“²is“a“reader{agenøćt,“is“returning“µaŽ”‘?²to–UUthe“reservøće.ŽŸŽŪ‘?Ė6.3Ž‘Y1¾ŽBŸ’Ł0Ž‘Ż&Ėrealizes‘ÕTŽBŸ’Ł1ŽŽŸŽŪ‘?²The–z constrainøćts“D,“W1,“W2“can“bGe“read“as“a“rather“direct“description“of“what“theŽ”‘?reader{agenšøćts–do“for“their“customers“in“øBŸ’±0Ž‘|s².“The“fact“that“ev˜ery“run“of“øBŸ’±0Ž‘ v²satis esŽŽŽŒ‹åf o#f ż¬Üš 5#f żäܚ‘?²D,–WōW1,“W2“follošøćws“from“the“programs“and“the“Progress“Pro˜viso“(together“withޤ ‘?the–UUsemanøćtics“describšGed“ab˜o•øćv“e–UUor“in“[Gur95Ž‘QĖ]).Ž© d³‘ND‘§Ōis–Øsatis ed“in“øBŸ’±0Ž‘$s²since,“for“evšøćery“mo˜v˜e“µt“²of“µX‘pā²executing“ĪSta˜rt²,“for“ev˜ery“µY‘’üø6²=Ž”‘?µX‘Čā²,–ōNthere“is“a“reader“µrG²(µX:©;‘ŖØY‘8ä²)“at“PøćostŽ‘PĀ(ĪStaøćrtŽ‘øē²(µx²)).“By“programs“and“the“ProgressŽ”‘?Pro•øćviso›k’eac“h˜of˜these˜readers˜mak“es˜a˜single˜self˜destructiv“e˜mo“v“e,˜whic“h˜is˜theŽ”‘?µb–Ēõ²required“bšøćy“D;“b˜y“programs“and“the“Progress“Pro˜viso“µX‘×²ev˜en˜tually“executesŽ”‘?ĪTickøćet².ަ‘NBy–Š­programs“and“Progress“Prošøćviso,“for“ev˜ery“µY‘’üø6²=‘ǵX‘S²there“is“a“reader“µrG²(µX:©;‘ŖØY‘8ä²)Ž”‘?at‘Ž»PøćostŽ‘ė/(ĪEntryޑꭲ(µx²)).–Ž»That“reader“makšøćes“a“mo˜v˜e“in“µW‘c²(µx²).“F‘’*Ŗor“W1,“W2“it“thenŽ”‘?suces–UUto“noteŽŸ÷}‘?ĖF‘’ «act‘ÕT4.ŽŽ‘f:ŹA‘move–µt“Źby“µrG²(µX:©;‘ŖØY‘8ä²)“Źin“µW‘c²(µx²)“Źis“the“last“such“move“i “it“is“suc–’}'c“essful,Ž”‘?i.e.‘“ēµT‘cŸü^’·0Ž‘1Ȳ(µx²)–ǵ<“Rǟü^’·0Ž‘ā²(µY‘8ä²)ŸĪ:ĶPr–ĮeŽ‘ t©ŸĪ:±(“t±)Ž‘:Ź.ŽŸ’Ė‘N²W1–3°is“namely“satis ed“in“øBŸ’±0Ž‘°#²since,“for“eacšøćh“µY‘r‘ø6²=‘9­µX‘Čā²,“w˜e“can“tak˜e“the“lastŽ”‘?wšøćaiting–UUsection“mo˜v˜e“of“µrG²(µX:©;‘ŖØY‘8ä²)“for“the“claimed“µb².ަ‘NW2–‘is“satis ed“in“øBŸ’±0Ž‘ {²since,“if“all“µrG²(µX:©;‘ŖØY‘8ä²)“for“µY‘’üø6²=‘ǵX‘Yź²ha•øćv“e–‘a“last“mo•øćv“e–‘in“µW‘c²(µx²),Ž”‘?bšøćy–}Progress“Pro˜viso“µX‘ę_²m˜ust“ev˜en˜tually“execute“ĪEntry#².“Th˜us“for“some“µY‘M’ø6²=‘®µXŽ”‘?²the–ZÖreader“µrG²(µX:©;‘ŖØY‘8ä²)“kšøćeeps“reading“forev˜er|tak˜e“the“sequence“of“his“mo˜v˜es“forŽ”‘?µbŸ’±1Ž–C‹µ<›ĒbŸ’±2Ž“µ<˜ø–ŖØ“ޑDzas‘UUclaimed.ަ‘NW‘’*Ŗe›4ha•øćv“e˜th“us˜established˜that˜ev“ery˜run˜µŸ’±0Ž–°‡²of˜øBŸ’±0Ž“²can˜bGe˜viewøćed˜as˜a˜runŽ”‘?of–Ł`øBŸ’±1Ž›|s².“Since“øBŸ’±1Ž˜²,“as“far“as“reading“is“concerned,“can“bGe“viewšøćed“as“a“declarativ˜eŽ”‘?description–zof“algorithmic“bšGehaøćviour,“rather“then“an“algorithm“prop˜er,“µŸ’±0Ž‘ķ²canŽ”‘?also–UUbšGe“seen“as“a“realization“of“b˜ehaøćviour“prescrib˜ed“bøćy“øBŸ’±1Ž‘|s².ަ‘NT‘’*Ŗo–6YbšGe“more“precise,“let“us“inøćtro˜duce“an“appropriate“implemenøćtation“relationŽ”‘?bGet•øćw“een›UUmo“v“es˜and˜runs˜of˜the˜t“w“o˜ASMs.ަ‘NA‘ż¼mo•øćv“e›żŅµtŸ’±0Ž‘zE²b“y˜customer˜µX‘Ę“²in˜øBŸ’±0Ž‘zEŹimplements˜²a˜mo“v“e˜µtŸ’±1Ž‘zE²b“y˜the˜same˜customerŽ”‘?in–5–øBŸ’±1Ž‘² ²if“the“indisputable“pšGortions“of“states“(v‘’qĒalues“of“mo˜deŽ‘Ņ (µX–Čā²)µ;›ŖØRDz(µX“²)µ;˜A²(µX:©;˜X“²))Ž”‘?at‘UUPreŽ›€(µtŸ’±0Ž–|s²)µ;‘ŖØ²PøćostŽ‘(µtŸ’±0Ž“²)–UUcoincide“with“those“at“PreŽ˜(µtŸ’±1Ž–|s²)µ;‘ŖØ²PøćostŽ‘(µtŸ’±1Ž“²)‘UUrespGectivøćely‘’*Ŗ.ަ‘NA‘Žėrun–ŽśµŸ’±0Ž› m²of“øBŸ’±0Ž˜Źimplements“²a“run“µŸ’±1Ž˜²of“øBŸ’±1Ž˜²if“the“partial“order“of“customers'Ž”‘?mo•øćv“es–qßin“µŸ’±0Ž‘īR²is“order{isomorphic“to“the“partial“order“of“customers'“mo•øćv“es–qßin“µŸ’±1Ž‘|s²,Ž”‘?implemenšøćting–Žžit“pGoin˜t˜wise:“whenev˜er“the“isomorphism“maps“a“mo˜v˜e“µtŸ’±0Ž› q²in“µŸ’±0Ž˜²toŽ”‘?a›UUmo•øćv“e˜µtŸ’±1Ž–ŃȲin˜µŸ’±1Ž‘|s²,˜then˜µtŸ’±0Ž“²implemenøćts˜µtŸ’±1Ž‘|s².ަ‘NIn–‹‹these“terms,“wšøće“ha˜v˜e“established“that“øBŸ’±1Ž‘ž²(more“spGeci cally‘’*Ŗ,“D,“W1,“W2)Ž”‘?prošøćvides–Xa“sound“description“of“algorithmic“bGeha˜viour:“øBŸ’±0Ž‘Ė²is“an“algorithm“bGe-Ž”‘?ha•øćving›UUlik“e˜that.˜F‘’*Ŗor˜the˜record,Ž©÷}‘?ĖLemma‘ÕT8.ŽŽ‘uøŃ(Soundness–ÕTof“øBŸ’±1Ž›|sĖ)–“ēŹEach“run“of“øBŸ’±0Ž‘ZŹimplements“a“run“of“øBŸ’±1Ž˜Ź.ŽŸ’Ė‘N²W‘’*Ŗe–ˆŒcan“actually“claim“more.“The“requiremenšøćts“D,“W1,“W2“allo˜w“man˜y“dif-Ž”‘?feren•øćt› ×bGeha“viours.˜Is˜there˜a˜bGeha“viour,˜allo“w“ed˜b“y˜øBŸ’±1Ž‘|s²,˜whic“h˜is˜not˜captured˜b“yŽ”‘?the–?*reader{agenšøćts“of“øBŸ’±0Ž‘|s²?“Not“really‘’*Ŗ.“This“is“the“con˜ten˜t“of“the“follo˜wing“lemma,Ž”‘?expressing–UUa“kind“of“completeness“propGertøćy‘’*Ŗ.ަ‘?ĖLemma‘ÕT9.ŽŽ‘uøŃ(Completeness–39of“øBŸ’±1Ž‘|sĖ)–8ŹEach“run“µŸ’±1ޛޫŹof“øBŸ’±1Ž˜Źis“implemente‘’}'d“by“a“runŽ”‘?µŸ’±0Ž‘ZŹof‘“ēøBŸ’±0Ž‘|sŹ.ŽŽŽŒ‹o#f ż¬Üš 5#f żäܚ‘?ŹPr–’}'o“of.ŽŽ‘^UI²The–µéidea“is“to“transform“µŸ’±1Ž›2\²to“µŸ’±0Ž˜²bšøćy“implemen˜ting“reading“mo˜v˜es“of“µŸ’±1ŽŽ¤ ‘?²with–š'appropriate“mo•øćv“es–š'of“reader{agenšøćts,“pGossibly“ignoring“some“inconsequen˜tialŽ”‘?monitored›tmo•øćv“es˜of˜µŸ’±1Ž‘|s².˜The˜replacemen“t˜proGcess˜is˜done˜in˜the˜order˜of˜µŸ’±1Ž‘|s²,˜thatŽ”‘?is–³Yearlier“read“mo•øćv“es–³Yare“replaced“(or“discarded)“earlier.“The“folloøćwing“conditionsŽ”‘?will–ī-bGe“guaranšøćteed“b˜y“induction“for“ev˜ery“mo˜v˜e“µb“²in˜troGduced“b˜y“replacemen˜t,“forŽ”‘?evšøćery–aæcustomer“µX‘*”²and“ev˜ery“doGorw˜a˜y“µx“²of“µX‘Čā².“A˜t“PreŽ‘Œk(µb²)“there“is“a“reader“agen˜tŽ”‘?µr‘p!²=›)µrG²(µX:©;‘ŖØY‘8ä²)–)°for“some“µY‘ačø6²=˜µX‘Čā².“If“µb“²is“a“mo•øćv“e–)°of“µr‘pͲin“µx²,“then“moGdeŽ‘Ę&(µrG²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘{†²=Ž”‘?doGorw•øća“yŽ‘g¬L(so–śthat“µr›Aœ²self{destructs“at“µb²),“and“if“µb“²is“a“mo•øćv“e–śof“µr˜²in“µW‘c²(µx²),“thenŽ”‘?moGdeŽ‘Vœv(µrG²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘š²=‘ĒwøćaitŽ‘øį(so–UUthat“µr‘œr²self{destructs“at“its“last“mo•øćv“e–UUin“µW‘c²(µx²)).Ž© L$‘NNoøćw–GŲlet“µx–[F²=“(µa;‘ŖØb²)–GŲbšGe“a“do˜orw•øća“y–GŲof“µX‘Čā².“By“D,“for“eacøćh“µY‘”*ø6²=‘[FµX‘ŗ²there“is“aŽ”‘?mo•øćv“e›’_µb²(µY‘8ä²)–,Óø2“µx˜²sucøćh˜that˜µA²(µX:©;‘ŖØY›8ä²)ŸĪ:±PreŽ‘ <ŸĪ:(āTickĖetŽ‘”±(“x±))Ž‘4X²=“µRDz(µY˜²)ŸĪ:±PreŽ‘ <ŸĪ:(“b±)Ž‘R‚².–’_Recall“that“wøće“canŽ”‘?assume–“b²,–ēdwšøće“can“implemen˜t“µb“²with“an“unsuccessful,“nonselfdestructiv˜eŽ”‘?read–UUof“µrG²(µX:©;‘ŖØY‘8ä²).ަ‘NFinally‘’*Ŗ,›€yremo•øćv“e˜all˜remaining˜monitored˜mo“v“es˜in˜µŸ’±1Ž‘|s².˜The˜result˜is˜the˜desiredŽ”‘?run–UUµŸ’±0Ž‘ŃȲof“øBŸ’±0Ž›|s²,“implemenøćting“µŸ’±1Ž˜².’ĶžøuŽ’ĶžtŽŽŸ!|µ‘?Ā7Ž‘S@Concluding‘€RemarksŽŸ|µ‘?²Corrollary–€†2“implies“the“follošøćwing“Źc‘’}'o niteness‘R§²propGert˜y“for“the“partial“runs“of“theŽ”‘?Bakšøćery–nTalgorithm:“for“eac˜h“mo˜v˜e“µt“²the“set“øfµsøjµs–šĀø6µ>“tøg–nT²is“ nite.“This“is“a“propGert˜yŽ”‘?of–c=the“Bakšøćery“Algorithm,“and“not“of“the“moGdelling“framew˜ork:“in“spite“of“ niteŽ”‘?history‘’*Ŗ,–yit“is“easy“to“concoGct“legitimate“partially“ordered“runs“of“some“algorithmŽ”‘?whicšøćh–å•violate“the“co niteness“propGert˜y‘’*Ŗ.“In“the“case“of“the“Bak˜ery“Algorithm,“theŽ”‘?co niteness–^įpropGertšøćy“implies“that“an˜y“t˜w˜o“in nitely“activ˜e“customers“ha˜v˜e“toŽ”‘?syncšøćhronize–UUin nitely“man˜y“times.ަ‘NThe–&-co niteness“propšGertøćy“is“an“example“of“a“prop˜ertøćy“of“partial“runs“thatŽ”‘?is–ˆüobfuscated“in“linear“runs“(since“for“linears“runs“it“amounøćts“to“ nite“history).Ž”‘?This–š`indicates“that“concurrenšøćt“computations“ma˜y“ha˜v˜e“signi can˜t“propGertiesŽ”‘?whicšøćh–vcannot“bGe“disco˜v˜ered“b˜y“studying“only“their“linearizations.“Concurren˜tŽ”‘?computations–UUshould“bGe“analyzed“directly‘’*Ŗ.ŽŸ!|µ‘?ĀAc• kno“wledgemen“tsŽŸ|µ‘?²W‘’*Ŗe–Ł|thank“Anšøćte“Djerek,“RobGert“Esc˜h˜bac˜h“and“Igor“Urbiha,“who“ha˜v˜e“pro˜videdŽ”‘?všøćery–UUuseful“remarks“on“a“draft“v˜ersion“of“this“papGer.ŽŽŽŒ‹’° o#f ż¬Üš 5#f żäܚ‘?ĀReferencesŽŸ‘?¾[Abr93]ŽŽ‘došUri–TAbraham.›ĪBak¾9ery“algorithms.˜Unpublished“man¾9uscript,“pp.“35,“1993.ޤ ‘?[BGR95]ŽŽ‘g¶Egon–GB‘ū`orger,“Y‘’:«uri“Gurevicš¾9h,“and“Dean“Rosenzw˜eig.‘­żThe“bak˜ery“algorithm:Ž”‘došY‘’:«et–1Ęanother“spAĒeci cation“and“v¾9eri cation.‘n’In“E.“B‘ū`orger,“editor,“ó;¼j‘¹ cmti9ęSp•‡e“ci c“ationŽ”‘došand–N cmmi10ó 0e—rcmmi7óO Ś\cmmi5óKń`y cmr10óŁ“ Rcmr7ó†›Zcmr5óś±u cmex10łßßßßßßß