Under consideration for publication in Theory and

UnderconsiderationforpublicationinTheoryandPracticeofLogicProgramming1EnhancedSharingAnalysisTechniques:AComprehensiveEvaluationROBERTOBAGNARADepartmentofMathematics,UniversityofParma,Italy(e-mail:[e-mail])ENEAZAFFANELLADepartmentofMathematics,UniversityofParma,Italy(e-mail:[e-mail])PATRICIAM.HILLySchoolofComputing,UniversityofLeeds,Leeds,U.K.(e-mail:[e-mail])AbstractSharing,anabstractdomaindevelopedbyD.JacobsandA.Langenfortheanalysisoflogicprograms,derivesusefulaliasinginformation.Itiswell-knownthatacommonlyusedcoreoftechniques,suchastheintegrationofSharingwithfreenessandlinearityinformation,cansignicantlyimprovetheprecisionoftheanalysis.However,anumberofotherproposalsforreneddomaincombinationshavebeencirculatingforyears.Onefeaturethatiscommontotheseproposalsisthattheydonotseemtohaveundergoneathoroughexperimentalevaluationevenwithrespecttotheexpectedprecisiongains.Inthispaperweexperimentallyevaluate:helpingSharingwiththedenitelygroundvariablesfoundusingPos,thedomainofpositiveBooleanformulas;theincorporationofexplicitstructuralinformation;afullimplementationofthereducedproductofSharingandPos;theissueofreorderingthebindingsinthecomputationoftheabstractmgu;anoriginalproposalfortheadditionofanewmoderecordingthesetofvariablesthataredeemedtobegroundorfree;arenedwayofusinglinearitytoimprovetheanalysis;therecoveryofhiddeninformationinthecombinationofSharingwithfreenessinformation.Finally,wediscusstheissueofwhethertrackingcompoundnessallowsthecomputationofmoresharinginformation.1IntroductionIntheexecutionofalogicprogram,twovariablesarealiasedorshareatsomepro-grampointiftheyareboundtotermsthathaveacommonvariable.Conversely,twovariablesareindependentiftheyareboundtotermsthathavenovariablesincommon.Thatis,ifitisnotpossiblefortwovariablestosharethentheyareTheworkoftherstandsecondauthorshasbeenpartlysupportedbyMURSTproject\Cer-ticazioneautomaticadiprogrammimedianteinterpretazioneastratta.yThisworkwaspartlysupportedbyEPSRCundergrantGR/M05645.2R.Bagnara,E.ZaanellaandP.M.Hilldenitelyindependentandviceversa.Inlogicprogramming,aknowledgeofthepos-siblealiasing(or,equivalently,deniteindependence)betweenvariableshassomeimportantapplications.InformationaboutvariablealiasingisessentialfortheecientexploitationofAND-parallelism(Chang,DespainandDeGroot1985,HermenegildoandGreene1990,JacobsandLangen1992,MuthukumarandHermenegildo1992).Informally,twoatomsinagoalareexecutedinparallelif,byamixtureofcompile-timeandrun-timechecks,itcanbeguaranteedthattheydonotshareanyvariable.Thisimpliestheabsenceofbindingconictsatrun-time:itwillneverhappenthattheprocessesassociatedtothetwoatomstrytobindthesamevariable.Anothersignicantapplicationisoccurs-checkreduction(Crnogorac,KellyandSndergaard1996,Sndergaard1986).Itiswell-knownthatmanyimplementedlogicprogramminglanguages(e.g.,almostallPrologsystems)omittheoccurs-checkfromtheunicationprocedure.Occurs-checkreductionamountstoidentifyingtheunicationswheresuchanomissionissafe,and,forthispurpose,informationonthepossiblealiasingofprogramvariablesiscrucial.Aliasinginformationcanalsobeusedindirectlyinthecomputationofotherinterestingprogramproperties.Forinstance,theprecisionwithwhichfreenessin-formationcanbecomputeddepends,inacriticalway,ontheprecisionwithwhichaliasingcanbetracked(Bruynooghe,CodishandMulkers1994a,Codish,Dams,FileandBruynooghe1993,File1994,KingandSoper1994,Langen1990,Muthuku-marandHermenegildo1991).Inadditiontothesewell-knownapplications,arecentlineofresearchhasshownthataliasinginformationcanbeexploitedinInductiveLogicProgramming(ILP).Inparticular,in(Blockeel,Demoen,Janssens,VandencasteeleandLaer2000),theauthorsconsiderseveraloptimizationsproposedforspeedinguptherenementofinductivelydenedpredicatesinILPsystems.Theapplicabilityoftheseopti-mizations,previouslydenedintermsofsyntacticconditionsontheconsideredpredicate,canberecastastestsonvariablealiasing.Therefore,byusingtheresultsoftheanalysistoguidetheoptimizationphase,correctnessresultsaresimplyin-heritedand,thankstothegaininprecision,therearemoreopportunitiestoapplytheproposedoptimizations.Beforecontinuing,abriefnoteonterminology:avariableiscompoundifitisboundtoanon-variableterm,itisgroundifitisboundtoatermcontainingnovariables,itisfreeifitisnotcompound,itislinearifitisboundtoatermthatdoesnotcontainmultipleoccurrencesofavariable.Sharing,adomainduetoD.JacobsandA.Langen(JacobsandLangen1989,JacobsandLangen1992,Langen1990),isbasedontheconceptofset-sharing.AnelementoftheSharingdomain,whichisasetofsharing-groups(i.e.,asetofsetsofvariables),representsinformationongroundness,groundnessdependencies,possiblealiasing,andmorecomplexsharing-dependenciesamongthevariablesthatareinvolvedintheexecutionofalogicprogram(Bagnara,HillandZaanella1997).EventhoughSharingis,inasense,remarkablyprecise,itiswell-knownthatmoreprecisionisattainablebycombiningitwithotherdomains.AsarguedinformallybyH.Sndergaard(Sndergaard1986),linearityinformationcanbesuitablyexploitedEnhancedSharingAnalysisTechniques:AComprehensiveEv