Whereas an extension with non-interference of Hoare logic for sequential programs Owicki--Gries logic ensures the correctness of concurrent programs on strict consistency, it is unsound to weak memory models adopted by modern computer architectures and specifications of programming languages. This paper proposes a novel non-interference notion and provides concurrent program logic sound to timestamp semantics corresponding to a weak memory model that allows delays in the effects of store instructions. This paper reports three theoretically interesting techniques for modifying non-interference to support delays in the effects of store instructions. The techniques contribute to a better understanding of constructing concurrent program logic.

翻译：尽管针对顺序程序的Hoare逻辑在非干扰性方面的扩展——Owicki-Gries逻辑能够确保并发程序在严格一致性下的正确性，但其对现代计算机体系结构和编程语言规范所采用的弱内存模型并不具备可靠性。本文提出了一种新颖的非干扰性概念，并构建了一种对时间戳语义可靠的并发程序逻辑，该语义对应于允许存储指令效果延迟的弱内存模型。本文报告了三种在理论上具有重要意义的修改非干扰性以支持存储指令效果延迟的技术。这些技术有助于更好地理解并发程序逻辑的构建方法。