面向RISC-V向量算法库的自动化测试方法

RISC-V因其精简、开源、可定制的特点受到学术界和工业界的广泛关注,围绕RISC-V的软件生态也在逐步完善。2021年9月,RISC-V委员会发布了1.0版本的向量指令集规范（RVV）,为面向RISC-V的数据级并行优化提供了标准,且部分算法库（如OpenCV）已有面向RVV的移植工作。算法库的开发移植是基于明确的函数原型和语义规范,通常将具有基础（标量）版本的代码实现作为参考,开发的向量版本算法需要符合规范以保证算法库的兼容性。本文提出了一种面向RVV算法库的自动化测试方法,通过对算法函数原型进行解析生成符合规范的测试数据,将向量算法库的测试结果与参考实现对比分析给出测试结论,从而实现算法库的自动化测试。与传统的自动化测试框架相比,本方法无需手动编写测试用例,也无需提供待测目标的设计规范。实验表明,本方法可快速、有效地对RVV算法库进行测试。     

基于Coq的RVWMO加载值公理形式化描述与推论证明

RISC-V内存一致性模型（RVWMO）规定了RISC-V多核系统的访存序约束,是RISC-V软硬件设计者共同遵守的重要规范,旨在为硬件设计提供灵活性的同时保证软件的易开发性。RISC-V指令集规范使用全局访存序、保留程序序以及三条公理（加载值公理、原子公理与进度保证公理）描述RVWMO。通过运用RVWMO的规则,可对多线程程序的访存序合法性进行判定,进而指导芯片设计、验证与软件开发。其中,加载值公理是最为复杂和难以运用的规则之一,是多个典型案例合法性判定的重要基础。然而,规范对于该公理的描述及案例讲解主要基于自然语言,缺乏清晰严格的形式化描述和推理过程,不利于读者理解和运用该公理。本文基于交互式定理辅助证明工具Coq,给出了RVWMO加载值公理的形式化描述以及相关引理、定理和推论的证明,对于理解运用RVWMO加载值公理和判定访存序的合法性具有重要意义。     

基于QEMU的RISC-V程序性能分析

开源指令集规范RISC-V具有模块化、高可定制的特点,可根据特定应用或需求定制指令集,从而优化性能、节约能耗,提高芯片的应用适配性。为了分析目标场景的需求以优化指令集设计,往往需要基于模拟器深入分析目标应用的特点。为此,本文面向RISC-V,提出了一种基于QEMU模拟器的程序性能分析技术,以动态二进制插桩的方式收集程序的运行信息,并结合调试信息进行基本块级和函数级的热点标注。相比于传统的性能分析技术（如Gprof等）,本技术具有以下优势：一是不受硬件平台和操作系统的限制,适用于早期的指令集设计阶段;二是考虑了模拟器与真实芯片之间执行指令的差异,引入指令预估代价模型对结果进行修正。此外,本文提出的性能分析技术也可用于指导程序性能优化以及编译优化等。     

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

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