copyright c00903

《copyright c00903》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、SRCTechnicalNote2001-003November19,2001Thread-ModularVerificationForShared-MemoryProgramsCormacFlanaganStephenN.FreundShazQadeerSystemsResearchCenter130LyttonAvenuePaloAlto,California94301http://www.research.compaq.com/SRC/CopyrightcCompaqComputerCorporation2001.Al

2、lrightsreservedAbstractEnsuringthereliabilityofmultithreadedsoftwaresystemsisdifficultduetotheinteractionbetweenthreads.Thispaperdescribesthedesignandimplementationofastaticcheckerforsuchsystems.Toavoidconsideringallpossiblethreadinterleavings,thecheckerusesassume-g

3、uaranteereasoning,andreliesontheprogrammertospecifyanenvironmentassumptionthatconstrainstheinteractionbetweenthreads.Usingthisenvironmentassumption,thecheckerreducestheverificationoftheoriginalmultithreadedprogramtotheverificationofseveralse-quentialprograms,onefore

4、achthread.Thesesequentialprogramsaresubsequentlyanalyzedusingextendedstaticcheckingtechniques(basedonverificationconditionsandautomaticthe-oremproving).Experienceindicatesthatthecheckeriscapableofhandlingarangeofsynchro-nizationdisciplines.Inaddition,therequiredenv

5、ironmentassumptionsaresimpleandintuitiveforcommonsynchronizationidioms.1IntroductionEnsuringthereliabilityofcriticalsoftwaresystemsisanimportantbutextremelydifficulttask.Anumberofusefultoolsandtechniqueshavebeendevelopedforreasoningaboutsequentialsystems.Unfortunate

6、ly,thesesequentialanalysistoolsarenotapplicabletomanycriticalsoftwaresystemsbecausesuchsystemsareoftenmultithreaded.Thepresenceofmultiplethreadssignificantlycom-plicatestheanalysisbecauseofthepotentialforinterferencebetweenthreads;eachatomicstepofathreadcaninfluence

7、thesubsequentbehaviorofotherthreads.Formultithreadedprograms,morecomplexanalysistechniquesarenecessary.Theclassicalassertionalapproach[Ash75,OG76,Lam77,Lam88]requirescontrolpredicatesateachprogrampointtospecifythereachableprogramstates,buttheannotationburdenforusi

8、ngthisapproachishigh.Somepromisingtools[CDH+00,Yah01]usemodelcheckingandabstractinterpretationtoinferthereachablestatesetautomatically,buttheneedtoconsi