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.

翻译：归约（交互交错的代表性子集）的验证简化了参数化并发程序的正确性证明。我们引入了一类表达力丰富的句法归约，称之为自然归约。自然归约通过在参数化程序的线程模板中引入原子块和全局会合点来指定。我们研究了判断给定自然归约相对于给定（半）交换关系是否合理的问题。在线程间无同步的情况下，我们提出了一种完备的多项式时间算法。在考虑同步的情况下，我们给出了该问题的一般下界（参数化于同步机制），并证明即使对于锁定这样的简单机制，该问题也已是coNP-难的。