基于视图的公理推理用于 PSO（扩展版）

弱内存模型描述了现代多核架构上并发程序的语义。针对并发程序的推理技术，如 Owicki-Gries 风格的证明演算，必须建立在此类语义之上，因此需要为每一种新内存模型重新开发。近来，一种更统一的推理方法被提出，该方法基于若干核心公理构建正确性证明。这使得程序正确性的证明可以独立于内存模型，并通过证明特定内存模型实例化证明所需的所有公理，将证明迁移到该模型。该公理体系以线程视图（thread views）作为语义中的一等元素。本文中，我们研究这种公理推理形式对部分存储序（Partial Store Order, PSO）内存模型的适用性。由于 PSO 的标准语义并非基于视图，我们首先给出 PSO 的基于视图的语义，并证明其与原标准语义一致。接着我们表明，新的基于视图的语义满足除一条公理外的所有公理。缺失的公理涉及内存模型的消息传递（message-passing, MP）能力，而 PSO 不保证该能力。因此，只有不使用 MP 公理的证明才可迁移至 PSO。我们通过证明一个采用栅栏（fence）以确保消息传递的立沸测试（litmus test）的正确性，来阐释该推理技术。