SoftMC03-Preliminary-Version-Space-Reduction-Strat

SoftMC’03PreliminaryVersionSpace-ReductionStrategiesforModelCheckingDynamicSoftwareRobbya,MatthewB.Dwyera,JohnHatcliffaandRaduIosifbaDepartmentofComputingandInformationSciences,KansasStateUniversity234NicholsHall,ManhattanKS,66506,USA.{robby,dwyer,hatcliff}@cis.ksu.edubVerimag/CNRS2AvenuedeVignate,38610Gieres,[e-mail].1IntroductionDespiteitssignificantcomplexity,modelcheckinghasproventobeaneffec-tivetechniqueforuncoveringsubtleerrorsintheimplementationofconcur-rentprograms[2].Researchersareworkingonavarietyoftechniquestoallowmodelcheckingtoscaletobeaneffectiveanalysisframeworkforlarge,com-plexconcurrentprograms.Twodirectionsbeingpursuedareautomateddataabstraction(e.g.,[15])andthreadmodularapproaches(e.g.,[11,14]).Whiletheseofferthepotentialforscalability,theuseofsuchtechniquesiscurrentlylimitedtoreasoningaboutpropertiesofscalardatathatarelocaltothreads.Theyarenot,forexample,applicabletoreasoningaboutpropertiesthatspanmultipleprogramthreadsandthatrelatetocomplexheapstructures.Forthosekindsofproperties,whichariseinspecificationsofobject-basedconcur-rentsystems,generalexplicit-statemodelcheckingapproachesfordynamicsoftware[2,6,7]mustbeused.Inthispaper,wepresentmethodsthatenablememoryreductionsforexplicit-statemodelcheckingofdynamicsoftware.Reductionofboththenumberofprogramstatesthatarestoredandofthesizeofthosestatesarepresented.Ourworkextendsexistingapproachesforexploitingsymmetriesinthestructureofaprogram’sdynamicdata(i.e.,heap)[17].Specifically,wede-velopaflexibleframeworkforidentifyingsymmetricheapstatesthatistunabletotraderun-timeoverheadforprecision.Inaddition,weimprovethethreadThisisapreliminaryversion.ThefinalversionwillbepublishedinElectronicNotesinTheoreticalComputerScienceURL:(orprocess)symmetry[1]inthecalculationofheapsymmetryinformationtoimproveontheresultsof[17]byprovidingbetterheuristicsforthreadorder-ing.Ingeneral,ourapproachcanbeappliedtoanynon-deterministicheapobjectdiagram.Theframeworkispresentedusinggroup-theoreticnotionsthatgreatlysimplifyitsformalization.Wealsoextendexistingapproachestocompressingtherepresentationofindividualprogramstates(e.g.,[16])byidentifyinginformationthatissharedbymultiplestatecomponentsandelim-inatingthatduplicateinformationfromthestateencoding.Thecontributionsofthepaperinclude:(i)thedefinitionofaframeworkandalgorithmforcombinedheapandthreadsymmetryreductioninexplicit-statemodelchecking;(ii)thedefinitionofaframeworkandalgorithmforduplication-reducingstate-spaceencodings;and(iii)empiricaldatatosup-porttheeffectivenessofthesememoryreductionsonacollectionofrealisticexamples.ThesereductionsareimplementedinanewmodelcheckingframeworkcalledBogor.Bogor[21]isanextensibleandhighlymodularexplicit-statemodelcheckingframework.Itprovidesarichmodelinglanguageincludingfeaturesthatallowfordynamiccreationofobjectsandthreads,garbagecol-lection,virtualmethodcallsandexceptionhandling.Italsoprovidesextensionmechanismstoeasethetaskofcustomizingthemodelcheckerwithdomain-specificabstractionlayersandtoaccommodate,forexample,variationsinschedulingpolicies,searchmodesforstateexploration,stateencodings,andcheckersforspecificationlanguages.Bogorhasbeencustomizedtosupportdifferentkindsofsoftwareartifactsincluding:Javasourcecode[9]andevent-drivencomponent-baseddesigns[8,12].ThetechniquesdescribedinthispaperarebroadlyapplicableandhelptomakeBogoranefficientcoreonwhichtobuilddomain-specificmodelchecking-basedanalyses.Thenextsectionpresentsanexampleusedtointroducethereductionspresentedinthepaper.Section3presentsourgeneralsymmetryreductionframeworkanddescribeshowheapandthreadsymmetriesarecombined.Sec-tion4describeshowinformationfromsymmetryreductionscandrivethecompressionofheapdataencodings.Section5presentspreliminaryempiricalresultsthatsuggestthebenefitofusingourmemoryreductions.RelatedworkisdiscussedinSection6andweconcludewithadiscussionoffutureworkinSection7.2AnExampleFigure1presentsafragmentoftheBIR(Bogor’sinputlanguage)modelfortheN-diningphilosophersproblem–anexampleofresourcedeadlockincon-currentprograms.Thisexampleissmall,butinterestingenoughtoillustratemanyofourproposedreductionstrategies.ABIRsystem(inthiscasenamednDiningPhilosophers)consistsofdec-larationsofrecordsandthreads.BIRrecordsareusedtomodelthestateof2Robby,Dwyer,Hatcliff,IosifsystemnDiningPhilosophers{toprecordObject{}recordForkextendsObject{booleanisHeld;}threadPhilosopher(Forkleft,Forkright){locloc0://getleftwhen!left.isHelddo{left.isHeld:=true;}gotoloc1;locloc1://getrightwhen!right.isHelddo{right.isHeld:=true;}gotoloc2;locloc2://droprightwhentruedo{right.isHeld:=false;}gotoloc3;locloc3://dropleftwhentruedo{left.isHeld:=false;}gotoloc0;}mainthreadMAIN(){...}}Fig.1.N-DiningPhilosophersExample(excerpts)F1trueWVUTPQRSP3loc0rightooleft;;;;;;;;;ιǫ//ǫ%%ǫ99WVUTPQRSP1loc1leftAAright;;;;;;;;;F2falseF3falseWVUTPQRSP2loc0leftoorightAAFig.2.3-DiningPhilosophersStateEx-ampleJavaobjects,andasubtyperelationisassociatedwiththemtomodelJava’sclassinheritancehiera