Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

Hamed Nemati, Mads Dam

TL;DR

The paper introduces a past-time temporal epistemic logic with perfect-recall histories to reason about shared-memory concurrency from a thread's local perspective. It develops a formal interleaving semantics, a sound sequent-style proof system, and a concrete instantiation with instrumented reads, enabling local knowledge-based reasoning that yields global safety results. A key contribution is the locality of reasoning via the Prev operator and stability concepts, which together support a rely-guarantee style approach embedded directly in the logic. The Peterson mutual exclusion proof illustrates how local knowledge about a thread's last step, combined with environmental stability, implies global invariants and mutual exclusion; the framework also supports compositional reasoning and model-constraint explanations for relies and guarantees. This approach offers a modular path to correctness proofs in concurrent programs and lays groundwork for automation and integration with existing rely-guarantee and separation-logic techniques.

Abstract

Shared-memory concurrency is difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments for classic algorithms are epistemic: a thread enters a critical region only when, from its local view, it can rule out that another thread is concurrently in that region. We make such arguments explicit by introducing a past-time temporal epistemic logic interpreted over interleaving executions with perfect-recall local histories. Past-time operators support "since" reasoning, while epistemic modalities capture what a given thread can conclude from its own observation history. We give semantics and a sound proof system, instantiate the logic to a simple shared-memory language with instrumented read/write observations, and illustrate the approach on Peterson's mutual exclusion algorithm by proving a local knowledge condition that implies mutual exclusion.

Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

TL;DR

The paper introduces a past-time temporal epistemic logic with perfect-recall histories to reason about shared-memory concurrency from a thread's local perspective. It develops a formal interleaving semantics, a sound sequent-style proof system, and a concrete instantiation with instrumented reads, enabling local knowledge-based reasoning that yields global safety results. A key contribution is the locality of reasoning via the Prev operator and stability concepts, which together support a rely-guarantee style approach embedded directly in the logic. The Peterson mutual exclusion proof illustrates how local knowledge about a thread's last step, combined with environmental stability, implies global invariants and mutual exclusion; the framework also supports compositional reasoning and model-constraint explanations for relies and guarantees. This approach offers a modular path to correctness proofs in concurrent programs and lays groundwork for automation and integration with existing rely-guarantee and separation-logic techniques.

Abstract

Shared-memory concurrency is difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments for classic algorithms are epistemic: a thread enters a critical region only when, from its local view, it can rule out that another thread is concurrently in that region. We make such arguments explicit by introducing a past-time temporal epistemic logic interpreted over interleaving executions with perfect-recall local histories. Past-time operators support "since" reasoning, while epistemic modalities capture what a given thread can conclude from its own observation history. We give semantics and a sound proof system, instantiate the logic to a simple shared-memory language with instrumented read/write observations, and illustrate the approach on Peterson's mutual exclusion algorithm by proving a local knowledge condition that implies mutual exclusion.

Paper Structure

This paper contains 74 sections, 6 theorems, 46 equations.

Table of Contents

  1. Introduction
  2. Motivation and Running Example
  3. Epistemic view of interference.
  4. Last-step facts and stability.
  5. Running example:
  6. Program Model and Observations
  7. States and runs.
  8. Scheduling predicate.
  9. Observations and perfect recall.
  10. Asynchrony and "no global clock".
  11. Past-Time Temporal Epistemic Logic
  12. Syntax
  13. State and transition formulas
  14. Derived operators
  15. Last-step operator
  16. ...and 59 more sections

Key Result

theorem 1

If $\Gamma\vdash \phi$ is derivable, then $\Gamma\models \phi$, i.e., for every model and every point $(\pi,i)$, if $(\pi,i)\models \bigwedge\Gamma$ then $(\pi,i)\models \phi$.

Theorems & Definitions (12)

  • theorem 1: Soundness
  • proof : Proof sketch
  • definition 1: Stability under the environment
  • lemma 1: Closure properties
  • proof : Proof sketch
  • lemma 2: Stability lifting
  • proof : Proof sketch
  • lemma 3: Knowledge persistence between $A$-steps
  • proof : Proof sketch
  • corollary 1: Epistemic stability lifting
  • ...and 2 more