TransForm：形式化规约内存一致性模型并合成增强型 Litmus 测试
摘要
内存一致性模型（MCMs）规定了并行程序中共享内存访问的合法顺序与可见性。传统上，指令集架构（ISA）的 MCMs 假设相关的程序可见内存排序行为仅由用户级程序指令之间的共享内存交互产生。这一假设未考虑虚拟内存（VM）实现可能导致的额外共享内存交互，这些交互发生在用户级程序指令与以下两者之间：1）系统级操作（例如由系统调用发起的地址重映射和转译后备缓冲器失效）以及 2）硬件级操作（例如硬件页表遍历和脏位更新），且发生于用户级程序执行期间。这些额外的共享内存交互会影响用户级程序可观测的内存排序行为。因此，内存转滞模型（MTMs）作为 MCMs 的超集被提出，以额外阐明感知虚拟内存的一致性规则。然而，此前尚无工作支持形式化 MTM 规约，亦无支持其自动化分析的方法。为填补上述空白，本文提出 TransForm 框架。首先，TransForm 具备用于形式化规约 MTMs 的公理化词汇。其次，TransForm 包含一个合成引擎，当提供 TransForm MTM 规约时，支持自动生成带有 MTM 特性（即增强型 litmus 测试，或 ELTs）的 litmus 测试。作为一个案例研究，我们基于先前工作对 Intel x86 MTM 实现的 ELT 评估以及可用公开文档的观察，正式定义了 Intel x86 处理器的一种估计 MTM，称为 x86t_elt。给定 x86t_elt 和合成边界作为输入，TransForm 的合成引擎成功生成了一组 ELTs，其中包括先前工作中的相关 ELTs。
引用
@article{arxiv.2008.03578,
title = {TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests},
author = {Naorin Hossain and Caroline Trippel and Margaret Martonosi},
journal= {arXiv preprint arXiv:2008.03578},
year = {2020}
}
备注
*This is an updated version of the TransForm paper that features updated results reflecting performance optimizations and software bug fixes. 14 pages, 11 figures, Proceedings of the 47th Annual International Symposium on Computer Architecture (ISCA)