From Matching Logic To Parallel Imperative Language Verification

TL;DR

This paper develops a matching logic framework for verifying parallel imperative programs, establishing its soundness and completeness with respect to operational semantics, and demonstrates its effectiveness through a standard parallel programming example.

Contribution

It introduces the first matching logic approach for parallel imperative language verification, redefining interference concepts and linking semantics with a symbolic verifier.

Findings

The matching logic verifier is sound and complete for PIMP.

Redefinition of 'interference-free' as character parallel rule.

Successful verification of a standard parallel programming problem.

Abstract

Program verification is to develop the program's proof system, and to prove the proof system soundness with respect to a trusted operational semantics of the program. However, many practical program verifiers are not based on operational semantics and can't seriously validate the program. Matching logic is proposed to make program verification based on operational semantics. In this paper, following Grigore Ro{\c{s}}u 's work, we consider matching logic for parallel imperative language(PIMP). According to our investigation, this paper is the first study on matching logic for PIMP. In our matching logic, we redefine "interference-free" to character parallel rule and prove the soundness of matching logic to the operational semantics of PIMP. We also link PIMP's operational semantics and PIMP's verification formally by constructing a matching logic verifier for PIMP which executes rewriting logic semantics symbolically on configuration patterns and is sound and complete to matching logic for PIMP. That is our matching logic verifier for PIMP is sound to the operational semantics of PIMP. Finally, we also verify the matching logic verifier through an example which is a standard problem in parallel programming.