Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Owicki--Gries Logic for Timestamp Semantics

Tatsuya Abe

TL;DR

The paper addresses the challenge of verifying concurrent programs under weak memory models that permit delays in store instructions. It introduces timestamp semantics with vector clocks and an observation-based non-interference framework to extend Owicki–Gries reasoning to weak memory. The main contributions are threefold: (1) ensuring load-assignment soundness via non-interference, (2) updating vector clocks by substituting thread identifiers, and (3) introducing timestamp variables to broaden the assertion language and constrain interference. This work provides a theoretically grounded foundation for reasoning about concurrency on modern architectures and sets directions for future work toward completeness and compositionality, including extending to load buffering and promises.

Abstract

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.

Owicki--Gries Logic for Timestamp Semantics

TL;DR

The paper addresses the challenge of verifying concurrent programs under weak memory models that permit delays in store instructions. It introduces timestamp semantics with vector clocks and an observation-based non-interference framework to extend Owicki–Gries reasoning to weak memory. The main contributions are threefold: (1) ensuring load-assignment soundness via non-interference, (2) updating vector clocks by substituting thread identifiers, and (3) introducing timestamp variables to broaden the assertion language and constrain interference. This work provides a theoretically grounded foundation for reasoning about concurrency on modern architectures and sets directions for future work toward completeness and compositionality, including extending to load buffering and promises.

Abstract

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.

Paper Structure

This paper contains 8 sections, 2 theorems, 21 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Owicki--Gries Logic
  3. Timestamp Semantics
  4. Observation-Based Logic
  5. Formal system
  6. Non-observation-interference
  7. Related Work and Discussion
  8. Conclusion and Future Work

Key Result

Theorem 1

$\vdash \varphi \: \{\mathord{s_0 \parallel \cdots \parallel s_{N-1}}\} \: \psi$ implies $\vDash \varphi \: \{\mathord{s_0 \parallel \cdots \parallel s_{N-1}}\} \: \psi$.

Figures (7)

  • Figure 1: Parallel compositionality by non-interference.
  • Figure 2: Derivation of Coherence on non-interference.
  • Figure 3: Derivation of One-Two on non-interference.
  • Figure 4: Derivation of One-One on non-interference.
  • Figure 5: Derivation of Store Buffering on non-interference.
  • ...and 2 more figures

Theorems & Definitions (2)

  • Theorem 1: Owicki1976A
  • Theorem 2