Race analysis for SystemC using model checking
Race analysis for SystemC using model checking
复制标题
DOI：
10.1145/1754405.1754406
复制
发表时间：
2010-05
期刊：
影响因子：
--
通讯作者：
Nicolas Blanc;D. Kroening
中科院分区：
文献类型：
--
作者：
Nicolas Blanc;D. Kroening
SystemC是一种系统级建模语言，它提供了广泛的功能来描述不同抽象级别的并发系统。SystemC标准允许模拟器实现确定性的调度策略，这通常隐藏了与并发相关的设计缺陷。我们提出了一种新的编译器SystemC集成了正式的和可扩展的竞争分析。这种分析结合了经典的静态分析和模型检查技术。分析的结果不仅对诊断竞争条件的影响有价值，而且还可以用于显着提高仿真性能。我们的编译器产生一个模拟器，在运行时使用的竞争分析信息进行偏序减少，从而消除上下文切换，不影响模拟的结果。实验结果表明，仿真加速一个数量级，更好。
SystemC is a system-level modeling language that offers a wide range of features to describe concurrent systems at different levels of abstraction. The SystemC standard permits simulators to implement a deterministic scheduling policy, which often hides concurrency-related design flaws. We present a novel compiler for SystemC that integrates a formal and scalable race analysis. This analysis combines both classic static analysis and model checking techniques. The outcome of the analysis is not only valuable to diagnose the effect of race conditions, but can also be used to improve simulation performance dramatically. Our compiler produces a simulator that uses the race analysis information at runtime to perform partial-order reduction, thereby eliminating context switches that do not affect the result of the simulation. Experimental results show simulation speedups of one order of magnitude and better.