Concurrent matching logic

TL;DR

This paper introduces concurrent matching logic (CML), extending matching logic to reason about concurrent programs with shared memory, providing a soundness proof and connecting it to concurrent separation logic.

Contribution

The paper presents a novel concurrent matching logic framework and demonstrates its soundness, bridging it with existing concurrent separation logic under certain conditions.

Findings

CML can reason about fault-free partial correctness of concurrent programs.

A soundness proof of CML in terms of operational semantics is provided.

CSL assertions can be transformed into CML assertions, linking the two logics.

Abstract

Abstract. Matching logic cannot handle concurrency. We introduce concurrent matching logic (CML) to reason about fault-free partial correctness of shared-memory concurrent programs. We also present a soundness proof for concurrent matching logic (CML) in terms of operational semantics. Under certain assumptions, the assertion of CSL can be transformed into the assertion of CML. Hence, CSL can be seen as an instance of CML.