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,[e-mail]manticsfortheconcurrencymonadofthepurelyfunctionallanguageOpal,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