一句话：提出 HMC，面向硬件内存模型的无状态模型检测，支持 load buffering 并兼顾效率与可扩展性。
无状态模型检测（SMC）通过系统探索并发程序的所有执行来验证安全性质。现有工作已将其扩展到 x86-TSO 等硬件内存模型，但对允许 load buffering 行为的模型（如 POWER、ARMv7、ARMv8、RISC-V）支持不足：要么为效率忽略此类行为，要么因额外复杂度而难以扩展。本文提出 HMC，旨在为这类硬件内存模型提供 SMC 支持，在覆盖 load buffering 执行的同时保持效率与可扩展性。摘要未报告具体实验数据。
Stateless Model Checking (SMC) is an effective technique for verifying safety properties of a concurrent program by systematically exploring all of its executions. While SMC has been extended to handle hardware memory models like x86-TSO, it does not adequately support models that allow load buffering behaviours, such as the POWER, ARMv7, ARMv8, and RISC-V models. Existing SMC tools either do not consider such behaviours in the name of efficiency, or do not scale so well due to the extra complexity induced by these behaviours.