On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
For researchers in formal verification of concurrent programs, this paper provides complexity results for a new class of reductions, but the results are incremental as they extend known techniques.
The paper introduces natural reductions for verifying parameterized concurrent programs and studies the complexity of checking their soundness. It presents a polynomial-time algorithm for the unsynchronized case and shows coNP-hardness for simple synchronization mechanisms like locking.
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.