基于上下文定界的Fork/Join并行性的并发程序可达性分析

摘要：

随着多核技术日益发展,并发程序通过引入Fork/Join并行性,将任务分解为更细粒度的子任务并行执行,从而充分利用多核处理器提供的计算性能.并发执行线程之间的交错可能产生隐匿的程序设计错误,因此有必要对此类并发程序的正确性进行分析.上下文定界分析方法是一种检测并发程序中隐匿错误的高效方法,计算线程有限次上下文切换内的可达状态,确定错误状态是否可达.针对Fork/Join并行性的并发程序的可达性分析思想如下:首先,动态并发程序被建模为可模拟线程Fork/Join操作的动态并发下推系统P；然后从P中提取模拟其k-定界执行的并发下推系统Pk.现有的上下文定界可达算法可解决提取后的并发下推系统的k-定界可达性问题.

关键词：上下文定界、并发、可达性分析、Fork/Join并行性、动态线程创建

所属期刊栏目：35

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目61063002,61262008;中国博士后基金资助项目20090450211;广西自然科学基金资助项目2011GXNSFA018164,2011GXNSFA018166;广西高等学校优秀人才资助计划资助项目;广西可信软件重点实验室开放基金;广西研究生科研创新项目资助项目2011105950812M19

在线出版日期：2013-04-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1-6