Formal Description and Proof of Corollaries for RVWMO Load Value Axiom in Coq
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 im-portant 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 pro-gress axiom).By using the rules of RVWMO,the legality of the memory access sequence in multi-threaded programs can be de-termined,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 ap-ply 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 under-standing and applying the load value axiom of RVWMO,and determining the legality of memory access sequences.
NETL
NSTL
万方数据
