欢迎来到天天文库
浏览记录
ID:33928659
大小:226.52 KB
页数:20页
时间:2019-02-28
《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
此文档下载收益归作者所有