在弱一致性模型中线程模块化的静态分析方法

摘要

本文提出一种内存感知情况下,静态程序分析方法.这种方法能够精准的分析并发软件在弱一致性模型下的表现,例如:x86-TSO(标准存储器模型)内存系统,SPARC-PSO(SPARC可扩充处理器架构)(PSO部分存储命令模型),SPARC-ROM(弱一致性存储模型).本文方法的核心是用统一的框架来确定内部线程间的干扰存在的可行性,从而避免虚假数据流在静态分析中的传播,提高静态分析器的性能.制定了检查线程干扰可行性的数据标准,能够高效的解决问题并能很好地适应一系列的硬件级的存储模型.与现在的技术相比,本文的方法可以明显的减少虚假报警和无关的数据产生.对于这种改进的方法,使用了大量的多线程的C语言程序进行评估.实验显示,就系统运行时开销而言,本文的方法显著优于其他技术水平.