基于SMT求解器的嵌入式多线程程序数据竞态条件分析  

Data Race Condition Analysis of Embedded Multi Thread Program Based on SMT Solver

作　　者：容会[1] 潘有顺 王艳玲 周祖坤[5] 王晓亮[6] RONG Hui;PAN Youshun;WANG Yanling;ZHOU Zukun;WANG Xiaoliang(Faculty of Art & Design,Kunming Metallurgy College,Kunming 650033;ComputerTechnologyApplicationKeyLabofYunnanProvince,KunmingUniversityofScienceandTechnology,Kunming 650500;Faculty of Information Engineering and Automation,Kunming University of Science and Technology,Kunming 650500;Faculty of Foreign Languages,Kunming Metallurgy College,Kunming 650033;Recruitment and Employment Office,Kunming Metallurgy College,Kunming 650033;Business Faculty,Kunming Metallurgy College,Kunming 650033)

机构地区：[1]昆明冶金高等专科学校艺术设计学院,昆明650033 [2]昆明理工大学云南省计算机技术应用重点实验室,昆明650500 [3]昆明理工大学信息工程与自动化学院,昆明650500 [4]昆明冶金高等专科学校外语学院,昆明650033 [5]昆明冶金高等专科学校招生就业处,昆明650033 [6]昆明冶金高等专科学校商学院,昆明650033

出　　处：《计算机与数字工程》2018年第3期424-428,共5页Computer & Digital Engineering

基　　金：国家自然科学基金项目(编号:61662088);云南省应用基础研究项目(编号:2013FZ107);昆明冶金高等专科学校科研基金项目(编号:14B004)资助

摘　　要：针对嵌入式多线程程序中出现的数据竞态条件,论文提出了一种基于SMT求解器数据竞态条件检测分析方法。通过对多线程程序执行路径与源程序分析,构建对应的约束条件,将其作为输入,SMT求解器验证是否满足数据竞态条件。通过实验,论文提出的嵌入式多线程程序数据竞态条件的分析与检测方法在检测效率上还是比较理想的。In view of the data race conditions in embedded multithreaded programs,a method for detecting and analyzing race race condition based on SMT solver is proposed in this paper.Through analyzing the execution path and source program of multi thread program,the corresponding constraint condition is constructed,and the SMT solver is used to verify whether the data competition condition is satisfied.Through experiments,the method of analyzing and detecting the data race condition of embedded multithreaded programs is more satisfactory.

关 键 词：嵌入式多线程程序 数据竞态条件 竞态条件分析 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]