-
题名过程间并发程序分析不可判定的一个新证明方法
- 1
-
-
作者
缪力
张大方
-
机构
湖南大学软件学院
-
出处
《计算技术与自动化》
2007年第2期53-56,共4页
-
基金
国家自然科学基金资助项目(60473031
60673155)
-
文摘
过程间并发程序分析问题是一个不可判定问题,理解这个不可判定问题的来源是发展一个有效的分析算法的基础。现有的证明[1]通过构造三个并发任务的PCP问题实例,证明过程间并发程序分析是一个不可判定问题。利用反射的思想,仅仅用两个并发任务构造该问题的一个PCP问题实例,证明在两个并发任务的情况下,过程间并发程序分析是一个不可判定问题。
-
关键词
过程间并发程序分析
上下文敏感
同步敏感
不可判定问题
-
Keywords
concurrent interprocedural program analysis
context - sensitive analysis
synchronization - sensitive analysis
undecidable problem
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-
-
题名通信下推系统的一种有界可达算法
- 2
-
-
作者
缪力
张大方
-
机构
湖南大学软件学院
-
出处
《计算机工程与应用》
CSCD
北大核心
2008年第24期19-21,共3页
-
基金
国家自然科学基金No.60673155
No.90718008~~
-
文摘
Qadeer首次针对并发下推系统提出一种有界可达算法,通过限定上下文切换的次数使得算法可终止,可有效地分析过程间并发程序。但是并发下推系统以全局变量模拟同步,不适应于当前广泛使用的基于事件驱动的并发程序。针对通信下推系统,提出一种基于双重调度的有界可达算法,通过限定同步调度的次数,结合线程间的同步调度和线程内的路径调度解决通信下推系统的可达性问题,从而为事件驱动的过程间并发程序分析提供了算法基础。
-
关键词
有界可达算法
通信下推系统
并发过程间程序分析
模型检查
-
Keywords
bounded reaching algorithm
communicated pushdown system
interprocedural concurrent program analysis
model checking
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-