基于全同步对覆盖的线程调度序列生成方法

？针对多线程并发程序生成覆盖同步语句的线程调度序列(tss)效率低问题,提出了一种基于全同步对覆盖(apsc)准则的tss生成(tgba)方法。首先,对并发程序中的同步语句,定义了同步对及apsc;然后,给出了一个同步对-线程关联图(sptg)构建方法;在此基础上,生成满足apsc的tss;最后,使用jpf检测工具,对4个java类库并发程序进行了tss生成实验,并与常用的默认线程调度(ds)、抢占式线程调度(ps)和交叉线程调度(cs)序列生成方法在生成效率方面进行了对比分析。实验结果表明,与ds、cs方法相比,tgba方法生成的tss能够覆盖全部同步对;当满足apsc时,与ps方法相比,tgba方法测试生成所需要的状态数、迁移数至少减少了19889和44352,并且生成效率平均提升了1.95倍,因此tgba方法能够降低状态空间的规模开销,提高tss的生成效率。