编程语言和工具实验室

IMM: Compilation Correctness for Relaxed Memory Models

IMM 框架简化了从编程语言内存模型（如 Promising 和 Weakestmo）到硬件内存模型（x86、Power、Arm、RISC-V）的编译的正确性证明。该框架在 Coq 中被机械化。

我们正在开发一个中间的弱内存模型，IMM，作为将从具有弱内存一致性语义的并发编程语言到主流多核架构（如 POWER 和 ARM）的编译的正确性证明模块化的一种方式。我们使用 IMM 来证明从多种新的编程语言内存模型（主要是旨在解决凭空产生的问题）到硬件内存模型（如 POWER、ARMv7、ARMv8、RISC-V 和 x86-TSO）的编译的正确性。我们的结果在 Coq 中进行了机械化处理，据我们所知，这是第一个针对弱于 x86-TSO 的模型进行机器验证的编译正确性结果。