Combining Symbolic Execution with Model Checking t

CombiningSymbolicExecutionwithModelCheckingtoVerifyParallelNumericalProgramsSTEPHENF.SIEGELUniversityofDelawareANASTASIAMIRONOVAUniversityofUtahandGEORGES.AVRUNINandLORIA.CLARKEUniversityofMassachusettsWepresentamethodtoverifythecorrectnessofparallelprogramsthatperformcomplexnumericalcomputations,includingcomputationsinvolvingoating-pointarithmetic.Thismethodrequiresthatasequentialversionoftheprogrambeprovided,toserveasthespecicationfortheparallelone.Thekeyideaistousemodelchecking,togetherwithsymbolicexecution,toestablishtheequivalenceofthetwoprograms.Inthisapproachthepathconditionfromsymbolicexecutionofthesequentialprogramisusedtoconstrainthesearchthroughtheparallelprogram.Tohandleoating-pointoperations,threedierenttypesofequivalencearesupported.Severalexamplesarepresented,demonstratingtheapproachandactualerrorsthatwerefound.Limitationsanddirectionsforfutureresearcharealsodescribed.CategoriesandSubjectDescriptors:D.2.4[SoftwareEngineering]:Software/ProgramVeri-cation|formalmethods,modelchecking,validationGeneralTerms:VericationAdditionalKeyWordsandPhrases:Finite-stateverication,numericalprogram,oating-point,modelchecking,concurrency,parallelprogramming,highperformancecomputing,symbolicexe-cution,MPI,MessagePassingInterface,SpinThisisarevisedandextendedversionofapaperpresentedatthe2006InternationalSymposiumonSoftwareTestingandAnalysis(ISSTA2006).ThisresearchwaspartiallysupportedbytheNationalScienceFoundationunderawardsCCF-0427071,CCR-0205575,andCCF-0541035,andbytheU.S.DepartmentofDefense/ArmyResearchOceunderawardsDAAD19-01-1-0564andDAAD19-03-1-0133.WealsowishtothanktheComputingResearchAssociation'sCRA-WDis-tributedMentorProgramandtheCollegeofNaturalSciencesandMathematicsattheUniversityofMassachusettsforsponsoringandfundingMironovaduringthesummerof2004.Anyopin-ions,ndings,andconclusionsorrecommendationsexpressedinthispublicationarethoseoftheauthorsanddonotnecessarilyreecttheviewsoftheNationalScienceFoundationortheU.S.DepartmentofDefense/ArmyResearchOce.Authors'addresses:S.Siegel,DepartmentofComputerandInformationSciences,UniversityofDelaware,Newark,DE19716;email:[e-mail];A.Mironova,ScienticComputingandImagingInstitute,UniversityofUtah,SaltLakeCity,UT84112;email:[e-mail];G.Avrunin,L.Clarke,DepartmentofComputerScience,UniversityofMassachusetts,Amherst,MA01003;email:favrunin,[e-mail]/hardcopyofallorpartofthismaterialwithoutfeeforpersonalorclassroomuseprovidedthatthecopiesarenotmadeordistributedforprotorcommercialadvantage,theACMcopyright/servernotice,thetitleofthepublication,anditsdateappear,andnoticeisgiventhatcopyingisbypermissionoftheACM,Inc.Tocopyotherwise,torepublish,topostonservers,ortoredistributetolistsrequirespriorspecicpermissionand/orafee.c2007ACM0000-0000/2007/0000-0001$5.00ACMJournalName,Vol.V,No.N,September2007,PagesBD.TBD
StephenF.Siegeletal.1.INTRODUCTIONIndomainsthatrequireextensivecomputation,suchashigh-performancescienticcomputing,aprogrammaybedividedupamongseveralprocessorsworkinginparallelinordertoreducetheoverallexecutiontimeandincreasethetotalamountofmemoryavailabletotheprogram.Theprocessof\parallelizingasequentialprogramisnotoriouslydicultanderror-prone.Attemptstoautomatethisprocesshavemetwithonlylimitedsuccess,andthusmostparallelcodeisstillwrittenbyhand.Thedevelopersofsuchprogramsexpendanenormousamountofeortintesting,debugging,andavarietyofadhocmethodstoconvincethemselvesthattheircodeiscorrect.Henceanytechniquesthatcanhelpestablishthecorrectnessoftheseprogramsorndbugsinthemwouldbeveryuseful.Inthispaperwefocusonparallelnumericalprograms.Byanumericalprogramwemeanaprogramwhoseprimaryfunctionistoperformanumericalcomputation.Forthepurposesofthispaper,wewillthinkofanumericalprogramastakingavectorof(usuallyoating-point)numbersforinputandproducinganothersuchvectorasoutput.Examplesincludeprogramsthatimplementmatrixalgorithms,simulatephysicalphenomena,ormodeltheevolutionofasystemofdierentialequations.Weareinterestedintechniquesthatcanestablishthecorrectnessofaprogramofthistype|i.e.,provethattheprogramalwaysproducesthecorrectoutputforanyinput|orexhibitappropriatecounterexamplesiftheprogramisnotcorrect.Theusualmethodforaccomplishingthis|testing|hastwosignicantdraw-backs.Intherstplace,itisusuallyinfeasibletotestmorethanatinyfractionoftheinputsthataparallelnumericalprogramwillencounterinuse.Thus,testingcanrevealbugs,but,asiswell-known,itcannotshowthattheprogrambehavescorrectlyontheinputsthatarenottested.Secondly,thebehaviorofconcurrentprograms,includingmostparallelnumericalprograms,typicallydependsontheorderinwhicheventsoccurindierentprocesses.Thisorderdependsinturnontheloadontheprocessors,thelatencyofthecommunicationnetwork,andothersuchfactors.Aparallelnumericalprogrammaythusbehavedierentlyondierentexecutionswiththesameinputvector,sogettingthecorrectresultonatestexe-cutiondoesnotevenguaranteethattheprogramwillbehavecorrectlyonanotherexecutionwiththesameinput.Themethodproposedhere,whichcombinesmodelcheckingwithsymbolicex