面向RISC-V内存一致性测试的自动化分析方法

An Automated Analysis Approach for RISC-V Memory Consistency Testing

开源架构RISC-V定义了其内存一致性模型RVWMO,作为多核RISC-V系统软硬件设计开发的重要规范.在多核芯片的验证阶段,需要对芯片的内存一致性进行严格全面的测试.测试通常针对某一访存顺序模式,选取典型的并行程序片段进行大规模测试(又称Litmus测试),通过程序运行的最终状态推测芯片内存一致性模型.通常,更为宽松的内存一致性会导致更多的程序状态.分析Litmus测试结果对于验证芯片的RVWMO兼容性、探索多核系统的内存一致性优化的可能性具有重要意义.以RVWMO规范下允许的程序状态为基准,芯片实测得到更多的程序状态表明其存在兼容性问题,得到更少的程序状态表明其仍具有优化空间.面对规模庞大、行为复杂的Litmus测试,如何对其测试结果进行自动化分析是亟待解决的问题.本文对Litmus测试的原理和输出结果进行了深入分析,提出一种面向RISC-V内存一致性测试的自动化分析方法,采用形式化方法对Litmus测试进行基于RVWMO规范的模拟运行,并通过与芯片的实测结果进行对比分析给出测试结论.本方法基于Hifive Unmatched开发板开展测试.实验表明,本文提出的方法可快速、有效地对RISC-V内存一致性测试进行自动化分析.

The open-source architecture RISC-V has defined its memory consistency model RVWMO as an important specification for the software and hardware design and development of multi-core RISC-V systems.During the verification phase of multi-core chips,strict and comprehensive testing of the memory consistency of the chip is indispensable.Testing usually focuses on a specific memory access order and selects typical parallel program segments for large-scale testing(also known as Litmus testing)to deduce the memory consistency model of the chip based on the final state of the program execution.Analysis of Litmus test results is important for verifying the compatibility of the chip's RVWMO and exploring the possibility of memory consistency optimization in multi-core systems.Based on the program states allowed by the RVWMO specification,more program states are observed in chip testing,which indicates the existence of compatibility,while fewer program states observed may indicate the potential of optimization.In the face of the large-scale and complex behavior of Litmus testing,how to automate the analysis of its test results is an urgent problem to be solved.This study made a deep analysis of the principle and output results of Litmus testing and proposed an automated analysis approach for RISC-V memory consistency testing,which used formal methods to simulate Litmus testing based on the RVWMO specification,and drew conclusions by comparing the results with the measured data of the chip.This approach was tested on the Hifive Unmatched board.The experiment shows that the approach can effectively and quickly perform automated analysis of RISC-V memory consistency testing.