On the Complexity of Checking Soundness of Natural Reductions (Extended Version)

TL;DR

This paper studies the complexity of verifying the soundness of natural reductions in concurrent programs, providing efficient algorithms for some cases and complexity bounds for others.

Contribution

It introduces natural reductions with atomic blocks and rendezvous points, and analyzes the computational complexity of checking their soundness.

Findings

Polynomial-time algorithm for soundness without synchronization

Lower bounds and coNP-hardness results with synchronization mechanisms

Abstract

The verification of reductions, representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syntactic reductions, which we call natural reductions. Natural reductions are specified by introducing atomic blocks and global rendezvous points in the parameterized program's thread template. We study the problem of deciding whether a given natural reduction is sound wrt. a given (semi-)commutativity relation. In the case that there is no synchronization between threads, we present a sound and complete polynomial-time algorithm. In the case where synchronization is considered, we provide a general lower bound for the problem (parametric in the synchronization mechanism), and show that the problem is coNP-hard already for a simple mechanism like locking.