中断驱动型航天嵌入式软件原子性违反检测方法于婷婷1,2李超1,2王博祥1陈睿1,2江云松1,21（北京轩宇信息技术有限公司北京100190）2（北京控制工程研究所北京100190）（yutingting@sunwiseinfo.com）AtomicityViolationDetectionforInterrupt-DrivenAerospaceEmbeddedSoftwareYuTingting1,2,LiChao1,2,WangBoxiang1,ChenRui1,2,andJiangYunsong1,21（BeijingSunwiseInformationTechnologyLtd.,Beijing100190）2（BeijingInstituteofControlEngineering,Beijing100190）AbstractThedependabilityofembeddedsoftwareisvitaltothesuccessoftheaerospacemission.Aerospaceembeddedsoftwareextensivelyusesinterrupt-drivenconcurrencymechanisms.However,uncertaininterleavingexecutionofinterruptsmaycauseconcurrencybugs,whichcouldresultinserioussafetyproblems.Researcheshadshowedthatatomicityviolationwasthemostprominentinterruptconcurrencybug.Currentatomicityviolationdetectionmethodsforinterrupt-drivenembeddedsoftwarecannotachievebothhighprecisionandhighscalability,andtheireffectivenessonrealembeddedsoftwarehasnotbeenevaluated.Tosignificantlyimprovetheabilityoftechniquesinbugdetection,wedesignanempiricalstudyon82atomicityviolationsinaerospaceembeddedsoftwareandgaintheirmanifestationcharacteristicsofatomicregionrange,thenumberofinterruptnestinglevels,shareddataaccessinterleavingpattern,accesspatternsandaccessgranularities.Onthisbasis,wepresentintAtom-S,apreciseandefficientstaticdetectiontechniqueforatomicityviolations.Firstly,torealizeaccurateanalysisofshareddata,intAtom-Sconstructsafine-grainedmemorymodelparameterizedbynumericalinvariants,andintroducesrule-basedmethodtoeliminateflagvariableaccesses.Moreover,itcanhandlearrayelementsaswellassharedI/Oaddresses.Then,alightweightdataflowanalysistechniqueisusedtofindallaccessinterleavingsthatmatchthepatternsaspotentialbugcandidates.Finally,intAtom-Sadoptsaconsecutiveaccesspairfeasibilityanalysisandaccessinterleavingfeasibilityanalysistoprunetheinfeasiblepaths.intAtom-Sgraduallyeliminatesfalsepositives,andobtainsthefinalatomicityviolations.Experimentsonabenchmarkand8real-worldaeros...
