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

Formal Description and Proof of Corollaries for RVWMOLoad Value Axiom in Coq

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

The RISC-V Weak Memory Ordering(RVWMO)specifies the memory access sequencing constraints in RISC-V multi-core systems,aiming to provide hardware designers with flexibility while ensuring software ease of development.It is an important specification that RISC-V software and hardware designers must follow.The RISC-V Instruction Set Manual describes RVWMO using global memory order,preserved program order,and three axioms(load value axiom,atomicity axiom,and progress axiom).By using the rules of RVWMO,the legality of the memory access sequence in multi-threaded programs can be determined,which can guide chip design,verification,and software development.Among these rules,the load value axiom is one of the most complex and difficult rules to apply,and it is an important basis for determining the legality of multiple typical case validity judgments.However,the manual s description and case explanations of this axiom are mainly based on natural language and lack clear and rigorous formal descriptions and reasoning processes,thus making it difficult for readers to understand and apply the axiom.In light of this,this research makes a formal description of the RVWMO load value axiom and proofs of relevant lemmas,theorems,and consequences using the interactive theorem proving tool Coq,which is of great significance for understanding and applying the load value axiom of RVWMO,and determining the legality of memory access sequences.