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.
翻译:ARMV8 和 RISC-V 等现代处理器允许执行处决,在这种过程中可以重新排序独立指令。为了应对这种现象,已经开发出所谓的有希望的语义学,这样可以让线条读出尚未写成的数值。每个承诺都是投机性的更新,后来通过实际写作加以验证(完成)。有希望的语义学可以运作,为制定证据计算法提供了一条路径。在本文中,我们发展了不正确的逻辑风格,从而形成了关于国家可达性的推理框架。与不正确逻辑一样,我们的说法并不相近,因为所有有效承诺的一套在开始执行时并不知道。我们逻辑使用事件结构作为假设,以缩写形式代表许诺和完成的事件之间的排序。我们证明了我们的证据计算方法的正确性和完整性,并通过证明标准微弱记忆点测试的可达性来证明其适用性来证明其适用性。