Compositional Concurrent Program Logic for Timestamp Semantics Compositional Concurrent Program Logic for Timestamp Semantics

Tatsuya Abe. Compositional Concurrent Program Logic for Timestamp Semantics. JSSST Computer Software, 43(3):24–36, 2026.

Parallel executions of instructions are taken for granted on modern computer architectures, so the delayed effects of store instructions must be considered. Such delays are formally captured by timestamp semantics. The author previously constructed Owicki–Gries style logic for timestamp semantics; however, it inherits the well-known non-compositionality problem of Owicki–Gries logic. In this paper, we address the non-compositional problem by presenting Jones style compositional logic based on the rely/guarantee notion. A key idea is to express an observation (of an effect) performed by a load instruction as a delay of the effect caused by the store instruction in the rely/guarantee system. Our compositional logic is not specific to a weak memory model, and we keep the assertion language simple. Consequently, it serves as a foundation for logics for timestamp semantics.