IRP/DSM技术在河南油田电网中的应用

介绍了河南油田实施IRP/DSM技术的具体措施和经验,河南油田实施IRP/DSM技术后,全面提高了机采效率,降低了电力系统综合网损和用电单耗,降低了生产成本和电力工程的建设投资,取得了显著的经济效益。     

面向RISC-V的汇编程序语义等价性自动化测试系统

本文设计并实现了一套面向RISC-V的汇编程序语义等价性自动化测试系统.在面向RISC-V开发软件时,尤其是基于扩展指令(例如向量指令)编写高效的程序时,很难避免以手写汇编的方式编写代码.例如,为标准的C函数库编写相应的向量版函数.与编译器自动生成的代码不同,手写的汇编代码虽然可以最大限度地提高程序的效率,但因绕过了编译时对程序的约束(如类型检查、寄存器分配等)而对开发者提出了更高的要求.能否对新版本与标准版本的汇编程序进行快速地、自动化的语义等价性测试,将大大影响代码的正确性和软件开发和调试的效率.已有面向RISC-V的测试框架缺乏对语义等价性测试的支持,也未考虑程序执行带来的副作用.本研究基于模拟器的动态测试环境,设计并实现了一套面向RISC-V的汇编程序语义等价性自动化测试系统.系统通过跟踪机器状态,捕获程序执行的副作用,并结合用户定义的测试目标生成测试报告.实验表明,本系统相比已有的测试系统,能够有效地对RISC-V汇编程序的语义等价性进行测试.     

连铸中加稀土改善钢质量的探讨

为探讨稀土在连铸过程中的加入方法及其对改善钢质量的影响,在首钢试验厂双流123×123mm~2弧形连铸机上,在保护性气氛下向结晶器内喂入混合稀土金属丝,并进行加稀土与不加稀土的对比试验。结果表明,试验条件下、稀土在钢中收得率可达80％以上、分布比较均匀;铸坯凝固组织致密,内裂敏感性大大减轻;加稀土钢比较干净;钢中常规夹杂物大部分被细小而又不易变形的稀土夹杂物取代、故使钢材横向冲击值显著提高。     

面向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架构的主流模拟器QEMU和Spike均具有指令追踪功能, 但其时间和空间开销过大, 在应对规模较大的应用时效率低下. 本文提出了一种基于QEMU的指令追踪技术, 将程序中的基本块、控制流图等静态信息与分支选择等动态信息解耦, 在保证指令序列不失真的同时高效追踪执行序列. 相比QEMU原生实现的指令追踪, 本文提出的指令追踪技术的时间开销平均降低了80%以上, 空间开销平均降低了95%以上. 此外, 本文面向RISC-V架构, 实现了多种场景下的指令序列离线分析, 包括指令分类统计、程序热点标记、行为模式分析等.     

基于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内存一致性测试进行自动化分析。     

离心泵叶片修补技术应用分析

河南油田水电厂双河大口井水源泵站单泵运行时存在扬程富裕、单耗高的问题,通过对离心泵叶轮车削和用铸铁修补剂修补叶片改变叶片型线、叶片出口角等途径改善泵的运行特性。实施后检测结果表明,在不改变电机、泵体和管道、且满足供水需要的前提下,水泵电耗下降了28％,节能效果显著。