This paper combines rely/guarantee, abstract patterns and matching logic to reason about concurrent programs in a modular and compositional manner. According to the separation property, the state can be divided into two disjoint parts, the local state and the shared state. We use matching logic to deal with the local state, and use rely/guarantee and abstract patterns to deal with the shared state. The power of rely/guarantee is to describe interference between concurrent programs. The advantage of abstract patterns is supporting fictional separation, which indicates that we logically consider abstract patterns to represent disjoint elements, although these elements are not disjoint under a certain implementation. By combining the advantages of rely/guarantee, abstract patterns and matching logic, our approach realize that clients of the module can be verified completely according to the specification of the module, regardless of the implementation of the module. In addition, we use several examples to illustrate our approach, define our logic judgments, and prove the soundness of our logic.

We combine “ownership transfer” with matching logic to reason about fault-free partial correctness of shared-memory concurrent programs. As we all know, what really gives separation logic (concurrent separation logic) an edge is the ownership transfer of the heap. Inspired by this, we use matching logic to realize variable ownership (permission) and its transfer mechanism, which reveals the hidden principle behind “protected variables” of resource and “rely set” in extended CSL. In addition, variable ownership can replace Dijkstra’s semaphore blocking technique to achieve the critical section. Soundness is important to us, we provide a semantic model that supports the separation property and demonstrate the soundness of our logic based on trace semantics.