ABSTRACT Automatically Proving the Correctness of Compiler Optimizations

CompilerOptimizations

SorinLerner

DepartmentofComputerScienceandEngineering

UniversityofWashington

ToddMillsteinCraigChambers

{lerns,todd,chambers}@cs.washington.edu

ABSTRACT

Wedescribeatechniqueforautomaticallyprovingcompileroptimizationssound,meaningthattheirtransformationsarealwayssemantics-preserving.Wefirstpresentadomain-specificlanguage,calledCobalt,forimplementingoptimiza-tionsasguardedrewriterules.CobaltoptimizationsoperateoveraC-likeintermediaterepresentationincludingunstruc-turedcontrolflow,pointerstolocalvariablesanddynami-callyallocatedmemory,andrecursiveprocedures.Thenwedescribeatechniqueforautomaticallyprovingthesound-nessofCobaltoptimizations.Ourtechniquerequiresanau-tomatictheoremprovertodischargeasmallsetofsimple,optimization-specificproofobligationsforeachoptimiza-tion.WehavewrittenavarietyofforwardandbackwardintraproceduraldataflowoptimizationsinCobalt,includ-ingconstantpropagationandfolding,branchfolding,fullandpartialredundancyelimination,fullandpartialdeadassignmentelimination,andsimpleformsofpoints-toanaly-sis.Weimplementedoursoundness-checkingstrategyusingtheSimplifyautomatictheoremprover,andwehaveusedthisimplementationtoautomaticallyproveouroptimiza-tionscorrect.Ourcheckerfoundmanysubtlebugsduringthecourseofdevelopingouroptimizations.Wealsoimple-mentedanexecutionengineforCobaltoptimizationsaspartoftheWhirlwindcompilerinfrastructure.

CategoriesandSubjectDescriptors

D.2.4[SoftwareEngineering]:Software/ProgramVeri-fication–correctnessproofs,reliability,validation;D.3.4[ProgrammingLanguages]:Processors–compilers,op-timization;F.3.1[LogicsandMeaningsofPrograms]:SpecifyingandVerifyingandReasoningaboutPrograms–mechanicalverification

GeneralTerms

Reliability,languages,verification.

Keywords

Compileroptimization,automatedcorrectnessproofs.

Permissiontomakedigitalorhardcopiesofallorpartofthisworkforpersonalorclassroomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributedforprofitorcommercialadvantageandthatcopiesbearthisnoticeandthefullcitationonthefirstpage.Tocopyotherwise,torepublish,topostonserversortoredistributetolists,requirespriorspecificpermissionand/orafee.

PLDI’03,June9–11,2003,SanDiego,California,USA.Copyright2003ACM1-58113-662-5/03/0006...$5.00.

1.INTRODUCTION

Compilersareanimportantpartoftheinfrastructurere-lieduponbyprogrammers.Ifacompilerisfaulty,thensoarepotentiallyallprogramscompiledwithit.Unfortu-nately,compilererrorscanbedifficultforprogrammerstodetectanddebug.First,becausethecompiler’soutputcan-notbeeasilyinspected,problemscanoftenbefoundonlybyrunningacompiledprogram.Second,thecompilermayappeartobecorrectovermanyruns,withaproblemonlymanifestingitselfwhenaparticularcompiledprogramisrunwithaparticularinput.Finally,whenaproblemdoesap-pear,itcanbedifficulttodeterminewhetheritisanerrorinthecompilerorinthesourceprogramthatwascompiled.Forthesereasons,itisveryusefultodeveloptoolsandtechniquesthatgivecompilerdevelopersandprogrammersconfidenceintheircompilers.Onewaytogainconfidenceinthecorrectnessofacompileristorunitonvariousprogramsandcheckthattheoptimizedversionofeachprogrampro-ducescorrectresultsonvariousinputs.Whilethismethodcanincreaseconfidence,itcannotprovideanyguarantees:itdoesnotguaranteetheabsenceofbugsinthecompiler,nordoesitevenguaranteethatanyoneparticularoptimizedprogramiscorrectonallinputs.Italsocanbetedioustoassembleanextensivetestsuiteofprogramsandprograminputs.

Translationvalidation[26,20]andcrediblecompila-tion[28,27]improveonthistestingapproachbyautomat-icallycheckingwhetherornottheoptimizedversionofaninputprogramissemanticallyequivalenttotheoriginalpro-gram.Thesetechniquescanthereforeguaranteethecorrect-nessofcertainoptimizedprograms,butthecompileritselfisstillnotguaranteedtobebug-free:theremayexistprogramsforwhichthecompilerproducesincorrectoutput.Thereislittlerecourseforaprogrammerifacompiledprogramcan-notbevalidated.Furthermore,theseapproachescanhaveasubstantialimpactonthetimetorunanoptimization.Thebestsolutionwouldbetoprovethecompilersound,meaningthatforanyinputprogram,thecompileralwaysproducesanequivalentoutputprogram.Optimizations,andsometimesevencompletecompilers,havebeenprovensoundbyhand[1,2,16,14,8,24,3,11].However,manuallyprov-inglargepartsofacompilersoundrequiresalotofeffortandtheoreticalskillonthepartofthecompilerwriter.Inaddition,theseproofsareusuallydoneforoptimizationsaswrittenonpaper,andbugsmaystillarisewhenthealgo-rithmsareimplementedfromthepaperspecification.

Wepresentanewtechniqueforprovingthesoundnessofcompileroptimizationsthatcombinesthebenefitsfrom

thelasttwoapproaches:ourapproachisfullyautomated,asincrediblecompilersandtranslationvalidation,butitalsoprovesoptimizationscorrectonceandforall,foranyinputprogram.Weachievethisgoalbyprovidingthecom-pilerwriterwithadomain-specificlanguageforimplement-ingoptimizationsthatisbothflexibleenoughtoexpressavarietyofoptimizationsandamenabletoautomatedcor-rectnessreasoning.

Themaincontributionsofthispaperareasfollows:•Wepresentalanguage,calledCobalt,fordefiningop-timizationsoverprogramsexpressedinaC-likeinter-mediatelanguageincludingunstructuredcontrolflow,pointerstolocalvariablesanddynamicallyallocatedmemory,andrecursiveprocedures.Toimplementanoptimization(i.e.,ananalysisplusacodetransfor-mation),usersprovidearewriterulealongwithaguarddescribingtheconditionsthatmustholdfortheruletobetriggeredatsomenodeofaninputpro-gram’scontrol-flowgraph(CFG).Theoptimizationalsoincludesasmallpredicateoverprogramstates,whichcapturesthekey“insight”behindtheoptimiza-tionthatjustifiesitscorrectness.Cobaltalsoallowsuserstoexpresspureanalyses,suchaspointeranalysis.Pureanalysescanbeusedbothtoverifypropertiesofinterestaboutaprogramandtoprovideinformationtobeconsumedbylatertransformations.OptimizationsandpureanalyseswritteninCobaltaredirectlyexe-cutablebyaspecialdataflowanalysisenginewrittenforthispurpose;theydonotneedtobereimplementedinadifferentlanguagetoberun.•WehaveusedCobalttoexpressavarietyofintrapro-ceduralforwardandbackwarddataflowoptimizations,includingconstantpropagationandfolding,copyprop-agation,commonsubexpressionelimination,branchfolding,partialredundancyelimination,partialdeadassignmentelimination,andloop-invariantcodemo-tion.WehavealsousedCobalttoexpressseveralsim-pleintraproceduralpointeranalyses,whoseresultsweexploitedintheaboveoptimizations.•WepresentastrategyforautomaticallyprovingthesoundnessofoptimizationsandanalysesexpressedinCobalt.Thestrategyrequiresanautomatictheoremprovertodischargeasmallsetofproofobligationsforeachoptimization.Wehavemanuallyproventhatiftheseobligationsholdforanyparticularoptimization,thenthatoptimizationissound.Themanualprooftakescareofthenecessaryinductionoverprogramex-ecutiontraces,whichisdifficulttoautomate.Asaresult,theautomatictheoremproverisgivenonlynon-inductivetheoremstoproveaboutindividualprogramstates.•Wehaveimplementedourcorrectnesscheckingstrat-egyusingSimplify[31,23],theautomatictheo-remproverusedintheExtendedStaticCheckerforJava[6].WehavewrittenageneralsetofaxiomsthatareusedbySimplifytoautomaticallydischargetheoptimization-specificproofobligationsgeneratedbyourstrategy.Theaxiomssimplyencodetheseman-ticsofprogramsinourintermediatelanguage.Newop-timizationprogramscanbewrittenandprovensound

withoutrequiringanymodificationstoSimplify’sax-iomset.

•Wehaveusedourcorrectnesscheckertoautomaticallyprovecorrectalloftheoptimizationsandpureanaly-seslistedabove.Thecorrectnesscheckeruncoveredanumberofsubtleproblemswithearlierversionsofouroptimizationsthatmighthaveeludedmanualtestingforalongtime.•WehaveimplementedanexecutionengineforCobaltoptimizationsaspartoftheWhirlwindcompilerinfras-tructure,andwehaveusedittosuccessfullyexecuteallofouroptimizations.Byprovidinggreaterconfidenceinthecorrectnessofcom-pileroptimizations,wehopetoprovideafoundationforex-tensiblecompilers.Anextensiblecompilerwouldallowuserstoincludenewoptimizationstailoredtotheirapplicationsordomainsofinterest.Theextensiblecompilercanprotectit-selffrombuggyuseroptimizationsbyverifyingtheircorrect-nessusingourstrategy;anybugsintheresultingextendedcompilercanbeblamedonotheraspectsofthecompiler’simplementation,notontheuser’soptimizations.Extensiblecompilerscouldalsobeagoodvehicleforresearchintonewcompileroptimizations.

ThenextsectionintroducesCobaltbyexampleandsketchesourstrategyforautomaticallyprovingsoundnessofCobaltoptimizations.Sections3and4formallydefineCobaltandourautomaticproofstrategy,respectively.Sec-tion5discussesourimplementationofCobalt’sexecutionengineandcorrectnesschecker.Section6evaluatesourwork,andsection7discussesfuturework.Section8de-scribesrelatedwork,andsection9offersourconclusions.

2.OVERVIEW

Inthissection,weinformallydescribeCobaltandourtechniqueforprovingCobaltoptimizationssoundthroughanumberofexamples.Acompaniontechnicalreport[13]containsthecompletedefinitionsofalltheoptimizationsandanalyseswehavewritteninCobalt.

2.1ForwardTransformationPatterns2.1.1Semantics

TheheartofaCobaltoptimizationisitstransformationpattern.Foraforwardoptimization,atransformationpat-ternhasthefollowingform:

ψ1followedbyψ2untils⇒s󰀁withwitnessPAtransformationpatterndescribestheconditionsunderwhichastatementsmaybetransformedtos󰀁.Theformulasψ1andψ2,whicharepropertiesofastatementsuchas“xisdefinedandyisnotused,”togetheractastheguardindicatingwhenitislegaltoperformthistransformation:scanbetransformedtos󰀁ifonallpathsintheCFGfromthestartoftheprocedurebeingoptimizedtos,thereexistsastatementsatisfyingψ1,followedbyzeroormorestatementssatisfyingψ2,followedbys.Figure1showsthisscenariopictorially.

Forwardtransformationpatternscodifyascenariocom-montomanyforwarddataflowanalyses:anenablingstate-mentestablishestheconditionsnecessaryforatransforma-tiontobeperformeddownstream,andanyinterveningstate-mentsareinnocuous,i.e.,donotinvalidatetheconditions.

paths in the CFGboundary whereψ1holds

region whereψ2holds

statement sFigure1:CFGpathsleadingtoastatementswhichcanbetransformedtos󰀁bythetransformationpatternψ1followedbyψ2untils⇒s󰀁withwitnessP.Theshadedregioncanonlybeenteredthroughastatementsatisfyingψ1,andallstatementswithintheregionsatisfyψ2.Thestatementscanonlybereachedbyfirstpassingthroughthisshadedregion.

Theformulaψ1capturesthepropertiesthatmakeastate-mentenabling,andψ2capturesthepropertiesthatmakeastatementinnocuous.ThewitnessPcapturestheconditionsestablishedbytheenablingstatementthatallowthetrans-formationtobesafelyperformed.Witnesseshavenoeffectonthesemanticsofanoptimization;theywillbediscussedmorebelowinthecontextofourstrategyforautomaticallyprovingoptimizationssound.

Example1.Asimpleformofconstantpropagationre-placesstatementsoftheformX:=YwithX:=Cifthereisanearlier(enabling)statementoftheformY:=Candeachintervening(innocuous)statementdoesnotmodifyY.TheenablingstatementensuresthatvariableYholdsthevalueC,andthisconditionisnotinvalidatedbytheinnocu-ousstatements,therebyallowingthetransformationtobesafelyperformeddownstream.Thissequenceofeventsisex-pressedbythefollowingtransformationpattern(thewitnessisdiscussedinmoredetailinsection2.1.2):stmt(Y:=C)followedby¬mayDef(Y)until

X:=Y⇒X:=Cwithwitnessη(Y)=C

The“patternvariables”XandYmaybeinstantiatedwithanyvariablesoftheprocedurebeingoptimized,whilethepat-ternvariableCmaybeinstantiatedwithconstantsintheprocedure.

2.1.2Soundness

Atransformationpatternissound,i.e.,correct,ifallthetransformationsitallowsaresemantics-preserving.Forwardtransformationpatternshaveanaturalapproachforunder-standingtheir󰀁soundness.Considerastatementstrans-formedtos.Anyexecutiontraceoftheprocedurethatcontainss󰀁willatsomepointexecuteanenablingstatement,followedbyzeroormoreinnocuousstatements,beforereach-ings󰀁.Asmentionedearlier,executingtheenablingstate-mentestablishessomeconditionsatthesubsequentstateofexecution.Theseconditionsarethenpreservedbytheinnocuousstatements.Finally,theconditionsimplythatsands󰀁havethesameeffectatthepointwheres󰀁isexecuted.Asaresult,theoriginalprogramandthetransformedpro-gramhavethesamesemantics.

Ourautomaticstrategyforprovingoptimizationssoundisbasedontheaboveintuition.Aspartofthecodeforafor-wardtransformationpattern,optimizationwritersprovideaforwardwitnessP,whichisa(possiblyfirst-order)predicateoveranexecutionstate,denotedη.Thewitnessplaystheroleoftheconditionsmentionedinthepreviousparagraphandistheintuitivereasonwhythetransformationpatterniscorrect.Ourstrategyattemptstoprovethatthewitnessisestablishedbytheenablingstatementandpreservedbytheinnocuousstatements,andthatitimpliesthatsands󰀁havethesameeffect.1Wecalltheregionofanexecutiontracebetweentheenablingstatementandthetransformedstatementthewitnessingregion.Infigure1,thepartofatracethatisinsidetheshadedareaisitswitnessingregion.Inexample1,theforwardwitnessη(Y)=CdenotesthefactthatthevalueofYinexecutionstateηisC.Ourimple-mentationprovesautomaticallythatthewitnessη(Y)=CisestablishedbythestatementY:=C,preservedbystate-mentsthatdonotmodifythecontentsofY,andimpliesthatX:=YandX:=Chavethesameeffect.Therefore,theconstantpropagationtransformationpatternisautomati-callyproventobesound.

2.1.3Labels

Eachnodeinaprocedure’sCFGislabeledwithprop-ertiesthataretrueatthatnode,suchasstmt(x:=5)ormayDef(y).Theformulasψ1andψ2inanoptimizationarebooleanexpressionsovertheselabels.

Userscandefineanewkindoflabelbygivingapredicateoverastatement,referredtointhepredicate’sbodyusingthedistinguishedvariablecurrStmt.Asatrivialexample,thestmt(S)label,whichdenotesthatthestatementatthecurrentnodeisS,canbedefinedas:

stmt(S)currStmt=S

Asanotherexample,syntacticDef(Y),whichstandsforsyntacticdefinitionofY,canbedefinedas:

syntacticDef(Y)

casecurrStmt

ofdeclX⇒X=YX:=...⇒X=Yelse⇒

false

endcase

ThelabelsyntacticDef(Y)holdsatanodeifandonlyifthecurrentstatementisadeclarationoforanassignmentto

Y.The“case”predicateisaconveniencethatprovidesaformofpatternmatching,butitiseasilydesugaredintoanordinarylogicalexpression.Similarly,patternvariablesandellipsesgetdesugaredintoordinaryquantifiedvariables.GiventhedefinitionofsyntacticDef,aconservativever-sionofthemayDeflabelfromexample1canbedefinedas:

mayDef(Y)

casecurrStmtof

∗X:=ZX:=P(Z)⇒trueelse⇒⇒true

endcase

syntacticDef(Y)

Inotherwords,astatementmaydefinevariableYifthestatementiseitherapointerstore(sinceourintermediatelanguageallowstakingtheaddressofalocalvariable),aprocedurecall(sincetheproceduremaybepassedpointersfromwhichtheaddressofYisreachable),orotherwiseasyntacticdefinitionofY.

Inadditiontodefininglabelsusingpredicates,userscanalsodefinelabelsusingtheresultsofananalysis.Section2.4showshowsuchlabelsaredefinedandhowtheycanbeusedtomakemayDeflessconservativeinthefaceofpointers.

2.2BackwardTransformationPatterns

Abackwardtransformationpatternissimilartoafor-wardone,exceptthatthedirectionoftheflowofanalysisisreversed:

ψ1precededbyψ2sinces⇒s󰀁withwitnessPThebackwardtransformationpatternabovesaysthatsmaybetransformedtos󰀁ifonallpathsintheCFGfromstotheendoftheprocedure,thereexistsastatementsatisfyingψ1,precededbyzeroormorestatementssatisfyingψ2,precededbys.Thewitnessingregionofaprogramexecutiontraceconsistsofthestatesbetweenthetransformedstatementandthestatementsatisfyingψ1;Piscalledabackwardwitness.Aswithforwardtransformationpatterns,thebackwardwitnessplaystheroleofaninvariantinthewitnessingre-gion.However,inabackwardtransformationthewitness-ingregionoccursafter,ratherthanbefore,thepointwherethetransformedstatementhasbeenexecuted.Therefore,ingeneralabackwardwitnessmustbeapredicatethatre-latestwoexecutionstatesηoldandηnew,representingcorre-spondingexecutionstatesinthewitnessingregionoftracesintheoriginalandtransformedprograms.Ourautomaticproofstrategyattemptstoprovethatthebackwardwitnessisestablishedbythetransformationandpreservedbytheinnocuousstates.Finally,weprovethataftertheenablingstatementisexecuted,thewitnessimpliesthattheoriginalandtransformedexecutionstatesbecomeidentical,imply-ingthatthetransformationissemantics-preserving.Example2.Deadassignmenteliminationmaybeimple-mentedinCobaltbythefollowingbackwardtransformationpattern:

(stmt(X:=...)∨stmt(return...))∧¬mayUse(X)precededby¬mayUse(X)since

X:=E⇒skipwithwitness

ηold/X=ηnew/X

Weexpressstatementremovalbyreplacementwithaskipstatement.2TheremovalofX:=EisenabledbyeitheralaterassignmenttoXorareturnstatement,whichsignalstheendoftheprocedure.Precedingstatementsareinnocuousiftheydon’tusethecontentsofX.

Thebackwardwitnessηold/X=ηnew/Xsaysthatηoldandηnewareequal“upto”X:correspondingstatesinthewit-nessingregionoftheoriginalandtransformedprogramsareidenticalexceptforthecontentsofvariableX.Thisinvari-antisestablishedbytheremovalofX:=EandpreservedthroughouttheregionbecauseXisnotused.Thewitnessim-pliesthataredefinitionofXorareturnstatementcausestheexecutionstatesofthetwotracestobecomeidentical.

2.3ProfitabilityHeuristics

Ifanoptimization’stransformationpatternisprovensound,thenitislegaltotransformallmatchingoccurrencesofthatpattern.Forsomeoptimizations,includingourtwoexamplesabove,alllegaltransformationsarealsoprofitable.However,inmorecomplexoptimizations,suchascodemo-tionandoptimizationsthattradeofftimeandspace,manytransformationsmaypreserveprogrambehaviorwhileonlyasmallsubsetofthemimprovethecode.Toaddressthisdistinctionbetweenlegalityandprofitability,anoptimiza-tioniswrittenintwopieces.Thetransformationpatterndefinesonlywhichtransformationsarelegal.Anoptimiza-tionseparatelydescribeswhichofthelegaltransformationsarealsoprofitableandshouldbeperformed;wecallthissecondpieceofanoptimizationitsprofitabilityheuristic.Anoptimization’sprofitabilityheuristicisexpressedviaachoosefunction,whichcanbearbitrarilycomplexandwrit-teninalanguageoftheuser’schoice.Giventheset∆ofthelegaltransformationsdeterminedbythetransformationpattern,andgiventheprocedurebeingoptimized,choosereturnsthesubsetofthetransformationsin∆thatshouldactuallybeperformed.AcompleteoptimizationinCobaltthereforehasthefollowingform,whereOpatisatransfor-mationpattern:

Opatfilteredthroughchoose

Thiswayoffactoringoptimizationsintoatransformationpatternandaprofitabilityheuristiciscriticaltoourabil-itytoproveoptimizationssoundautomatically,sinceonlyanoptimization’stransformationpatternaffectssoundness.Transformationpatternstendtobesimpleevenforcom-plicatedoptimizations,withthebulkofanoptimization’scomplexitypertainingtoprofitability.Profitabilityheuris-ticscanbewritteninanylanguage,therebyremovinganylimitationsontheirexpressiveness.Withoutprofitabilityheuristics,theextracomplexityaddedtoguardstoexpressprofitabilityinformationwouldpreventautomatedcorrect-nessreasoning.

Fortheconstantpropagationanddeadassignmentelimi-nationoptimizationsshownearlier,thechoosefunctionre-turnsallinstances:chooseall(∆,p)=∆.Thisprofitabilityheuristicisthedefaultifnoneisspecifiedexplicitly.Be-lowwegiveanexampleofanoptimizationwithanontrivialchoosefunction.

Example3.Considertheimplementationofpartialredun-dancyelimination(PRE)[15,10]inCobalt.Onewayto

performPREistofirstinsertcopiesofstatementsinwell-chosenplacesinordertoconvertpartialredundanciesintofullredundancies,andthentoeliminatethefullredundan-ciesbyrunningastandardcommonsubexpressionelimina-tion(CSE)optimizationexpressibleinCobalt.Forexample,inthefollowingcodefragment,thecomputationx:=a+battheendispartiallyredundant,sinceitisredundantonlywhenthetruelegofthebranchisexecuted:

b:=...;if(...){

a:=...;x:=a+b;}else{

...//don’tdefinea,b,orx,anddon’tusex.}

x:=a+b;

Thispartialredundancycanbeeliminatedbymakingacopyoftheassignmentx:=a+binthefalselegofthebranch.NowtheassignmentafterthebranchisfullyredundantandcanberemovedbyrunningCSEfollowedbyself-assignmentremoval(removingassignmentsoftheformx:=x).

Thecriterionthatdetermineswhenitislegaltodupli-cateastatementisrelativelysimple.MostofthecomplexityinPREinvolvesdeterminingwhichofthemanylegaldu-plicationsareprofitable,sothatpartialredundancieswillbeconvertedtofullredundanciesatminimumcost.Thefirst,“codeduplication”passofPREcanbeexpressedinCobaltasthefollowingbackwardoptimization:

stmt(X:=E)∧¬mayUse(X)precededby

unchanged(E)∧¬mayDef(X)∧¬mayUse(X)since

skip⇒X:=Ewithwitness

ηold/X=ηnew/Xfilteredthrough...

Analogoustostatementremoval,weexpressstatementinsertionasreplacementofaskipstatement.3Thelabelunchanged(E)isdefined(bytheoptimizationwriter,asde-scribedinsection2.1.3)tobetrueatastatementsifsdoesnotredefinethecontentsofanyvariablementionedinE.Thetransformationpatternforcodeduplicationallowstheinsertionif,onallpathsintheCFGfromtheskip,X:=EisprecededbystatementsthatdonotmodifyEandXanddonotuseX,whichareprecededbytheskip.Inthecodefrag-mentabove,thetransformationpatternallowsx:=a+btobeduplicatedintheelsebranch,aswellasother(unprof-itable)duplications.Thisoptimization’schoosefunctionisresponsibleforselectingthoselegalcodeinsertionsthatalsoarethelatestonesthatturnallpartialredundanciesintofullredundanciesanddonotintroduceanypartiallydeadcom-putations.Thisconditionisrathercomplicated,butitcanbeimplementedinalanguageoftheuser’schoiceandcanbeignoredwhenverifyingthesoundnessofPRE.

suchanotion,additionalmechanismswouldberequiredinordertodefinethesemanticsofalabelintroducedbyaback-wardanalysis.Sofarwehavenotencounteredaneedforbackwardanalyses.

Cobaltalsocurrentlyonlyallowstheresultsofaforwardanalysistobeusedinaforwardoptimization,orinanotherforwardanalysis.Allowingaforwardanalysistobeusedinabackwardoptimizationmayresultininterference,wherebyatransformationtriggeredbythebackwardoptimizationinvalidatestheresultsoftheforwardanalysis.Thisissueisdiscussedinmoredetailinsection4.1.

3.COBALT

ThissectionprovidesaformaldefinitionofCobaltandoftheintermediatelanguagethatCobaltoptimizationsmanip-ulate.Thefullformaldetailscanbefoundinourtechnicalreport[13].

3.1IntermediateLanguage

Aprogramπinour(untyped)intermediatelanguageisdescribedbythefollowinggrammar:Progsπ::=pr...pr

Procspr::=p(x){s;...;s;}

Stmtss::=declx|skip|lhs:=e|x:=new|x:=p(b)|ifbgotoιelseι|returnx

Exprse::=b|∗x|&x|opb...bLocatableslhs::=x|∗xBaseExprsb::=x|c

Opsop::=variousoperatorswitharity≥1Vars

x::=x|y|z|...ProcNamesp::=p|q|r|...Constsc::=constantsIndices

ι

::=

0|1|2|...

Aprogramπisasequenceofprocedures,andeachprocedureisasequenceofstatements.Weassumeadistinguishedpro-cedurenamedmain.Statementsincludelocalvariabledec-larations,assignmentstolocalvariablesandthroughpoint-ers,heapmemoryallocation,procedurecallsandreturns,andconditionalbranches(unconditionalbranchescanbesimulatedwithconditionalbranches).Weassumethatnoproceduredeclaresthesamelocalvariablemorethanonce.Weassumethateachprocedureendswithareturnstate-ment.Statementsareindexedconsecutivelyfrom0,andstmtAt(π,ι)returnsthestatementwithindexιinπ.Ex-pressionsincludeconstants,localvariablereferences,pointerdereferences,takingtheaddressesoflocalvariables,andn-aryoperatorsovernon-pointervalues.

Astateofexecutionofaprogramisatupleη=(ι,ρ,σ,ξ,M).Theindexιindicateswhichstatementisabouttobeexecuted.Theenvironmentρisamapfromvariablesinscopetotheirlocationsinmemory,andthestoreσdescribesthecontentsofmemorybymappinglocationstovalues(constantsandlocations).Thedynamiccallchainisrepresentedbyastackξ,andMisthememoryallocator,whichreturnsfreshlocationsasneeded.

Thestatesofaprogramπtransitionaccordingtothestatetransition󰀁function→π.Wedenotebyη→πη󰀁thefactthatηistheprogramstatethatis“steppedto”whenexecutionproceedsfromstateη.Thedefinitionof→πisstandardandisgiveninouraccompanyingtechnicalreport[13].Wealsodefineanintraproceduralstatetransitionfunction󰀦→π.

Thisfunctionactslike→πexceptwhenthestatementtobeexecutedisaprocedurecall.Inthatcase,󰀦→πsteps“over”thecall,returningtheprogramstatethatwilleventuallybereachedwhencontrolreturnstothecallingprocedure.

Wemodelrun-timeerrorsthroughtheabsenceofstatetransitions:ifinsomestateηprogramexecutionwouldfailwitharun-timeerror,therewon’tbeanyη󰀁suchthatη→πη󰀁istrue.Likewise,ifaprocedurecalldoesnotreturnsuccessfully,󰀁e.g.,becauseofinfiniterecursion,therewon’tbeanyηsuchthatη󰀦→πη󰀁istrue.

3.2Cobalt

Inthissection,wefirstspecifythesyntaxofarewriterule’soriginalandtransformedstatementssands󰀁.Thenwedefinethesyntaxusedforexpressingψ1andψ2.Finally,weprovidethesemanticsofoptimizations.ThewitnessPdoesnotaffectthe(dynamic)semanticsofoptimizations.

3.2.1Syntaxofsands󰀁

Statementssands󰀁aredefinedinthesyntaxoftheex-tendedintermediatelanguage,whichaugmentstheinterme-diatelanguagewithaformoffreevariablescalledpatternvariables.Eachproductioninthegrammaroftheoriginalintermediatelanguageisextendedwithacaseforapatternvariable.Afewexamplesareshownbelow:

Exprse::=···|E

Varsx::=···|X|Y|Z|...Consts

c::=

···|C

Statementsintheextendedintermediatelanguageareinstantiatedbysubstitutingforeachpatternvariableaprogramfragmentoftheappropriatekindfromtheintermediate-languageprogrambeingoptimized.Forex-ample,thestatementX:=Eintheextendedintermedi-atelanguagecontainstwopatternvariablesXandE,andthisstatementcanbeinstantiatedtoformanintermediate-languagestatementassigninganyexpressionoccurringintheintermediateprogramtoanyvariableoccurringintheintermediateprogram.

3.2.2SyntaxandSemanticsofψ1andψ2

Thesyntaxforψ,andalsoforlabeldefinitions,isde-scribedbythefollowinggrammar:ψ

::=

true|false|¬ψ|ψ∨ψ|ψ∧ψ|l(t,...,t)|t=t|

casetoft⇒ψ···t⇒ψelse⇒ψendcase

Intheabovegrammar,lrangesoverlabelnamesandtrangesoverterms,whichareelementsdrawnfromtheex-tendedintermediatelanguageaswellasthedistinguishedtermcurrStmt.Thegrammarconsistsofpropositionallogicaugmentedwithlabelpredicates,termequality,andthecasepredicate.

ThesemanticsofaformulaψisdefinedwithrespecttoalabeledCFG.EachnodenintheCFGforprocedurepislabeledwithafinitesetLp(ι),whereιisn’sindex.Lp(ι)includeslabelsl(t1,...,tn)wherethetermsdonotcontainpatternvariables.Forexample,anodecouldbelabeledwithstmt(x:=3)andmayDef(x).

Themeaningofaformulaψatanodedependsonasubsti-tutionθmappingthepatternvariablesinψtofragmentsofp.Weextendsubstitutionstoformulasandprogramfrag-mentscontainingpatternvariablesintheusualway.We

writeι|=pθψtoindicatethatthenodewithindexιsatis-fiesψinthelabeledCFGofpundersubstitutionθ.Thedefinitionofι|=pbeingι|=p

θψisstraightforward,withthebasecaseθl(t1,...,tn)⇐⇒θ(l(t1,...,tn))∈Lp(ι).Thecompletedefinitionof|=pθisinourtechnicalreport[13].

3.2.3SemanticsofOptimizations

Wedefinethesemanticsofoptimizationsandanalysesinseveralpieces.First,themeaningofaforwardguardψ1fol-lowedbyψ2isafunctionthattakesaprocedureandreturnsasetofmatchingindiceswiththeircorrespondingsubstitu-tions:

Definition1.ThemeaningofaforwardguardOguardoftheformψ1followedbyψ2isasfollows:

Oguard(p)={(ι,θ)|

forallpathsι1,...,ιj,ιinp’sCFG

suchthatι1istheindexofp’sentrynode∃k.(1≤k≤j∧ιk|=pθψ1∧∀i.(kTheabovedefinitionformalizesthedescriptionofforwardguardsfromSection2.Themeaningofabackwardguardψ1precededbyψ2isidentical,exceptthattheguardisevaluatedonCFGpathsι,ιj,...,ι1thatstart,ratherthanend,atι,whereι1istheindexoftheprocedure’sexitnode.Guardscanbeseenasarestrictedformoftemporallogicformula,expressibleinvariantsofbothLinearTemporalLogic(LTL)[7]andComputationTreeLogic(CTL)[5].Nextwedefinethesemanticsoftransformationpat-terns.Aforward(backward)transformationpatternOpat=Oguarduntil(since)s⇒s󰀁withwitnessPsimplyfiltersthesetofnodesmatchingitsguardtoincludeonlythosenodesoftheforms:

Opat(p)={(ι,θ)|(ι,θ)∈Oguard(p)andι|=pθstmt(s)}

Themeaningofanoptimizationisafunctionthattakesaprocedurepandreturnstheprocedureproducedbyapplyingtopalltransformationsselectedbythechoosefunction.Definition2.GivenanoptimizationOoftheformOpatfilteredthroughchoose,whereOpathasrewriterules⇒s󰀁,themeaningofOisasfollows:

O(p)=let∆:=Opat(p)in

app(s󰀁,p,choose(∆,p)∩∆)

whereapp(s󰀁,p,∆󰀁)returnstheprocedureidenticaltopbutwiththenodewithindexιtransformedtoθ(s󰀁),foreach(ι,θ)in∆󰀁.4

Finally,themeaningofapureanalysisOguardde-fineslabelwithwitnessPappliedtoaprocedurepisanewversionofp’sCFGwhereforeachpair(ι,θ)inOguard(p),thenodewithindexιisadditionallylabeledwithθ(label).

4.PROVINGSOUNDNESSAUTOMATICALLY

InthissectionwedescribeourtechniqueforautomaticallyprovingsoundnessofCobaltoptimizations.Thefulldetails,includingtheproofsofthetheorems,areinourtechnicalreport[13].

Wesaythatanintermediate-languageprogramπ󰀁isasemanticallyequivalenttransformationofπif,whenevermain(v1)returnsv2inπ,forsomevaluesv1andv2,thenit

5

Theexampleillustratesapotentialunsoundnessfromcombiningfor-wardandbackwardtransformationpatterns.Thisisthereasonthatwecurrentlydisallowemployingaforwardpureanalysisinabackwardtransformation.Wecan,however,provethataforwardtransforma-tionpatterncannotinterferewithanyforwardpureanalysis.

4.2ForwardTransformationPatterns

Consideraforwardtransformationpatternofthefollow-ingform:

ψ1followedbyψ2untils⇒s󰀁withwitnessPAsdiscussedinsection2,ourproofstrategyentailsshowingthattheforwardwitnessPholdsthroughoutthewitness-ingregionandthatthewitnessimpliessands󰀁havethesamesemantics.Thiscannaturallybeshownbyinductionoverthestatesinthewitnessingregionofanexecutiontraceleadingtoatransformedstatement.Ingeneral,itisdifficultforanautomatictheoremprovertodeterminewhenproofbyinductionisnecessaryandtoperformsuchaproofwithastrongenoughinductivehypothesis.Thereforeweinsteadrequireanautomatictheoremprovertodischargeonlynon-inductiveobligations,whichpertaintoindividualexecutionstatesratherthanentireexecutiontraces.Wehaveproventhatiftheseobligationsholdforanyparticularoptimization,thenthatoptimizationissound.Weuseindexasanaccessoronstates:index((ι,ρ,σ,ξ,M))=ι.Theoptimization-specificobligations,tobedischargedbyanautomatictheoremprover,areasfollows,whereθ(P)isthepredicateformedbyapplyingθtoeachpatternvariableinthedefinitionofP:

F1.Ifη󰀦→πη󰀁andindex(η)|=pθψ1,thenθ(P)(η󰀁

).

F2.Ifθ(P)(η)andη󰀦→πη󰀁andindex(η)|=pθ(P)(η󰀁

θψ2,then).F3.Ifθ(P)(η)andη󰀦→πη󰀁andι=index(η)and

stmtAt(π,ι)=θ(s)andstmtAt(π󰀁,ι)=θ(s󰀁),thenη󰀦→π󰀁η󰀁.ConditionF1ensuresthatthewitnessholdsatanystatefollowingtheexecutionofanenablingstatement(onesat-isfyingψ1).ConditionF2ensuresthatthewitnessispre-servedbyanyinnocuousstatement(onesatisfyingψ2).Fi-nally,conditionF3ensuresthatsands󰀁havethesamese-manticswhenexecutedfromastatesatisfyingthewitness.Asanexample,considerconditionF1fortheconstantpropagationoptimizationfromexample1.Theconditionlooksasfollows:Ifη󰀦→πη󰀁andindex(η)|=pthenθ(η󰀁

Y)=C).Theconditioniseasilyθstmt(Y:=C),(provenauto-maticallyfromthesemanticsofassignmentsandthestmtlabel.

Thefollowingtheoremvalidatestheoptimization-specificproofobligations.

Theorem1.IfOisaforwardoptimizationsatisfyingcon-ditionsF1,F2,andF3,thenOissound.

TheproofofthistheoremusesconditionsF1andF2aspartofthebasecaseandtheinductivecase,respectively,inaninductiveargumentthatthewitnessholdsthroughoutawitnessing󰀁region.ConditionF3isthenusedtoshowthatsandshavethesamesemanticsinthiscontext.

Apureanalysisψ1followedbyψ2defineslabelwithwitnessPisprovensoundsimilarly.WerequireconditionsF1andF2tobesatisfied;F3hasnoanalogue.Thesecon-ditionsallowustoshowthatlabelindeedhasthesemanticsofthewitnessP.

4.3BackwardTransformationPatterns

Considerabackwardtransformationpatternofthefol-lowingform:

ψ1precededbyψ2sinces⇒s󰀁withwitnessPTheoptimization-specificobligationsaresimilartothosefor

aforwardtransformationpattern,exceptthattheorderingofeventsinthewitnessingregionisreversed:

B1.Ifη󰀦→πηoldandη󰀦→π󰀁)=θ(s)andstmtAtηnewandι=index(η)and

stmtAt(π,ι(π󰀁,ι)=θ(s󰀁),thenθ(P)(ηold,ηnew).B2.Ifθ(P)(ηold,ηnew)and

ηold󰀦→πη󰀁

oldandιold=index(ηold)andιnew=index(ηnew)andιold|=πθψ2

andstmtAt(π,stmtAt(π󰀁

,ιnew),thenexistssomeη󰀁

ιold)=

newthatηnew󰀦→π󰀁θ(P)(η󰀁η󰀁

there

new

andold,η󰀁

such

new).

B3.Ifθ(P)(ηold,ηnew)andηold󰀦→πηandιold=

index(ηold)andιnew=index(ηnew)andιold|=πθψ1

andstmtAt(π,ιold)=stmtAt(π󰀁

,ιnew),thenηnew󰀦→π󰀁η.ConditionB1ensuresthatthebackwardwitnessholdsbe-tweentheoriginalandtransformed6programs,aftersands󰀁arerespectivelyexecuted.ConditionB2ensuresthatthebackwardwitnessispreservedthroughtheinnocuousstate-ments.ConditionB3ensuresthatthetwotracesbecomeidenticalagainafterexecutingtheenablingstatement(andexitingthewitnessingregion).

Analogoustotheforwardcase,thefollowingtheoremval-idatestheoptimization-specificproofobligationsforback-wardoptimizations.

Theorem2.IfOisabackwardoptimizationsatisfyingconditionsB1,B2,andB3,thenOissound.

5.IMPLEMENTINGCOBALT

WehaveimplementedatoolthatautomaticallychecksthecorrectnessofCobaltoptimizationsaswellasanexe-cutionengineforrunningthem.Section5.1describesourcorrectnesschecker,andsection5.2describesourexecutionengine.

5.1CorrectnessChecker

Wehaveimplementedourstrategyforautomaticallyprov-ingCobaltoptimizationssoundwiththeSimplifyauto-matictheoremprover.Foreachoptimization,weaskSim-plifytoprovethethreeassociatedoptimization-specificobligationsgivenasetofbackgroundaxioms.Therearetwokindsofbackgroundaxioms:optimization-independentonesandoptimization-dependentones.Theoptimization-independentaxiomssimplyencodethesemanticsofourin-termediatelanguageandtheyneednotbemodifiedinor-dertoprovenewoptimizationssound.Theoptimization-dependentaxiomsencodethesemanticsofuser-definedla-belsandaregeneratedautomaticallyfromtheCobaltlabel

definitions.Ourcorrectnesscheckertranslateslabeldefi-nitionsintoSimplifyaxiomsbyexpandingcaseexpressionsintoordinarybooleanexpressionsandperformingafewsim-pletransformationstoproduceaxiomsinaformacceptedbySimplify.

ToencodetheCobaltintermediatelanguageinSimplify,weintroducefunctionsymbolsthatrepresenttermconstruc-torsforeachkindofexpressionandstatement.Forexample,thetermassgn(var(x),deref(var(y))representsthestate-mentx:=∗y.Nextweformalizetherepresentationofpro-gramstates.Simplifyhasbuilt-inaxiomsaboutamapdatastructure,withassociatedfunctionsselectandupdatetoac-cesselementsand(functionally)updatethemap.Thisisusefulforrepresentingmanycomponentsofastate.Forex-ample,anenvironmentisamapfromvariablestolocations,andastoreisamapfromlocationstovalues.

Givenourrepresentationforstates,wedefineaxiomsforafunctionsymbolevalExpr,whichevaluatesanexpressioninagivenstate.TheevalExprfunctionrepresentsthefunc-tionη(·)usedinsection2.WealsodefineaxiomsforafunctionevalLExprwhichcomputesthelocationofalhsex-pressiongivenaprogramstate.ThenweprovideaxiomsforthestepIndex,stepEnv,stepStore,stepStack,andstepMemfunctions,whichtogetherdefinethestatetransitionfunc-tion→πfromsection3.1.Thesefunctionstakeastateandaprogramandreturnthenewvalueofthestatecomponentbeing“stepped.”Asanexample,theaxiomsforsteppinganindexandastorethroughanassignmentlhs:=eareasfollows:

∀η,π,lhs,e.

stmtAt(π,index(η))=assgn(lhs,e)⇒stepIndex(η,π)=index(η)+1

∀η,π,lhs,e.

stmtAt(π,index(η))=assgn(lhs,e)⇒

stepStore(η,π)=update(store(η),evalLExpr(η,lhs),

evalExpr(η,e))Thefirstaxiomsaysthatthenewindexisthecurrentindexincrementedbyone.Thesecondaxiomsaysthatthenewstoreisthesameastheoldone,butwiththelocationoflhsupdatedtothevalueofe.

Finally,the󰀦→πfunctionisdefinedintermsofthe→πfunction.Inthecontextofintraproceduralanalysis,wedonothaveaccesstothebodiesofcalledprocedures.There-fore,weconservativelymodelthesemanticsofsteppingoveraprocedurecallbyasetofaxiomsthatholdforanycall.Theprimaryaxiomsaysthatthestoreafteracallpreservesthevaluesoflocalvariablesinthecallerwhoselocationsarenotpointedtobeforethecall.Thisaxiomencodesthefactthatlocalsnotreachablefromthestorecannotbemodifiedbyacall.

WehaveimplementedandautomaticallyprovensoundadozenCobaltoptimizationsandanalyses(whicharegiveninourtechnicalreport[13]).Onamodernworkstation,thetimetakenbySimplifytodischargetheoptimization-specificobligationsfortheseoptimizationsrangesfrom3to104seconds,withanaverageof28seconds.

5.2ExecutionEngine

TorunCobaltoptimizationswithoutfirstrewritingtheminsomeotherlanguage,wehaveimplementedanexecutionengineforCobaltasananalysisintheWhirlwindcompiler,asuccessortoVortex[4].

Thisanalysisstoresateachprogrampointasetofsub-stitutions,witheachsubstitutionrepresentingapotentialwitnessingregion.Consideraforwardoptimization:

ψ1followedbyψ2untils⇒s󰀁

withwitnessPfilteredthroughchoose

Theflowfunctionforouranalysisworksasfollows.First,ifthestatementbeingprocessedsatisfiesψ1,thentheflowfunctionaddstotheoutgoingdataflowfactthesubstitutionthatcausedψ1tobetrue.Also,foreachsubstitutionθintheincomingdataflowfact,theflowfunctionchecksifθ(ψ2)istrueatthecurrentstatement.Ifitis,thenθispropagatedtotheoutgoingdataflowfact,andotherwiseitisdropped.Finally,mergenodessimplytaketheintersec-tionoftheincomingdataflowfacts.Aftertheanalysishasreachedafixedpoint,ifastatementhasasubstitutionθinitsincomingdataflowfactthatmakesθ(stmt(s))trueandthechoosefunctionselectsthisstatement,thenthestate-mentistransformedtoθ(s󰀁).

Forexample,inconstantpropagationwehaveψ1=stmt(Y:=C)andψ2=¬mayDef(Y).Belowweshowthedataflowfactspropagatedafterafewexamplestatements:

S1:a:=2;[Y→a,C→2]S2:b:=3;[Y→a,C→2],[Y→b,C→3]

S3:c:=a;

S1satisfiesψ1,soitsoutgoingdataflowfactcontainsthesub-stitution[Y→a,C→2].S2satisfiesψ2underthissubsti-tution,sothesubstitutionispropagated;S2alsosatisfiesψ1

so[Y→b,C→3]isaddedtotheoutgoingdataflowfact.Infact,thedataflowinformationafterS2isverysimilartotheregularconstantpropagationdataflowfact{a→2,b→3}.Atfixedpoint,thestatementc:=acanbetransformedtoc:=2becausetheincomingdataflowfactcontainsthemap[Y→a,C→2].Notethatthisimplementationevaluatesall“instances”oftheconstantpropagationtransformationpatternsimultaneously.

OuranalysisisimplementedusingourearlierframeworkforcomposableoptimizationsinWhirlwind[12].Thisframe-workallowsoptimizationstobedefinedmodularlyandthenautomaticallycombinesall-forwardorall-backwardopti-mizationsinordertogainmutuallybeneficialinteractions.AnalysesandoptimizationswritteninCobaltarethere-forealsocomposableinthisway.Furthermore,Whirlwind’sframeworkautomaticallycomposesanoptimizationwithit-self,allowingarecursivelydefinedoptimizationtobesolvedinanoptimistic,iterativemanner;thispropertyislikewiseconferredonCobaltoptimizations.Forexample,arecursiveversionofdead-assignmenteliminationallowsX:=EtoberemovedevenifXisusedbeforebeingredefined,aslongasitisonly7

usedbyotherdeadassignments(possiblyincludingitself).6.DISCUSSION

Inthissection,weevaluateoursystemalongthreedi-mensions:expressivenessofCobalt,debuggingvalue,andreducedtrustedcomputingbase.

Expressiveness.Oneofthekeychoicesinourapproachistorestrictthelanguageinwhichoptimizationscanbe

written,inordertogainautomaticreasoningaboutsound-ness.However,Cobalt’srestrictionsarenotasonerousastheymayfirstappear.First,muchofthecomplexityofanoptimizationcanbefactoredintotheprofitabilityheuristic,whichisunrestricted.Second,thepatternofawitnessingregion—beginningwithasingleenablingstatementandpassingthroughzeroormoreinnocuousstatementsbeforereachingthestatementtobetransformed—iscommontomanyforwardintraproceduraldataflowanalyses,andsimi-larlyforbackwardintraproceduraldataflowanalyses.Third,optimizationsthattraditionallyareexpressedashavingef-fectsatmultiplepointsintheprogram,suchasvarioussortsofcodemotion,caninfactbedecomposedintoseveralsim-plertransformations,eachofwhichfitsCobalt’stransforma-tionpatternsyntax.

ThePREexampleinsection2.3illustratesallthreeofthesepoints.PREisacomplexcode-motionoptimiza-tion[15,10],andyetitcanbeexpressedinCobaltusingsimpleforwardandbackwardpasseswithappropriateprof-itabilityheuristics.Ourwayoffactoringcomplicatedopti-mizationsintosmallerpieces,andseparatingthepartthataffectssoundnessfromthepartthatdoesn’t,allowsuserstowriteoptimizationsthatareintricateandexpressiveyetstillamenabletoautomatedcorrectnessreasoning.

Evenso,thecurrentversionofCobaltdoeshavelimita-tions.Forexample,itcannotexpressinterproceduralop-timizationsorone-to-manytransformations.Asmentionedinsection7,ourfutureworkwilladdresstheselimitations.Also,optimizationsandanalysesthatbuildcomplexdatastructurestorepresenttheirdataflowfactsmaybedifficulttoexpress.Finally,itispossibleforlimitationsineitherourproofstrategyorintheautomatictheoremprovertocauseasoundoptimizationexpressibleinCobalttoberejected.Inallthesecases,optimizationscanbewrittenoutsideofourframework,perhapsverifiedusingtranslationvalida-tion.OptimizationswritteninCobaltandprovencorrectcanpeacefullyco-existwithoptimizationswritten“thenor-malway.”

Debuggingbenefit.Writingcorrectoptimizationsisdifficultbecausetherearemanycornercasestoconsider,anditiseasytomissone.Oursysteminfactfoundsev-eralsubtleproblemsinpreviousversionsofouroptimiza-tions.Forexample,wehaveimplementedaformofcom-monsubexpressionelimination(CSE)thateliminatesnotonlyredundantarithmeticexpressions,butalsoredundantloads.Inparticular,thisoptimizationtriestoeliminateacomputationof∗Xiftheresultisalreadyavailablefromapreviousload.Ourinitialversionoftheoptimizationpre-cludedpointerstoresfromthewitnessingregion,toensurethatthevalueof∗Xwasnotmodified.However,afailedsoundnessproofmadeusrealizethatevenadirectassign-mentY:=...canchangethevalueof∗X,becauseXcouldpointtoY.Onceweincorporatedpointerinformationtomakesurethatdirectassignmentsinthewitnessingregionwerenotchangingthevalueof∗X,ourimplementationwasabletoautomaticallyprovetheoptimizationsound.With-outthestaticcheckstofindthebug,itcouldhavegoneundetectedforalongtime,becausethatparticularcornercasemaynotoccurinmanyprograms.

Reducedtrustedcomputingbase.Thetrustedcom-putingbase(TCB)ordinarilyincludestheentirecompiler.Inoursystemwehavemovedthecompiler’soptimizationphase,oneofthemostintricateanderror-proneportions,

outsideoftheTCB.Instead,wehaveshiftedthetrustinthisphasetothreecomponents:thecorrectnesschecker,in-cludingtheautomatictheoremprover,themanualproofsdoneaspartofourframework,andtheenginethatexe-cutesoptimizations.Becauseallofthesecomponentsareoptimization-independent,newoptimizationscanbeincor-poratedintothecompilerwithoutenlargingtheTCB.Fur-thermore,asdiscussedinsection5,theexecutionengineisimplementedasasingledataflowanalysiscommontoalluser-definedoptimizations.Thismeansthatthetrustwor-thinessoftheexecutionengineisakintothetrustworthinessofasingleoptimizationpassinatraditionalcompiler.

Trustcanbefurtherenhancedinseveralways.First,wecoulduseanautomatictheoremproverthatgeneratesproofs,suchastheproverintheTouchstonecompiler[22].Thiswouldallowtrusttobeshiftedfromthetheoremprovertoasimplerproofchecker.Themanualproofsofourframe-workaremadepublicforpeerreviewin[13]toincreaseconfidence.WecouldalsouseaninteractivetheoremproversuchasPVS[25]tovalidatetheseproofs.

7.FUTUREWORK

Therearemanydirectionsforfuturework.Weplantoex-tendCobalttohandleinterproceduraloptimizations.Oneapproachwouldextendthescopeofanalysisfromasingleproceduretothewholeprogram’scontrol-flowsupergraph.AtechnicalchallengeforthisapproachistheneedtoexpressthewitnessPinawaythatisrobustacrossprocedurecalls.Forexample,thepredicateη(Y)=Cdoesnotmakesenseonceacallissteppedinto,becauseYhasgoneoutofscope.Weintendtoextendthesyntaxforthewitnesstobemorepreciseaboutwhichlocationisbeingtalkedabout.Adif-ferentapproachtointerproceduralanalysiswouldusepureanalysestodefinesummariesofprocedures,whichcouldbeusedinintraproceduraloptimizationsofcallers.

CurrentlyCobaltonlysupportstransformationsthatre-placeasinglestatementwithasinglestatement.Itshouldberelativelystraightforwardtogeneralizetheframeworktohandleone-to-manystatementtransformations,allowingop-timizationslikeinliningtobeexpressed.Supportingmany-to-manystatementtransformations,includingvariouskindsoflooprestructuringoptimizations,wouldalsobeinterest-ing.

Weplantotryinferringthewitnesses,whicharecurrentlyprovidedbytheuser.Itmaybepossibletousesomesimpleheuristicstoguessawitnessfromthegiventransformationpattern.Asasimpleexample,intheconstantpropagationexampleofsection2,theappropriatewitness,thatYhasthevalueC,issimplythestrongestpostconditionoftheenablingstatementY:=C.Manyoftheotherforwardoptimizationsthatwehavewrittenalsohavethisproperty.Ourcurrentnotionofasemanticallyequivalenttransfor-mationreasonsonlyaboutcomputationsintheoriginalpro-gramthatterminatewithoutanerror.Itwouldbestraight-forwardtoreasonaboutcomputationsthatendinarun-timeerrorbyextendingthe→πfunctiontosteptoanexpliciter-rorstateinthesesituations.Wewouldalsoliketoextendthenotionofsemanticequivalencetoallowreasoningaboutnonterminatingcomputations.

Weplantoexploremoreefficientimplementationtech-niquesfortheCobaltexecutionengine,suchasgeneratingspecializedcodetoruneachoptimization[32].Anotherdi-rectionforimprovingefficiencywouldbetoallowanalyses

tobedefinedoverasparserepresentationsuchasadataflowgraph.

Finally,animportantconsiderationthatwehavenotad-dressedistheinterfacebetweentheoptimizationwriterandourautomaticcorrectnesschecker.Itwillbecriticaltopro-videusefulerrormessageswhenanoptimizationcannotbeprovensound.WhenSimplifycannotproveagivenpropo-sition,itreturnsacounterexamplecontext,whichisastateoftheworldthatviolatestheproposition.Aninterestingapproachwouldbetousethiscounterexamplecontexttosynthesizeasmallintermediate-languageprogramthatil-lustratesapotentialunsoundnessofthegivenoptimization.

8.RELATEDWORK

Temporallogichaspreviouslybeenusedtoexpressdataflowanalysesandreasonaboutthembyhand[32,33,29,30,11].OurlanguageisinspiredbyrecentworkinthisdirectionbyLaceyetal.[11].LaceydescribesalanguageforwritingoptimizationsasguardedrewriterulesevaluatedoveralabeledCFG,andourtransformationpatternsaremodeledonthislanguage.Lacey’sintermediatelanguagelacksseveralconstructsfoundinrealisticlanguages,includ-ingpointers,dynamicmemoryallocation,andprocedures.Laceydescribesageneralstrategy,basedonrelatingexe-cutiontracesoftheoriginalandtransformedprograms,formanuallyprovingthesoundnessofoptimizationsinhislan-guage.Threeexampleoptimizationsareshownandprovensoundbyhandusingthisstrategy.Unfortunately,thegen-eralityofthisstrategymakesitdifficulttoautomate.

Lacey’sguardsmaybearbitraryCTLformulas,whileourguardlanguagecanbeviewedasastrictsubsetofCTLthatcodifiesaparticularlycommonidiom.However,wearestillabletoexpressmorepreciseversionsofLacey’sthreeex-ampleoptimizations(aswellasmanyothers)andtoprovethemsoundautomatically.Further,Lacey’soptimizationlanguagehasnonotionoflabelsdefinedbypureanalysesnorofprofitabilityheuristics.Therefore,expressingoptimiza-tionsthatemploypointerinformation(assumingLacey’slanguagewereaugmentedwithpointers)oroptimizationslikePREwouldinsteadrequirewritingmorecomplicatedguards,andsomeoptimizationswesupportmaynotbeex-pressiblebyLacey.

Asmentionedintheintroduction,muchotherworkhasbeendoneonmanuallyprovingoptimizationscorrect[14,16,1,2,8,24,3].Transformationshavealsobeenprovencorrectmechanically,butnotautomatically:thetransfor-mationisprovensoundusinganinteractivetheoremprover,whichrequiresuserinvolvement.Forexample,Young[35]hasprovenacodegeneratorcorrectusingtheBoyer-Mooretheoremproverenhancedwithaninteractiveinterface[9].Insteadofprovingthatthecompilerisalwayscorrect,translationvalidation[26,20]andcrediblecompilation[28,27]bothattacktheproblemofcheckingthecorrectnessofagivencompilationrun.Therefore,abuginanoptimiza-tiononlyappearswhenthecompilerisrunonaprogramthattriggersthebug.Ourworkallowsoptimizationstobeprovencorrectbeforethecompilerisevenrunonce.How-ever,todosowerequireoptimizationstobewritteninaspecial-purposelanguage.OurapproachalsorequirestheCobaltexecutionenginetobepartoftheTCB,whiletrans-lationvalidationandcrediblecompilationdonotrequiretrustinanypartofthecompiler.

Proof-carryingcode[19],certifiedcompilation[21],typed

intermediatelanguages[34],andtypedassemblylan-guages[17,18]haveallbeenusedtoprovepropertiesofprogramsgeneratedbyacompiler.However,thekindsofpropertiesthattheseapproacheshavetypicallyguaranteedaretypesafetyandmemorysafety.Inourwork,weprovethestrongerpropertyofsemanticequivalencebetweentheoriginalandresultingprograms.

9.CONCLUSION

Wehavepresentedanapproachforautomaticallyprovingthecorrectnessofcompileroptimizations.Ourtechniqueprovidestheoptimizationwriterwithadomain-specificlan-guage,calledCobalt,forwritingoptimizations.Cobaltisbothreasonablyexpressiveandamenabletoautomatedcor-rectnessreasoning.Usingourtechniquewehaveprovencor-rectimplementationsofseveraloptimizationsoverarealisticintermediatelanguage.Webelieveourapproachisapromis-ingsteptowardthegoalofreliableanduser-extensiblecom-pilers.

Acknowledgments

ThisresearchissupportedinpartbyNSFgrantsCCR-0073379andACI-0203908,aMicrosoftGraduateFellow-ship,anIBMFacultyDevelopmentAward,andbygiftsfromSunMicrosystems.WewouldalsoliketothankKeunwooLee,AndrewPetersen,MarkSeigleandtheanonymousre-viewersfortheirusefulsuggestionsonhowtoimprovethepaper.

10.REFERENCES

[1]PatrickCousotandRadhiaCousot.Abstract

interpretation:Aunifiedlatticemodelforstaticanalysisofprogramsbyconstructionorapproximationoffixpoints.InConferenceRecordoftheFourthACMSymposiumon

PrinciplesofProgrammingLanguages,pages238–252,LosAngelesCA,January1977.

[2]PatrickCousotandRadhiaCousot.Systematicdesignof

programanalysisframeworks.InConferenceRecordoftheSixthACMSymposiumonPrinciplesofProgramming

Languages,pages269–282,SanAntonioTX,January1979.[3]PatrickCousotandRadhiaCousot.Systematicdesignof

programtransformationframeworksbyabstract

interpretation.InConferenceRecordofthe29thACMSIGPLAN-SIGACTSymposiumonPrinciplesof

ProgrammingLanguages,PortlandOR,January2002.

[4]JeffreyDean,GregDeFouw,DaveGrove,VassilyLitvinov,

andCraigChambers.Vortex:Anoptimizingcompilerforobject-orientedlanguages.InProceedingsofthe1996ACMConferenceonObject-OrientedProgrammingSystems,Languages,andApplications,pages83–100,SanJoseCA,October1996.

[5]E.M.ClarkeandE.A.Emerson.Synthesisof

SynchronizationSkeletonsforBranchingTimeTemporalLogic.InLogicsofPrograms:Workshop,volume131ofLectureNotesinComputerScience,YorktownHeights,NewYork,May1981.Springer-Verlag.

[6]CormacFlanagan,K.RustanM.Leino,MarkLillibridge,

GregNelson,JamesB.Saxe,andRaymieStata.ExtendedstaticcheckingforJava.InProceedingsoftheACMSIGPLAN’02ConferenceonProgrammingLanguageDesignandImplementation,June2002.

[7]DovGabbay,AmirPnueli,SaharonShelah,andJonathan

Stavi.Onthetemporalanalysisoffairness.InProceedingsofthe7thACMSIGPLAN-SIGACTsymposiumon

Principlesofprogramminglanguages,pages163–173,LasVegas,Nevada,1980.

[8]J.Guttman,J.Ramsdell,andM.Wand.VLISP:averified

implementationofScheme.LispandSymbolicCompucation,8(1-2):33–110,1995.

[9]M.KauffmannandR.S.Boyer.TheBoyer-Mooretheorem

proveranditsinteractiveenhancement.ComputersandMathematicswithApplications,29(2):27–62,1995.[10]JensKnoop,OliverR¨uthing,andBernhardSteffen.

Optimalcodemotion:Theoryandpractice.ACM

TransactionsonProgrammingLanguagesandSystems,16(4):1117–1155,July1994.

[11]DavidLacey,NeilD.Jones,EricVanWyk,and

CarlChristianFrederiksen.Provingcorrectnessofcompileroptimizationsbytemporallogic.InConferenceRecordofthe29thACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,PortlandOR,January2002.

[12]SorinLerner,DavidGrove,andCraigChambers.

Composingdataflowanalysesandtransformations.InConferenceRecordofthe29thACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,PortlandOR,January2002.

[13]SorinLerner,ToddMillstein,andCraigChambers.

Automaticallyprovingthecorrectnessofcompileroptimizations.TechnicalReportUW-CSE-02-11-02,UniversityofWashington,November2002.

[14]J.McCarthyandJ.Painter.Correctnessofacompilerfor

arithmeticexpressions.InT.J.Schwartz,editor,

ProceedingsofSymposiainAppliedMathematics,January1967.

[15]E.MorelandC.Renvoise.Globaloptimizationby

suppressionofpartialredundancies.CommunicationsoftheACM,22(2):96–103,February1979.

[16]F.LockwoodMorris.Adviceonstructuringcompilersand

provingthemcorrect.InConferenceRecordofthe1stACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,BostonMA,January1973.[17]GregMorrisett,KarlCrary,NealGlew,DanGrossman,

RichardSamuels,FrederickSmith,DavidWalker,StephanieWeirich,andSteveZdancewic.TALx86:A

realistictypedassemblylanguage.In1999ACMSIGPLANWorkshoponCompilerSupportforSystemSoftware,pages25–35,AtlantaGA,May1999.

[18]GregMorrisett,DavidWalker,KarlCrary,andNealGlew.

FromSystemFtoTypedAssemblyLanguage.ACMTransactionsonProgrammingLanguagesandSystems,21(3):528–569,May1999.

[19]GeorgeC.Necula.Proof-carryingcode.InConference

Recordofthe24thACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,Paris,France,January1997.

[20]GeorgeC.Necula.Translationvalidationforanoptimizing

compiler.InProceedingsoftheACMSIGPLANConferenceonProgrammingLanguageDesignandImplementation,pages83–95,Vancouver,Canada,June2000.[21]GeorgeC.NeculaandPeterLee.Thedesignand

implementationofacertifyingcompiler.InProceedingsoftheACMSIGPLAN’98ConferenceonProgramming

LanguageDesignandImplementation,Montreal,Canada,June1998.

[22]GeorgeC.NeculaandPeterLee.Proofgenerationinthe

Touchstonetheoremprover.InProceedingsofthe

InternationalConferenceonAutomatedDeduction,pages25–44,Pittsburgh,Pennsylvania,June2000.Springer-VerlagLNAI1831.

[23]GregNelsonandDerekC.Oppen.Simplificationby

cooperatingdecisionprocedures.ACMTransactionsonProgrammingLanguagesandSystems,1(2):245–257,October1979.

[24]D.P.Oliva,J.Ramsdell,andM.Wand.TheVLISP

verifiedPreSchemecompiler.LispandSymbolicComputation,8(1-2):111–182,1995.

[25]S.Owre,S.Rajan,J.M.Rushby,N.Shankar,andM.K.

Srivas.PVS:Combiningspecification,proofchecking,andmodelchecking.InComputer-AidedVerification,CAV’96,volume1102ofLectureNotesinComputerScience,pages411–414,NewBrunswick,NJ,July/August1996.Springer-Verlag.

[26]

A.Pnueli,M.Siegel,andE.Singerman.Translation

validation.InToolsandAlgorithmsforConstructionandAnalysisofSystems,TACAS’98,volume1384ofLectureNotesinComputerScience,pages151–166,1998.

[27]MartinRinard.Crediblecompilation.TechnicalReportMIT-LCS-TR-776,MassachusettsInstituteofTechnology,March1999.

[28]MartinRinardandDarkoMarinov.Crediblecompilation.InProceedingsoftheFLoCWorkshopRun-TimeResultVerification,July1999.

[29]

DavidA.Schmidt.Dataflowanalysisismodelcheckingofabstractinterpretations.InConferenceRecordofthe25thACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,SanDiegoCA,January1998.[30]

DavidA.SchmidtandBernhardSteffen.Dataflowanalysisasmodelcheckingofabstractinterpretations.InGiorgioLevi,editor,Proceedingsofthe5thInternational

SymposiumonStaticAnalysis(SAS),volume1503ofLectureNotesinComputerScience(LNCS),pages351–380.Springer-Verlag,September1998.[31]Simplifyautomatictheoremproverhomepage,

http://research.compaq.com/SRC/esc/Simplify.html.[32]

BernhardSteffen.Dataflowanalysisasmodelchecking.InT.ItoandA.R.Meyer,editors,TheoreticalAspectsof

ComputerScience(TACS),Sendai(Japan),volume526ofLectureNotesinComputerScience(LNCS),pages346–3.Springer-Verlag,September1991.

[33]BernhardSteffen.Generatingdataflowanalysisalgorithmsformodelspecifications.ScienceofComputerProgramming,21(2):115–139,1993.

[34]

DavidTarditi,GregMorrisett,PerryCheng,ChrisStone,RobertHarper,andPeterLee.TIL:Atype-directedoptimizingcompilerforML.InProceedingsoftheACMSIGPLAN’96ConferenceonProgrammingLanguageDesignandImplementation,PhiladelphiaPA,May1996.[35]

WilliamD.Young.Amechanicallyverifiedcodegenerator.JournalofAutomatedReasoning,5(4):493–518,December19.