Using model checking with symbolic execution to ve

UsingModelCheckingwithSymbolicExecutiontoVerifyParallelNumericalProgramsSTEPHENF.SIEGELUniversityofDelawareANASTASIAMIRONOVAUniversityofUtahandGEORGES.AVRUNINandLORIA.CLARKEUniversityofMassachusettsWepresentamethodtoverifythecorrectnessofparallelprogramsthatperformcomplexnumericalcomputations,includingcomputationsinvolvingfloating-pointarithmetic.Themethodrequiresthatasequentialversionoftheprogrambeprovided,toserveasthespecificationfortheparallelone.Thekeyideaistousemodelchecking,togetherwithsymbolicexecution,toestablishtheequivalenceofthetwoprograms.CategoriesandSubjectDescriptors:D.2.4[SoftwareEngineering]:Software/ProgramVerifi-cation—formalmethods,modelchecking,validationGeneralTerms:VerificationAdditionalKeyWordsandPhrases:Finitestateverification,numericalprogram,floating-point,modelchecking,concurrency,parallelprogramming,highperformancecomputing,symbolicexe-cution,MPI,MessagePassingInterface,Spin1.INTRODUCTIONIndomainsthatrequireextensivecomputation,suchashigh-performancescientificcomputing,aprogrammaybedividedupamongseveralprocessorsworkinginparallelinordertoreducetheoverallexecutiontimeandincreasethetotalamountofmemoryavailabletotheprogram.Theprocessof“parallelizing”asequentialprogramisnotoriouslydifficultanderror-prone.Attemptstoautomatethisprocesshavemetwithonlylimitedsuccess,andthusmostparallelcodeisstillwrittenbyThisisarevisedandextendedversionofapaperpresentedatISSTA2006.Thisresearchwaspar-tiallysupportedbytheNationalScienceFoundationunderawardsCCF-0427071,CCR-0205575,andCCF-0541035,andbytheU.S.DepartmentofDefense/ArmyResearchOfficeunderawardsDAAD19-01-1-0564andDAAD19-03-1-0133.WealsowishtothanktheComputingResearchAssociation’sCRA-WDistributedMentorProgramandtheCollegeofNaturalScienceandMath-ematicsattheUniversityofMassachusettsforsponsoringtheprogramandfunding,respectively,forMironovaduringthesummerof2004.Anyopinions,findings,andconclusionsorrecommenda-tionsexpressedinthispublicationarethoseoftheauthorsanddonotnecessarilyreflecttheviewsoftheNationalScienceFoundationortheU.S.DepartmentofDefense/ArmyResearchOffice.Authorsaddresses:S.Siegel,DepartmentofComputerandInformationSciences,UniversityofDelaware,Newark,DE19716;email:[e-mail];A.Mironova,ScientificComputingandImagingInstitute,UniversityofUtah,SaltLakeCity,UT84112;email:[e-mail];G.Avrunin,L.Clarke,DepartmentofComputerScience,UniversityofMassachusetts,Amherst,MA01003;email:{avrunin,clarke}@cs.umass.edu.2·StephenF.Siegeletal.hand.Thedevelopersofsuchprogramsexpendanenormousamountofeffortintesting,debugging,andavarietyofadhocmethodstoconvincethemselvesthattheircodeiscorrect.Henceanytechniquesthatcanhelpestablishthecorrectnessoftheseprogramsorfindbugsinthemwouldbeveryuseful.Inthispaperwefocusonparallelnumericalprograms,i.e.,parallelprogramsthattakeasinputavectorof(usuallyfloating-point)numbersandproduceasoutputanothersuchvector.Examplesincludeprogramsthatimplementmatrixalgorithms,simulatephysicalphenomena,ormodeltheevolutionofasystemofdifferentialequations.Weareinterestedintechniquesthatcanestablishthecor-rectnessofaprogramofthistype—i.e.,provethattheprogramalwaysproducesthecorrectoutputforanyinput—orexhibitappropriatecounterexamplesiftheprogramisnotcorrect.Theusualmethodforaccomplishingthis—testing—hastwosignificantdraw-backs.Inthefirstplace,itisusuallyinfeasibletotestmorethanatinyfractionoftheinputsthataparallelnumericalprogramwillencounterinuse.Thus,testingcanrevealbugs,but,asiswell-known,itcannotshowthattheprogrambehavescorrectlyontheinputsthatarenottested.Secondly,thebehaviorofconcurrentprograms,includingmostparallelnumericalprograms,typicallydependsontheorderinwhicheventsoccurindifferentprocesses.Thisorderdependsinturnontheloadontheprocessors,thelatencyofthecommunicationnetwork,andothersuchfactors.Aparallelnumericalprogrammaythusbehavedifferentlyondifferentexecutionswiththesameinputvector,sogettingthecorrectresultonatestexe-cutiondoesnotevenguaranteethattheprogramwillbehavecorrectlyonanotherexecutionwiththesameinput.Themethodproposedhere,whichcombinesmodelcheckingwithsymbolicexe-cutioninanovelway,doesnotexhibitthesetwolimitations:itcanbeusedtoshowthataparallelnumericalprogramproducestherightresultonanyinputvector,regardlessoftheparticularwayinwhichtheeventsfromtheconcurrentprocessesareinterleaved.Inattemptingtoapplymodelcheckingtechniquesinthissetting,twoissuesimmediatelypresentthemselves.First,thesetechniquesrequiretheprogrammertosupplyafinite-statemodeloftheprogrambeingchecked.Butnumericalprogramstypicallydealwithhugeamountsoffloating-pointdata,andtheverynatureofourproblemdictatesthatwecannotjustabstractthisdataaway.Henceitisnotobvioushowtoconstructappropriatefinite-statemodelsoftheprogramswithoutgreatlyexacerbatingthestateexplosionproblem.Thesecondissueconcernsthenatureofthepropertywewishtocheck:thestatementthattheoutputproducedbytheprogramiscorrectmustbemadeprecise,andformulatedinsomewaythatisamenabletomodelcheckingtools.Wedealwiththefirstissuebymodelingcomputationsintheprogramssymbol-ically.Thatis,inourmodel,theinputisconsideredtobeavector