CN 43-1258/TF ISSN 1007-130X
计算机工程与科学
Computer Engineering &. Science
文章编号：1007-130X(2013)02-0001-06
第35卷第2期2013年2月 Vol.35,No.2,Feb.2013
基于上下文定界的Fork/Join并行性的并发程序可达性分析
钱俊彦1.2，贾书贵1，蔡国永"，赵岭忠1
（1.桂林电子科技大学计算机科学与工程学院，广西桂林541004；
2.并行与分布处理国家重点实验室，湖南长沙410073)
摘要：随着多核技术日益发展，并发程序通过引入Fork/Join并行性，将任务分解为更细粒度的子任务并行执行，从而充分利用多核处理器提供的计算性能。并发执行线程之间的交错可能产生隐匿的程序设计错误，固此有必要对此类并发程序的正确性进行分析。上下文定界分析方法是一种检测并发程序中隐匿错误的高效方法，计算线程有限次上下文切换内的可达状态，确定错误状态是否可达。针对Fork/ Join并行性的并发程序的可达性分析思想如下：首先，动态并发程序被建模为可模拟线程Fork/Join操作的动态并发下推系统P；然后从P中提取模拟其k-定界执行的并发下推系统P。现有的上下文定界可达算法可解决提取后的并发下推系统的人-定界可达性问题。
关键词：上下文定界；并发；可达性分析；Fork/Join并行性；动态线程创建
中图分类号：TP311
doi:10.3969/j.issn.1007-130X.2013.02.001
文献标志码：A
Context-boundedanalysisofconcurrent programs with Fork/Join parallelism QIAN Jun-yan'-,JIA Shu-gui' ,CAI Guo-yong",ZHAO Ling-zhong'
(1, School of Computer Science and Engineering,Guilin University of Electronie Technology,Guilin 541004;
2. National Key Laboratory for Parallel and Distributed Processing, Changsha 410073,China)
Abstract As multi-core technique has been well developed, in order to utilize the computing power provided by multi-core processor, concurrent programs bring in Fork/Join parallelism to decompose a task into fine-grained subtasks, But interaction among concurrent threads results in insidious program ming errors, it is necessary to analyze the correctness of these concurrent programs, Context-bounded a-nalysis is an efficient method for finding insidious errors in concurrent programs by computing reachable states in a run within a bounded number of context switches, it determines whether an error state is reachable or not. In this paper, we perform reachablility analysis for concurrent programs with Fork/ Join parallelism. The main idea is as follows: dynamic concurrent programs is modeled as an abstract model-dynamic concurrent pushdown system P, the abstract model can simulate the Fork/Join opera tion, then a concurrent pushdown system P can be abstracted from dynamic pushdown system that simu late the k-bounded execution of P, and the k-reachability problems of abstracted P, can be solved by ex isting context-bounded reachability algorithm.
Key words:context-bounded; concurrency;reachability analysis fork/join parallelism;dynamic thread creation
收精旦期：2012-03-11：修回日期：2012-06-15
基金项目：国家自热科学基金资助项日（6106300251262008）：中国博士后基金资助项目（20090450211）：广西白自然科学基金资助项 9 助项目：广西研究生科研创新项目资助美目（2011105950812M19）
通讯地址：541004广西桂林市桂林电子科技大学计算机科学与工程学院
Address; School of Computer Science and Engineering.Guilin University of Electronic Technology ,Guilin 541004,Guangxi,P, R, China
万方数据