Simulating reachability using first-order logic wi

SimulatingReachabilityusingFirst-OrderLogicwithApplicationstoVerificationofLinkedDataStructuresT.Lev-Ami1,N.Immerman2?,T.Reps3??,M.Sagiv1,S.Srivastava2?,andG.Yorsh1???1SchoolofComp.Sci.,TelAvivUniv.,ftla,msagiv,[e-mail],Amherstfimmerman,[e-mail].,Univ.ofWisconsin,[e-mail]rnessexistingtheoremproversforfirst-orderlogictoautomaticallyverifysafetypropertiesofimperativeprogramsthatperformdynamicstorageallocationanddestructiveupdatingofpointer-valuedstructurefields.Oneofthemainobstaclesisspecifyingandprovingthe(absence)ofreachabilitypropertiesamongdynamicallyallocatedcells.Themaintechnicalcontributionsaremethodsforsimulatingreachabilityinacon-servativewayusingfirst-orderformulas—theformulasdescribeasupersetofthesetofprogramstatesthatcanactuallyarise.Thesemethodsareemployedforsemi-automaticprogramverification(i.e.,usingprogrammer-suppliedloopinvariants)onprogramssuchasmark-and-sweepgarbagecollectionanddestructivereversalofasinglylinkedlist.(Themark-and-sweepexamplehasbeenpreviouslyreportedasbeingbeyondthecapabilitiesofESC/Java.)1IntroductionThispaperexploreshowtoharnessexistingtheoremproversforfirst-orderlogictoprovereachabilitypropertiesofprogramsthatmanipulatedynamicallyallocateddatastructures.Theapproachthatweuseinvolvessimulatingreachabilityinaconserva-tivewayusingfirst-orderformulas—i.e.,theformulasdescribeasupersetofthesetofprogramstatesthatcanactuallyarise.Automaticallyestablishingsafetyandlivenesspropertiesofsequentialandconcur-rentprogramsthatpermitdynamicstorageallocationandlow-levelpointermanipula-tionsischallenging.Dynamicallocationcausesthestatespacetobeinfinite;moreover,aprogramispermittedtomutateadatastructurebydestructivelyupdatingpointer-valuedfieldsofnodes.Thesefeaturesremainevenifaprogramminglanguagehasgoodcapabilitiesfordataabstraction.Abstract-datatypeoperationsareimplementedusingloops,procedurecalls,andsequencesoflow-levelpointermanipulations;consequently,itishardtoprovethatadata-structureinvariantisreestablishedonceasequenceofop-erationsisfinished[1].InlanguagessuchasJava,concurrencyposesyetanotherchal-lenge:establishingtheabsenceofdeadlockrequiresestablishingtheabsenceofanycycleofthreadsthatarewaitingforlocksheldbyotherthreads.Reachabilityiscrucialforreasoningaboutlinkeddatastructures.Forinstance,toestablishthatamemoryconfigurationcontainsnogarbageelements,wemustshowthat?SupportedbyNSFgrantCCR-0207373andaGuggenheimfellowship.??SupportedbyONRundercontractsN00014-01-1-f0796,0708g.???PartiallysupportedbytheIsraeliAcademyofScienceeveryelementisreachablefromsomeprogramvariable.Othercaseswherereachabilityisausefulnotioninclude–Specifyingacyclicityofdata-structurefragments,i.e.,everyelementreachablefromnodencannotreachn–Specifyingtheeffectofprocedurecallswhenreferencesarepassedasarguments:onlyelementsthatarereachablefromaformalparametercanbemodified–Specifyingtheabsenceofdeadlocks–Specifyingsafetyconditionsthatallowestablishingthatadata-structuretraversalterminates,e.g.,thereisapathfromanodetoasink-nodeofthedatastructure.Theverificationofsuchpropertiespresentsachallenge.Evensimpledecidablefrag-mentsoffirst-orderlogicbecomeundecidablewhenreachabilityisadded[2,3].More-over,theutilityofmonadicsecond-orderlogicontreesisratherlimitedbecause(i)manyprogramsallownon-treedatastructures,(ii)expressingpostconditionsofprocedures(whichisessentialformodularreasoning)requiresreferringtothepre-statethatholdsbeforetheprocedureexecutes,andthuscannot,ingeneral,beexpressedinmonadicsecond-orderlogicontrees—evenforproceduresthatmanipulateonlysingly-linkedlists,suchasthein-situlist-reversalprogramshowninFig.6(a),and(iii)thecomplex-ityisprohibitive.Whileourworkwasactuallymotivatedbyourexperienceusingabstractinterpreta-tion–and,inparticular,theTVLAsystem[4–6]–toestablishpropertiesofprogramsthatmanipulateheap-allocateddatastructures,inthispaper,weconsidertheproblemofverifyingdata-structureoperations,assumingthatwehaveuser-suppliedloopinvari-ants.ThisissimilartotheapproachtakeninsystemslikeESC/Java[7],andPale[8].Thecontributionsofthepapercanbesummarizedasfollows:HandlingFO(TC)formulasusingFOtheoremprovers.Wewanttousefirst-ordertheoremproversandweneedtodiscussthetransitiveclosureofcertainbinarypredicates,f.However,first-ordertheoremproverscannothandletransitiveclosure.Wesolvethisconundrumbyaddinganewrelationsymbolftcforeachsuchf,togetherwithfirst-orderaxiomsthatassurethatftcisinterpretedcorrectly.ThetheoreticaldetailsofhowthisisdonearepresentedinSections3and4.Thefactthatweareabletohandletransitiveclosureeffectivelyandreasonablyautomaticallyisamajorcontributionandquitesurprising.AsexplainedinSection3,theaxiomsthatweaddtocontrolthebehavioroftheaddedpredicates,ftc,mustbesoundbutnotnecessarilycomplete.Onewaytothinkaboutthisisthatwearesimulatingaformula,Â,inwhichtransitiveclosureoccurs,withapurefirst-orderformulaÂ0.IfouraxiomsarenotcompletethenweareallowingÂ0todenotemorestoresthanÂdoes.Thisismotivatedbythefactthatabstractioncanbeanaidinthev