プログラミング言語とツールラボ

IMM: Compilation Correctness for Relaxed Memory Models

IMM フレームワークは、プログラミング言語メモリモデル (Promising や Weakestmo など) から、ハードウェアメモリモデル (x86、Power、Arm、および RISC-V など) へのコンパイルの正当性の証明を単純化します。フレームワークは Coq で機械化されています。

弱いメモリ一貫性セマンティクスを使用した並行プログラミング言語から、POWER や ARM などの主流マルチコアアーキテクチャへコンパイルする正当性の証明をモジュール化する 1 つの方法として、中程度に弱いメモリモデル (IMM) を開発しています。IMM を使用して、複数の新しいプログラミング言語のメモリモデル (主にどこからともなくあらわれる問題の修正を目的としているもの) から POWER、ARMv7、ARMv8、RISC-V、x86-TSO などのハードウェアメモリモデルにコンパイルする正当性を証明します。結果は Coq で機械化され、私たちの知る限りでは、これらは x86-TSO より弱いモデルに対して初めて機械検証したコンパイルの正当性の結果です。