AI 中文总结
研究针对顺序弱内存ISA的乱序多处理器验证问题，核心方法是设计核心规范并分两步证明，主要贡献是首次实现此类形式验证，借助核心规范简化证明，且利用LLM代理自动编写证明。
AI 中文摘要
乱序多处理器是现代硬件的关键部分，其验证面临核心间交织（读写到达共享内存的顺序不受限制）和核心内乱序执行（指令以非程序顺序发出）的挑战，两者结合产生弱结果，现代ISA允许此类行为。微架构还存在过度乱序执行，虽然后续会丢弃，但在全系统验证中使核心推理复杂化。先前工作未对有此类弱结果的乱序多处理器进行无界验证。本文首次针对顺序弱内存ISA对乱序多处理器进行形式验证。关键思想是精心设计的核心规范，将过度执行的本质捕获在单个指令列表中。在此基础上，将证明分解为两步：一是核心精化，证明核心实现符合该规范，抽象掉除过度执行和核心接口所需的微架构状态；二是系统包含，将乱序内存执行和核心间交织序列化到ISA中，借助核心规范轻松消除过度执行。所有证明都在Rocq中机械化，大量利用大语言模型（LLM）代理自动编写证明。
英文摘要
Out-of-order multiprocessor is a critical piece of modern hardware, and their verification must solve the following challenges. First, inter-core interleaving, in which the order their reads and writes reach shared memory is unrestricted. Second, intra-core out-of-order execution, in which instructions fire out of program order. The combination of the two yields weak outcomes, which no sequential execution explains, and modern ISA allows such behaviors to account for them. However, the microarchitecture even exhibits excess out-of-order executions, temporarily entering states forbidden by the ISA. While discarded later, such states complicate reasoning about the core in full-system verification. Prior works verify a range of processor designs, while none have performed unbounded verification for out-of-order multiprocessor exhibiting such weak outcomes. We present the first formal verification of an out-of-order multiprocessor against an in-order, weak-memory ISA. Our key idea is a well-designed core specification, which captures the essence of excess executions in a single list of instructions. Building upon this, we decompose the proof into two steps. The first is a core refinement, proving a core implementation against this specification, abstracting away every microarchitectural state except those necessary to reason about excess executions and the core interface. The second is a system inclusion, serializing the out-of-order memory executions and inter-core interleaving into the ISA, easily removing excess executions thanks to the core specification. All of our proofs are mechanized in Rocq, heavily utilizing large language model (LLM) agents to write proofs automatically.
