Concurrent-Software-Synthesis-Old-Challenge-–-New-Ideas并行软件合成的老–新观念的挑战资料课件

ComponentsbasedsystemswithProbabilisticchoiceDoronPeledBarIlanUniversityStructureDevelopmentofreliablesystems.Implementingcomponentsbasedsystems.Componentsbasedsystemswithprobabilisticchoices.Historyof(concurrent)softwaredevelopmentEarlysoftwaredevelopment:programming[AdaLovelance].Testingintroducedintothesoftwaredevelopmentcycle(inspection,walkthrough)[Meyer].Programverificationisinvented[Floyd,Hoare].Automaticverification(modelchecking)isinvented[Clarke+Emerson,Quelle+Sifakis].Automaticsynthesis?Whynotsynthesizethesoftwaredirectlyfromspecification?SpecificationSystemModelchecking/

testingYes!!No+

CounterexampleRevisionSpecificationSynthesisSystemAlessdirectapproachSpecificationSystemModelchecking/

testingYes!!No+

CounterexampleRevisionSpecificationSynthesisSystemCompilationIntermediatedescriptionInfact,synthesiswasattemptedquiteearlyFirstmodelcheckingpaperby[Clark+Emerson]wasalsoaboutsynthesis.Similaridea(differentformalism)by[Manna+Wolper].Translatethespecificationintoanautomaton(tableau)thatacceptsthesameexecutions.Thentranslatethisautomatonintocode.Thecodeissequential,orcontrolledbyacentralizedscheduler.R::P!4;

Q:R!x+5P::R?yR::Q?zReactivesequentialsystemssynthesisProblem[Buchi,Rabin]:Howtoautomaticallyconstructanautomatonthatinteractswithanuncontrolledenvironmentandguaranteesthattogethertheywillsatisfysomeregularproperty.[Pnueli+Rosner]:Similarfortheallowedexecutionstosatisfysometemporal(LTL)property*.Solution:Translation(LTLAutomata)+Determinization+Gametheoryconstruction.*Thisisasubproblemoftheabove,asLTLpropertiesarestar-freeregular.Complexityofsequentialsynthesisishigh2EXPTIMECompleteforLTLspecification.…But,thereareprovablesystemswherethenumberofstatesisdoublyexponential.Butmustthesizeofacircuitthatimplementssuchasystembealsodoublyexponential?[Fearnly+Peled+Schewe]:

Ifweknew,wecouldhavedecidedwhetherEXPSPACE=2EXPTIMEornot.ConcurrentsynthesisSeveralprocesses,withsomecommunicationarchitecture.WewantthesystemtosatisfysomeLTLproperty.[Pnueli+Rosner]:ItisundecidableeventocheckwhetherthereisasystemwiththegivenarchitecturethatsatisfiestheLTLproperty.Butundersomestrongassumptions(e.g.,hierarchicalsystems)wecansolvethis

[Pnueli+Rosner],[Finkbeiner+Schewe],[Thiagarajan+Madhusudan],[Kupferman+Vardi].Mostly,negativeresultsaboutsynthesisofconcurrentsystems.Fewpositiveresults:…,itisdecidableforsomeverylimitedarchitectures,mostlywhenthereisahierarchybetweentheprocesses.…inthesecases,thecomplexityisveryhigh…AlternativeAllowaformalismthatishighlevelbutalreadyincludesadistributionofthetastksamongautonomouscomponents.Providesasimpleautomaticwaytotransformthedesignintoimplementation.ComponentbasedsystemsAcomponent(process)isanautomaton.

Fromthemarkedstate,aandbareenabledlocally.dbafeC1Componentsmaysharetransitions,onwhichtheycoordinate.hcbgakjcabcmndbafeC1C2C3Verimag’sBIP(BehaviorInteractionsPriorities)arecomponentbasedsystems!BIPBIPAglobalstateisacombinationoflocalstateshdcbbagfeakjcabcmnC1C2C3Fromthegivenglobalstate,dandcareenabled.Thelocalviewofacomponentinaglobalstateisthelocalstate+enabledactions.hdcbbagfes4akjcabcmnC1C2C3ThelocalviewofC3hereis<s4,{c}>.AssumeamechanismwhereacomponentcansenseitslocalviewHowtoimplementscheduling?hdcbbagfeakjcabcmnC1C2C3C1maypickupa,whileC2maypickupb,butC3willpickupc.Notworking..Howtoimplementscheduling?hdcbbagfeakjcabcmnC1C2C3SoC1picksupb,C2picksupcandC3picksupa.Notworkingagain…WeneedsomemechanismfordecisionsMichaelRabinshowedthatasymmetricnon-probabilisticalgorithmcannotbegiven.Synchronizerslikeα–core,canbeused.Thisisinteraction-centricview.

Considerthecasethatwewanttoguaranteeselectionsbycomponents(e.g.,whenweneedtomakesomeprobabilisticchoices).Thisisacomponent-centricscheduling.SomeretrospectImplementingconcurrentsystemsfromasimplemodelofcomponentautomataisnotassimpleasthought.SimilarproblemsexistwhenimplementingmultiplechoicesynchronouscommunicationasinCSPorADA

R::[P?x[]Q?y]||P::R!3||Q::R!zInteractionbasedschedulingusing

α-coredbafeakjcabcmC1C3C1sendsOFFERtoa-interactionC2sendsOFFERtoa-interactiona-interactionsendsLOCKtoC1a-interactionsendsLOCKtoC2C1sendsOKtoa-interactionC2sendsOKtoa-interactiona-interactionsendsSTARTtoC1a-interactionsendsSTARTtoC2Moremessagesforcancellingcommunicationorfinishingit.Problemswiththeinteraction-basedschedulingExpensive:requiresquitealotofmessagepassing,andaprocessforeachcoordination.Doesnotsupportprobabilisticdecisions.Anerrorisidentifiedintheα-corealgoritmandwasfixedautomaticallyusingageneticprogrammingtoolbasedonmodelchecking[Katz+Peled].Considerthefollowingsituationa–Iwillwritealoneapapertoaconference.b–Wewillwritetogetherapapertoaconference.c–Youwillwritealoneapapertoaconference.Neitheryouormehavetimetowritetwopapers

(butwecanwriteoneeach,separately).cbbabC1C2Difficultsituation:whattodo?Wecandecideseparately,butneedtodecideconsistently:cannotbethatC1decidesonworkingseparatelyandC2decidestocollaborate.Todecideoncollaboration,weneedstocoordinate.cbbabC1C2Difficultsituation:whattodo?Perhapsweneedtothrowacoin.Saywebothhaveafaircoin.So,thechanceofcollaborationis50-50?Oneofusthrowsthecoinfaster…cbbabC1C20.50.50.50.5Howtomodelthisw.r.t.thestatespace?cbbabC1C20.50.50.50.5aabccMarkovProcess?

Agraph+adistributionfunctionfromeachstatetothesetofstatescbbabC1C20.50.50.50.5aabcc???Certainlynot…distributionmustsumsupto1!!cbbabC1C20.50.50.50.5aaccb0.50.50.5No,weusefaircoins…cbbabC1C20.50.50.50.5aaccb0.3330.3330.333OnlyifthechanceofC1andC2tothrowthecoinfirstis0.5each!cbbabC1C20.50.50.50.5aaccb0.50.250.25Amorerealisticmodel:

dependsonwhichcomponentthrowsthecoinfirst.cbbabC1C20.50.50.50.5aabcc0.50.50.50.5bC1C2C1C2Whatisthechanceofatooccur?

btooccur?ctooccur?cbbabC1C20.50.50.50.5aabcc0.50.50.50.5bC1C2C1C2Whatisthechanceofatooccur?

btooccur?ctooccur?cbbabC1C20.50.50.50.5aabcc0.50.50.50.5bC1C2C1C2Itreallydependsontheschedulingofthrowingthecoin.Ifwedonothavetheprobabilitiesforthat,wecanonlyprovidelowerandupperbound.Chanceofa(ofc)tooccurimmediatelybetween0and0.5.

Chancebtooccur0.5.cbbabC1C20.50.50.50.5aabcc0.50.50.50.5bC1C2C1C2MarkovDecisionProcessaabcc0.50.50.50.5bC1C2C1C2SetofstatesS.[Initialstates0.]ActionsA.ForeachstatesinS,A(s)isadistributionfunctiononS.

I.e.,0≤A(s)[s’]≤1and

ΣsinSA(s)[s’]=1.MarkovDecisionProcessModelingcomponentbasedsystemsaabcc0.50.50.50.5bC1C2C1C2SetofstatesS.ActionsA:inourcase,actionsarecomponentsmakingaprobabilitsticdecision.Theprobabilityofanactionmadebyacomponentonlydependsonitslocalview:

Foreachstates,s’inSwiththesamelocalviewforcomponentA,A(s)=A(s’).Adifferentscenario:

Theexecutionofcwillallowanalternativechoicefora.cbbabC1C20.50.5aaccbReflectingthechoicescbbabC1C20.50.5aacc0.50.5bC1C2C1C2Howtoimplementacomponentbasedsystem?hdcbbagfeakjcabcmnC1C2C3Howtoallowatleastonecomponenttheselection?Avoidacentralized(sequential)solution.Lockthechoicesofatleastonecomponent.ThenotionofaconflicthdcbbagfeakjcabcmnC1C2C3Transitionsofacomponentare“dependent”,whentheysharethesamecomponent,e.g.,aandb,ordandbinC1.Wesaythataandbareinconflictandthatdandbaresequential.Otherwisetheyare“independent”or“concurrent”.Thenotionofa“confusion”hdcbbagfeakjcabcmnC1C2C3Isapairoftransitionsofdifferentcomponents(a,c)suchthatexecutingcwilleitheraddorremoveaconflictingchoicetoa.Thenotionofa“confusion”hdcbbagfebcnC1C2Transitionsarein“confusion”iftheyareindependentbuttheexecutionofonecanchangethealternativechoicesfortheother.Symmetricconfusion:(a,c)

Transitionsareindependentbuttheexecutionofonecandecreasethealternativechoicesfortheother.Considernandc.Thenotionofa“confusion”hdcbbagfeakjcabcmnC1C2C3Transitionsarein“confusion”iftheyareindependentbuttheexecutionofonecanchangethealternativechoicesfortheother.Asymmetricconfusion:(n,a)Transitionsareindependentbuttheexecutionofonecanincreasethealternativechoicesfortheother.Executingnenablesbasadditionalalternativetoa.A“microscheduler”usingsemaphoresFirst,weneedtofreezethelocalviewofcomponents.

Thisincludesthelocalstateandenabledtransitions.Thenacomponentcanmakeadecisionbasedonthedistributionthatdependsonitslocalview.Whatcanmakeachangetothelocalview?

-anothercomponentmakingadifferentchoiceaboutanenabledjoinedtransition.

-duetoasymmetricconfusion,somejointtransitionsdisabled.

-duetoanasymmetricconfusion,somejointtransitionsenabled.A“microscheduler”usingsemaphoresProvidesemaphorespereachcomponent.Providesemaphorespereachconfusion.Inordertomakeadecisionaboutsomechoice,acomponentneedstocatchtherelevantsemaphores.Checklocalview.Catchthesemaphoresrelatedtocomponentsandconfusionsinvovledinview.Checkthattheviewhasnotchanged.Topreventdeadlocks,numberthesemaphoresandcatchtheminascendingorder,releaseindescendingorder[Dijkstra].A“microscheduler”usingsemaphoresOptimization:wedononeedsemaphoresforsymmetricconfusions:casewouldbeeliminatedbycapturingsemaphoreforcomponents.Couldalternativelycatchsemaphoresforthecomponentsthatsharethelocallybutnotgloballyenabledtransitions.

Thendonotneedsemaphoresforasymmetricconfusion.

Butthiswillreduceconcurrency.ForC2tomove…hdcbbagfeakjcabcmnC1C2C3cisenabeld.CatchessemaphoresonC2,onC3andontheconfusion(d,c).Why?ImplementationComponentsserveinamaster–slavemechanism.Aslaveoffersupdatesonlocallyenabledtransitionsthroughsharedvariablesandexecuteitspartinaselectedtransition.Alsosolvesalong-lastingproblemonmodelingandimplementingconcurrentsystemswithprobabilisticchoices[Katoen+Peled].Allowsparallelism.Nodeadlocks.Previoussolutionsinvolvedallowingonlyonetransitiontofireintheentiresystem.Simpletoimplement(implementedbyAyoubNouri)usingstandardsemaphoreoperations.Ifprobabilisticchoiceisnotnecessary,wecanremovesemaphoresforasymmetricconfusion.ImplementationAllowsparallelism.Transitionsarenotnecessarilysmallorsimple.Behavesasifatomic;linerarizability.Nodeadlocks.Previoussolutionsinvolvedallowingonlyonetransitiontofireintheentiresystem[Lynchetal].Simpletoimplement(implementedwithVerimag)usingstandardsemaphoreoperations.Ifprobabilisticchoiceisnotnecessary,wecanremovesemaphoresforasymmetricconfusion.SharedtransitionsEachcomponentsetsupasharedflagtoindicatewhenasharedtransitionaislocallyenabled(andresetswhenitbecomesdisabled).Tocheckitsview,acomponentneedstocheckwhichothercomponentsthatshareitslocallyenabledtransitionshavesetuptheirsharedflags.Canweeliminatetheseexpensivechecks?Howtoeliminaterepeatedchecksforenablednessofsharedtransitions?Canuseasynchronizerlikeα-core(notcheap…).Canuse«

knowledge

»toeliminatesomeofthechecks;Whatisknowledge?AcomponentX“knows”apropertypaboutthesystemifevery(global)stateofthesystemthatincludesthecurrentlocalstateofX,pholds.Jointknowledgeofcomponents:whencombiningtheirlocalstates.Morecomponentsknowtogethermore.CalculatethereachablestatesthathavethesamecurrentlocalstateofcomponentX.Thencheckwhetherthesestatessatisfyp.Canbedoneusingmodelcheckingtechniques,e.g.,basedonBDDs.Whentheleftcomponentisinlocalstates,itknowsthatthemiddlecomponentcannotbeinstatet.shdcbbagfeakjcabcmntqC1C3C2Howtouseprecalculatedknowled