NUVA: Architectural support for runtime verification of parametric specifications over multicores
NUVA: Architectural support for runtime verification of parametric specifications over multicores
复制标题
NUVA：对多核参数规范运行时验证的架构支持
DOI：
10.1109/cases.2015.7324554
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
W. Elsharkasy
中科院分区：
文献类型：
--
作者：
Ahmed Nassar;F. Kurdahi;W. Elsharkasy
软件验证（RV）最近出现作为一种补充技术，以扩大传统的软件验证方法的覆盖范围。为了解决纯软件RV框架的实质性性能和功耗开销，本文介绍了NUVA，这代表非均匀验证架构，一个分布式自动机为基础的RV架构参数规格的形式参数化有限状态自动机，与一个案例研究的高速缓存一致性非均匀内存访问（ccNUMA）多处理器。NUVA的核心是一个一致的分布式自动机事务存储器（ATM），有效地维护状态的动态人口的自动机检查器组织成一个有根的动态有向无环图（DAG）之间的所有处理器节点并发共享。ccNUMA多处理器的周期精确模型证实，性能下降1~3%，NoC消息流量增加10~15%，参数事件密度1为0.025 EPI的两个计算密集型的科学基准具有不规则的并发数据结构。详细的架构和实现指标，在台积电40纳米CMOS工艺。NUVA可以被设计为在250 MHz的工作频率下，对于四核多处理器芯片，平均总功率开销小于140 mW，面积开销为4 mm 2。据估计，当与英特尔1.6~3.2GHz的高端台式机和移动的四核处理器集成时，它也会产生1.9~2.6%的面积开销和0.5~1%的功耗开销。我们的硅实现实现了1.5 MEPS/mW的平均性能2。对于具有5 MIPS/mW的处理器核心，这对应于在0.01 EPI的参数事件密度下能量效率下降3.2%。
Runtime Verification (RV) has recently emerged as a complementary technology to extend coverage of conventional software verification methods. To address the substantial performance and power overhead of pure software RV frameworks, this paper introduces NUVA, which stands for nonuniform verification architecture, a distributed automata-based RV architecture for parametric specifications in the form of parameterized finite-state automata, with a case study over a cache-coherent nonuniform-memory-access (ccNUMA) multiprocessor. The core of NUVA is a coherent distributed automata transactional memory (ATM) that efficiently maintains states of a dynamic population of automata checkers organized into a rooted dynamic directed acyclic graph (DAG) concurrently shared among all processor nodes. A cycle-accurate model of a ccNUMA multiprocessor confirms that performance slowdown is 1~3% and NoC message traffic increases by 10~15% at parametric event density1 of 0.025 EPI for two compute-intensive scientific benchmarks having irregular concurrent data structures. The detailed architecture and implementation metrics in TSMC 40nm CMOS technology are presented. NUVA can be dimensioned to incur average total power overhead of less than 140mW and area overhead of 4mm2 for a quad-core multiprocessor chip, at operating frequency of 250MHz. It is also estimated to incur 1.9~2.6% area overhead and 0.5~1% power overhead when integrated with Intel's family of high-end desktop and mobile quad-core processors operating at 1.6~3.2GHz. Our silicon implementation achieves average performance2 of 1.5 MEPS/mW. For a processor core with 5 MIPS/mW, this corresponds to a 3.2% drop in energy efficiency at parametric event density of 0.01 EPI.