Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

TL;DR

This paper introduces a novel past-time temporal epistemic logic for reasoning about shared-memory concurrency, enabling explicit verification of correctness properties based on local thread knowledge and histories.

Contribution

It presents a new logic with semantics and proof system for verifying concurrent algorithms using local histories and epistemic reasoning, demonstrated on Peterson's mutual exclusion algorithm.

Findings

Logic successfully models thread knowledge in concurrent executions

Proves mutual exclusion property via local knowledge conditions

Provides a sound proof system for the logic

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.