一句话：将弱内存模型元理论问题归约为正则语言包含，并自动生成一致性检查，集成到 GenMC。
公理弱内存模型的元理论问题（如编译映射与局部程序变换的正确性）通常依赖冗长的人工证明。本文提出 Kater，把这类问题归约为更基本的“两个内存模型孰弱”问题；对一大类公理内存模型，进一步归约为正则语言包含问题，从而可判定。另一方面，执行图相对于给定内存模型的一致性检查通常需手工实现。Kater 可为这类模型自动导出高效检查，并将增量一致性检查集成到并发程序模型检测器 GenMC，得到首个以公理内存模型为输入参数、在时间和空间上高效的 bounded verifier。
The metatheory of axiomatic weak memory models covers questions like the correctness of compilation mappings from one model to another and the correctness of local program transformations according to a given model---topics usually requiring lengthy human investigation. We show that these questions can be solved by answering a more basic question: "Given two memory models, is one weaker than the other?" Moreover, for a wide class of axiomatic memory models, we show that this basic question can be reduced to a language inclusion problem between regular languages, which is decidable. Similarly, implementing an efficient check for whether an execution graph is consistent according to a given memory model has required non-trivial manual effort. Again, we show that such efficient checks can be derived automatically for a wide class of axiomatic memory models, and that incremental consistency checks can be incorporated in GenMC, a state-of-the-art model checker for concurrent programs. As a result, we get the first time- and space-efficient bounded verifier taking the axiomatic memory model as an input parameter.
@article{paperbot2092,
title = {Kater: Automating Weak Memory Model Metatheory and Consistency Checking},
author = {Michalis Kokologiannakis and Ori Lahav and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571212}
}