Program Regularization in Memory Consistency Verification
Program Regularization in Memory Consistency Verification
复制标题
DOI：
10.1109/tpds.2012.44
复制
发表时间：
2012-11
影响因子：
5.3
通讯作者：
Yunji Chen;Lei Li;Tianshi Chen;Ling Li;Lei Wang;Xiaoxue Feng;Weiwu Hu
中科院分区：
文献类型：
--
作者：
Yunji Chen;Lei Li;Tianshi Chen;Ling Li;Lei Wang;Xiaoxue Feng;Weiwu Hu
片上多处理器（CMP）存储器子系统的验证方法是根据给定的存储器一致性模型验证并行测试程序在CMP上的执行情况，这在理论和实践上都是一种非常耗时的方法。为了加速存储器一致性验证，先前的方法必须承担可用性的成本（例如，依赖于许多商品CMP没有提供的专用硬件支持）或完整性（例如，缺少一些bug）。同时，并行程序对内存一致性验证的影响或多或少被忽视了。一个证据是，很少有研究一直致力于寻找合适的测试程序，使更有效的验证从测试程序的一个新的角度，我们设计了一个实用的技术称为“程序正则化”，它可以有效地减少内存一致性验证的计算时间。程序正则化背后的关键直觉是，任何并行程序，如果被适当地改造，都可以实现有效的内存一致性验证。更具体地，对于原始程序，程序正则化引入一些辅助存储器地址，并且周期性地将访问这些地址的加载/存储操作插入到原始程序。利用正则化程序，当处理器数目固定时，可以在线性时间内（相对于存储器操作的数目）完成存储器一致性验证。实验结果表明，程序正则化可以显著提高内存一致性验证的速度。最后，我们的技术，它不依赖于具体的验证算法或专用的硬件支持，可以顺利地集成到现有的预硅/硅后验证平台的工业CMP，以加快存储器一致性验证。
A widely adopted methodology for verifying the memory subsystem of a Chip Multiprocessor (CMP) is to verify executions of parallel test programs on the CMP against the given memory consistency model, which has been long known to be time consuming in both theory and practice. To accelerate memory consistency verification, previous approaches have to bear the cost of availability (e.g., relying on dedicated hardware supports that have not been offered by many commodity CMPs) or completeness (e.g., missing some bugs). In the meantime, the impact of parallel programs on memory consistency verification has more or less been overlooked. One piece of evidence is that few investigations have been dedicated to finding appropriate test programs enabling more efficient verification From a novel perspective of test program, we devise a practical technique called “program regularization,” which can effectively reduce the computation time of memory consistency verification. The key intuition behind program regularization is that any parallel program, if being reformed appropriately, can enable efficient memory consistency verification. More specifically, for an original program, program regularization introduces some auxiliary memory addresses, and periodically inserts load/store operations accessing these addresses to the original program. With the regularized program, memory consistency verification can be accomplished in linear time (with respect to the number of memory operations) when the number of processors is fixed. Experimental results show that program regularization can significantly accelerate memory consistency verification. Last but not least, our technique, which does not rely on concrete verification algorithm or dedicated hardware support, can be smoothly integrated into existing presilicon/postsilicon verification platforms of industrial CMPs to speed up memory consistency verification.