  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.
