On the semantics of a concurrency monad with choic

整理文档很辛苦,赏杯茶钱您下走!

免费阅读已结束,点击下载阅读编辑剩下 ...

阅读已结束,您可以下载文档离线阅读编辑

资源描述

TechnischeUniversit¨atBerlinForschungsberichtedesFachbereichsInformatikOntheSemanticsofaConcurrencyMonadwithChoiceandServicesThomasFrauensteinWolfgangGrieskampMarioSudholtReportNo.96{14RevisedVersion,July1996TechnischeUniversit¨atBerlinFachbereich13InformatikFranklinstraße28/29D-10587BerlinOntheSemanticsofaConcurrencyMonadwithChoiceandServicesThomasFrauenstein,WolfgangGrieskampandMarioSudholtTechnischeUniversitatBerlin,FachbereichInformatik,Sekr.FR5-13,Franklinstr.28/29,10587Berlin,e-mail:fthofra,wg,fishg@cs.tu-berlin.deAbstractWedeveloptwosemanticsfortheconcurrencymonadofthepurelyfunctionallanguageOpal,whichprovidesageneralmonadicchoice,value-resultagentsandguardedclient-serverbasedcommunication.Thetransitionsemanticssupportsanoperationalunderstandingoftheconcurrencymonad.Thestate-transformerseman-ticsgivesanaxiomaticdescriptionoftheconcurrencymonadbyusingavariantoftemporalintervallogicassyntacticsugarontopofLCF.Inordertocopewithtypingproblemsinbothsemantics,amodiednotionofdynamictypesisdeveloped,whichentailsasaspecialcaselocalexistentialquanticationoftypevariablesinconstructorfunctions.Note:Thisversion(revisedversion,July1996)ofTR96-14diersfromtheprintedversiondatedMay1996inthatpartsofthestate-transformersemantics(Section5)havebeenrevised.CONTENTS2Contents1Introduction32TheKernelLanguage42.1Syntax......................................42.2OperationalSemantics.............................72.3LCF-StyleDenotationalSemantics......................73TheConcurrencyMonad84TransitionSemantics104.1ExtendingtheConcurrencyMonad......................104.2TheConcurrentTransitionSemantics.....................115State-TransformerSemantics135.1TheState....................................135.2RepresentingCommands............................145.3TemporalObservations.............................145.4AxiomatizationoftheConcurrencyMonad..................166RelatedandFutureWork187Conclusion201INTRODUCTION31IntroductionMuchhasbeensaidaboutthesuitabilityoffunctionallanguagesforthedesignandimple-mentationofalgorithms:theirelegance,mathematicalclarity,transparencyandveriabil-ityhavebeenpositivelynoticed.ButfunctionallanguagesarealsoconsideredtohaveanAchille’sheel:thehandlingofinput/outputand|moregenerally|programmingwithsideeectshas(atleast)beenclumsy.Variousapproacheshavebeenstudiedovertheyearsineortstoovercomethisde-ciency,notablystream-processingfunctions,continuationsandmonads.Thiswork,inparticularthatfocusingonthemonadicapproach,hasledtosomesuccessinsequentialI/Osituations.Thetermimperativefunctionalprogramming[JW93]hasbeencoinedtonameastyleofprogrammingwherecomputationsexhibitingside-eectsarerepresentedasvaluesofamonadictype.Theyareconstructedandtransformedinapurelyfunctionalstyleandinterpretedasfunctionstransformingaglobalstate{inthecaseofanI/Omonad,the\state-of-the-world.ConcurrentextensionsoftheusualI/OmonadfoundinlanguagessuchasHaskellandOpalhaverecentlybeendesigned,implementedandsuccessfullyapplied,e.g.totheconstructionofgraphicaluserinterfaces[FGPS96,JGF96,FJ95].TheseextensionsraisethequestionofanadequatesemanticmodelofI/Omonadsinthepresenceofindetermin-isticcomputations.Whilethe\state-of-the-worldparadigmforconventionalI/OmonadshasalreadybeenthesubjectofjustiedcriticismbecauseitstreatmentoftheunpredictablebehaviourofI/Ooperationsissomewhat\magical,itsapplicationtoexplicitconcurrentprogrammingraisesevenmorequestions.InthispaperwepresenttwosemanticmodelsoftheconcurrencymonadofthepurelyfunctionalprogrammingandspecicationlanguageOpal[DFG+94].Theconcurrencymonadprovidesamonadicchoice,value-resultagentsandguardedclient-servercommuni-cation.IthasbeenimplementedintheOpalsystemandusedtorealizeacomprehensivegraphicaluserinterfacelibrary[FGPS96].Here,wedevelopanoperationaltransitionse-manticsandanaxiomaticstate-transformersemanticsfortheconcurrencymonad,thathandleindeterminismexplicitly.Thetransitionsemanticsdenesmonadicvaluesastermsofaparticularfreetypethatareconstructedinadeterministicfunctionalwayanddeconstructedinanindeterministicconcurrentway.Thistreatmentreectsthecleardistinctionbetweentheworldof-reductionandthatofconcurrentexecution.Incontrast,thestate-transformersemanticspreservestheviewofmonadsasfunctionstransformingaglobalstate:however,indeter-minismismodelledbyassociatingalooseclassofpossibleinterpretationswitheachstatetransformer.Thistreatmentisnotconstructive;itspurposeistoprovideaframeworkforalgebraic-axiomaticspecicationandreasoningaboutconcurrentmonadicprogramswhichistechnicallysupportedbyavariantofinterval-basedtemporallogicdenedassyntacticsugarontopofanLCF-likelogic.Inordertoovercomerestrictionsonthetypesystemofthesimplytypedpolymorphic-calculuswhichhinderaformulationofoursemantics,wedevelopamodiednotionofdynamictypesthatallowsustohaveunboundtypevariablesinthedomainofconstructor2THEKERNELLANGUAGE4functions.Althoughwedonotneedthefullpowerofthiskindofdynamics|weonlyusethemtomodellocalexistentialquantication|wehavepreferredthisapproachbecauseofitssimplicityandwell-foundnessduetotheworkof[ACPP8

1 / 23
下载文档,编辑使用

©2015-2020 m.777doc.com 三七文档.

备案号:鲁ICP备2024069028号-1 客服联系 QQ:2149211541

×
保存成功