Some Considerations on a Calculus with Weak Refere

SomeConsiderations[e-mail][e-mail]27,2005AbstractWeakreferencesarereferencesthatdonotpreventtheobjecttheypointtofrombeinggarbagecollected.Mostrealisticlanguages,includingJava,SML/NJ,andOCamltonameafew,havesomefacilityforprogrammingwithweakreferences.Weakreferencesareusedinimplementingidiomslikememoizingfunctionsandhash-consinginordertoavoidpotentialmemoryleaks.However,thesemanticsofweakreferencesinmanylanguagesarenotclearlyspecified.Withoutaformalsemanticsforweakreferencesitbecomesimpossibletoprovethecorrectnessofimplementationsmakinguseofthisfeature.PreviousworkbyHallettandKfouryextendsλgc,alanguageformodelinggarbagecollection,toλweak,asimilarlanguagewithweakreferences.Usingthispreviouslyformalizedsemanticsforweakreferences,weconsidertwoissuesrelatedtowell-behavednessofprograms.Firstly,weprovideanew,simplerproofofthewell-behavednessofthesyntacticallyrestrictedfragmentofλweakdefinedpreviously.Secondly,wegiveanaturalsemanticcri-terionforwell-behavednessmuchbroaderthanthesyntacticrestriction,whichisusefulasprincipleforprogrammingwithweakreferences.Furthermoreweextendtheresult,provedinpreviouslyofλgc,whichallowsonetousetype-inferencetocollectsomereachableobjectsthatareneverused.Weprovethatthisresultholdsofourlanguage,andweextendthisresulttoallowthecollectionofweakly-referencedreachablegarbagewithoutincurringthecomputationaloverheadsometimesassociatedwithcollectingweakbindings(e.g.theneedtorecomputeamemoizedfunction).Lastlyweuseextendthesemanticframeworktomodelthekey/valueweakreferencesfoundinHaskellandweprovetheHaskellissemanticsequivalenttoasimplersemanticsduetothelackofside-effectsinourlanguage.1IntroductionTheabilitytoconciselyspecifyandformallyprovethecorrectnessofgarbagecollectionstrategieswasanimportantcontributionofMorrisett,FelleisenandHarper’sλgc.Bymodelingtheheapasasetofmutuallyrecursivedefinitions,thesemanticsofagarbagecollectionstrategycanbespecifiedasarewriterulewhichremovesbindingsfromthemutuallyrecursivesetwithoutalteringprogrambehavior.Theadditionofweakreferenceschangesthissituationinthatprogrambehaviorcandependonhowgarbagecollectionisemployed.However,thisdoesnotnegatetheusefulnessofhavingahigh-levelformalmodelwhichspecifieshowgarbagecollectionandweakreferencesinteract.Infact,some(perhapsinformal)modeliscriticaltowritingcorrectimplementationsusingweakreferences.Aformalmodel,whichextendsλgcwiththemeanstointroduceandconditionallydereferenceweakreferences,isintroducedin[HK05].Inthislanguage,asinλgc,allvaluesareallocatedto,andstayontheheapduringevaluation(unlessgarbagecollected).Forthisreasonitmakessensetocreateaweakreferencetoanyprogramvalue.Thesemanticsgivenessentiallymatchesthesemanticsforweakreferences1inSML/NJ[SML].Becauseofcompileroptimizationslikecommonsubexpressionelimination,theactualidentityofimmutableobjectsisnotstaticallyknown,andassuchthedocumentationclaimsthesemanticsis“ambiguous.”ThesemanticsusedinthispaperisnotambiguousandifanSMLprogrammerusesthissemanticshisprogramswillbehaveasintended,andwedonotneedtoworryaboutobjectidentitybecausethesemanticsdoesnotguaranteethatanyobjectwillbegarbagecollectedatanygiventime.Thecontributionsofthispaperareseveral.Firstly,weprovideamuchsimplerandcompleteproofofthewell-behavednessofasyntacticallyrestrictedclassofprograms.Theoriginalproofwasquitecomplicatedandonlyprovedapartofthetheorem.Secondly,weprovideanaturalsemanticcriterionforwell-behavednesswhichismuchbroaderthanthesyntacticrestriction.Thiscriterionisausefulprincipleforprogrammingwithweakreferences,andweuseittoargueforthecorrectnessofanimplementationofmemoizingfunctionapplication.Thirdly,weextendtheresultfrom[MFH95]whichallowstheuseoftype-inferencetocollectsomeobjectswhicharereachablebutneverused.Theextendedresultadditionallyallowstombstoningofweakreferencestothisreachablegarbage,withoutincurringtheruntimeoverheadsometimesassociatedwithtombstoningaweakreference.Lastly,weshowtheflexibilityoftheframeworkbyextendingittoformalizeamodelofthekey/valueweakreferencesfoundinHaskell.Thepaperisorganizedasfollows.InSection2weintroducethesyntaxandsemanticsofλweak.InSection3weexplainthesyntacticrestrictionthatweimposetoassureuniquenessofprogramresult.InSection4weprovethatrestrictedprogramshaveauniqueresult.InSection5wegiveanaturalsemanticcriterionforwell-behavedness.InSection6weprovethecorrectnessofatransformationthatusestypeinferencetobothdoextragarbagecollection,andtombstoneweakreferenceswithoutrequiringtheextracomputationthatmightnormallybenecessary.InSection7weformalizethesemanticsofthekey/valueweakreferencesfoundinHaskellandproveitequivalenttoasimplersemanticsintheabsenseofside-effects.2Modelingweakreferences:λweakInthissectionwegivetheformalsyntaxandsemanticsofλweak.SyntaxofλweakThesyntaxofλweak(giveninFigure1)isthatofastandardprogramminglanguagebasedontheλ-calculusalongwithadditionalprimitivesforintroducingweakreferencesanddoingconditionalweakdereferencing.Aλweakexpressioniseitheravariable(x),aninteger(i)