论文部分内容阅读
在多重中断C程序中，中断嵌套可能会导致一些非期望的交叠执行，从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题，对多重中断c程序的运行时语义进行建模，根据共享变量的访问给出了一种原子性的定义，提出了相应的数据竞争及原子性检测方法，并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后，设计并实现了一个数据竞争及原子性检测原型工具MIDAC（multiple interruption C program data race and atomicity che