论文标题
关于弱记忆模型中有关事件结构（扩展版本）的承诺的推理
Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version)
论文作者
论文摘要
诸如ARMV8和RISC-V之类的现代处理器允许执行过程，其中可以重新排序一个过程中的独立指令。为了应对这种现象，已经开发出所谓的有前途的语义，这允许线程读取尚未编写的值。每个诺言都是投机性更新，后来通过实际写作验证（实现）。有前途的语义是运行的，为开发证明计算的途径提供了途径。在本文中，我们开发了不正确的逻辑，从而为有关状态可及性的推理提供了一个框架。像错误的逻辑一样，我们的断言不足，因为在执行开始时，所有有效承诺的集合都不知道。我们的逻辑将事件结构用作断言，以压缩承诺和实现写作等事件之间的顺序。我们证明了证明计算的合理性和完整性，并通过证明标准弱记忆仪式测试的可及性能来证明其适用性。
Modern processors such as ARMv8 and RISC-V allow executions in which independent instructions within a process may be reordered. To cope with such phenomena, so called promising semantics have been developed, which permit threads to read values that have not yet been written. Each promise is a speculative update that is later validated (fulfilled) by an actual write. Promising semantics are operational, providing a pathway for developing proof calculi. In this paper, we develop an incorrectness-style logic, resulting in a framework for reasoning about state reachability. Like incorrectness logic, our assertions are underapproximating, since the set of all valid promises are not known at the start of execution. Our logic uses event structures as assertions to compactly represent the ordering among events such as promised and fulfilled writes. We prove soundness and completeness of our proof calculus and demonstrate its applicability by proving reachability properties of standard weak memory litmus tests.
