串行化顺序组合、流水线和硬件弱内存模型
Parallelized sequential composition, pipelines, and hardware weak memory models
摘要：
自从1965年CDC 6600及其“记分板”技术的引入以来，处理器已经（不一定）按程序顺序执行指令。高级代码的程序员可以以任意顺序对独立指令进行排序，并且重要的编程抽象和计算效率的问题是，可以依赖处理器来对低级指令进行合理的并行化/重新排序，以利用例如，多个ALU。在架构级别，这样的重新排序通常经由每处理器流水线来实现，指令被按顺序提取到流水线中，但是取决于本地考虑，可能乱序提交，只要任何重新排序从该处理器的角度保留顺序语义。然而，多核架构，其中多个管道并行运行，可以暴露这些处理器级的重新排序作为意外的，或“弱”的行为。这种弱行为很难推理，并且（通过投机执行）至少是一类广泛存在的安全漏洞的基础。在本文中，我们介绍了一种新的程序操作符，\emph{parallelized sequential composition}，它可以实例化的功能，控制原子指令的重新排序。它概括了顺序和并行组合，并且当适当地实例化时，表现出许多众所周知的硬件弱内存模型的弱行为。我们的框架允许应用已建立的合成技术（如。Owicki-Gries）用于弱行为的推理，并且便于从文献中抽象表达属性。的语义和理论的编码和验证定理证明，我们给出了一个实现的流水线语义，我们用它来经验性地显示对ARM和RISC-V的既定模型的一致性。
英文摘要：
Since the introduction of the CDC 6600 in 1965 and its `scoreboarding' technique processors have not (necessarily) executed instructions in program order. Programmers of high-level code may sequence independent instructions in arbitrary order, and it is a matter of significant programming abstraction and computational efficiency that the processor can be relied upon to make sensible parallelizations/reorderings of low-level instructions to take advantage of, eg., multiple ALUs. At the architectural level such reordering is typically implemented via a per-processor pipeline, into which instructions are fetched in order, but possibly committed out of order depending on local considerations, provided any reordering preserves sequential semantics from that processor's perspective. However multicore architectures, where several pipelines run in parallel, can expose these processor-level reorderings as unexpected, or `weak', behaviours. Such weak behaviours are hard to reason about, and (via speculative execution) underlie at least one class of widespread security vulnerability. In this paper we introduce a novel program operator, \emph{parallelized sequential composition}, which can be instantiated with a function that controls the reordering of atomic instructions. It generalises both sequential and parallel composition, and when appropriately instantiated exhibits many of the weak behaviours of well-known hardware weak memory models. Our framework admits the application of established compositional techniques (eg. Owicki-Gries) for reasoning about weak behaviours, and is convenient for abstractly expressing properties from the literature. The semantics and theory is encoded and verified in a theorem prover, and we give an implementation of the pipeline semantics which we use to empirically show conformance against established models of ARM and RISC-V.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
