过程间并发程序分析不可判定的一个新证明方法
过程间并发程序分析问题是一个不可判定问题,理解这个不可判定问题的来源是发展一个有效的分析算法的基础.现有的证明通过构造三个并发任务的PCP问题实例,证明了过程间并发程序分析过程间并发程序分析是一个不可判定问题.本文利用反射的思想,仅仅用两个并发任务构造了该问题的一个PCP问题实例,证明了在两个并发任务的情况下,过程间并发程序分析是一个不可判定问题.证明的构造过程直观地显示了这个不可判定问题的来源.不可判定的表现形式是,在一个任务内形成两个可交织的过程匹配,其中一个过程匹配是另一个并发任务的过程匹配通过同步匹配产生的”投影”.基于证明的启发,本文给出了一个简单的,过程间并发程序分析不可判定的必要条件.
并发程序分析 软件工程 并发任务
缪力 张大方 杨金民
湖南大学软件学院
国内会议
北戴河
中文
65-70
2006-08-07（万方平台首次上网日期，不代表论文的发表时间）