TransForm：正式发布瞬态模型和合成增强的石蕊试验
TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests
摘要：
内存一致性模型（MCMs）规定了并行程序中共享内存访问的合法顺序和可见性。传统上，指令集架构（ISA）MCM假设相关的程序可见内存排序行为仅由用户级程序指令之间发生的共享内存交互引起。该假设未能考虑虚拟存储器（VM）实现，其可能导致用户级程序指令与以下两者之间的附加共享存储器交互：1）系统级操作（例如，由系统调用发起的地址重映射和转换后备缓冲器无效）和2）硬件级操作（例如，硬件页表遍历和脏位更新）。这些额外的共享内存交互会影响用户级程序的可观察内存排序行为。因此，内存瞬态模型（MTM）已被创造作为一个超集的MCM，另外阐明虚拟机感知的一致性规则。然而，没有以前的工作已经启用正式的MTM规范，也没有方法来支持其自动化分析。为了填补上述空白，本文提出了TransForm框架。首先，TransForm提供了一个公理词汇表，用于正式指定MTM。其次，TransForm包括一个合成引擎，用于支持自动生成用MTM功能增强的石蕊测试（即，增强型石蕊试验（ELT）。作为案例研究，我们正式定义了英特尔x86处理器的估计MTM（称为x86t_elt），该MTM是基于对英特尔x86 MTM实施进行的基于ELT的评估所得出的观察结果，这些评估来自先前的工作和可用的公共文档。给定x86t_elt和合成边界作为输入，TransForm的合成引擎成功地产生了一组ELT，包括来自先前工作的相关ELT。
英文摘要：
Memory consistency models (MCMs) specify the legal ordering and visibility of shared memory accesses in a parallel program. Traditionally, instruction set architecture (ISA) MCMs assume that relevant program-visible memory ordering behaviors only result from shared memory interactions that take place between user-level program instructions. This assumption fails to account for virtual memory (VM) implementations that may result in additional shared memory interactions between user-level program instructions and both 1) system-level operations (e.g., address remappings and translation lookaside buffer invalidations initiated by system calls) and 2) hardware-level operations (e.g., hardware page table walks and dirty bit updates) during a user-level program's execution. These additional shared memory interactions can impact the observable memory ordering behaviors of user-level programs. Thus, memory transistency models (MTMs) have been coined as a superset of MCMs to additionally articulate VM-aware consistency rules. However, no prior work has enabled formal MTM specifications, nor methods to support their automated analysis. To fill the above gap, this paper presents the TransForm framework. First, TransForm features an axiomatic vocabulary for formally specifying MTMs. Second, TransForm includes a synthesis engine to support the automated generation of litmus tests enhanced with MTM features (i.e., enhanced litmus tests, or ELTs) when supplied with a TransForm MTM specification. As a case study, we formally define an estimated MTM for Intel x86 processors, called x86t_elt, that is based on observations made by an ELT-based evaluation of an Intel x86 MTM implementation from prior work and available public documentation. Given x86t_elt and a synthesis bound as input, TransForm's synthesis engine successfully produces a set of ELTs including relevant ELTs from prior work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
