在多重中断C程序中,中断嵌套可能会导致一些非期望的交叠执行,从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题,对多重中断C程序的运行时语义进行建模,根据共享变量的访问给出了一种...在多重中断C程序中,中断嵌套可能会导致一些非期望的交叠执行,从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题,对多重中断C程序的运行时语义进行建模,根据共享变量的访问给出了一种原子性的定义,提出了相应的数据竞争及原子性检测方法,并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后,设计并实现了一个数据竞争及原子性检测原型工具MIDAC(multiple interruption C program data race and atomicity checker),实验结果表明,该工具能够针对一定规模的实际程序得到很好的检测效果。展开更多
文摘在多重中断C程序中,中断嵌套可能会导致一些非期望的交叠执行,从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题,对多重中断C程序的运行时语义进行建模,根据共享变量的访问给出了一种原子性的定义,提出了相应的数据竞争及原子性检测方法,并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后,设计并实现了一个数据竞争及原子性检测原型工具MIDAC(multiple interruption C program data race and atomicity checker),实验结果表明,该工具能够针对一定规模的实际程序得到很好的检测效果。