自然简化的 soundness 检查复杂度研究（扩展版）
编程语言
2026-05-14 v1
摘要
reduction 的验证代表了参数并发程序正确性证明中交叉组合的子集。我们引入一种表达式丰富的语法简化类，称为自然简化 (natural reductions)。自然简化通过在参数化程序的线程模板中引入原子块和全局 rendezvous 点来指定。我们研究决定给定自然简化是否在给定（半）交换关系下具有 soundness 的问题。在线程之间不存在同步的情况下，我们提出了一种正确且在多项式时间内完成的算法。在考虑同步的情况下，我们提供了一个通用的下界（取决于同步机制的大小），并显示对于像锁定这样的简单机制，问题已是 coNP-hard。
引用
@article{arxiv.2605.13780,
title = {On the Complexity of Checking Soundness of Natural Reductions (Extended Version)},
author = {Constantin Enea and Azadeh Farzan and Dominik Klumpp},
journal= {arXiv preprint arXiv:2605.13780},
year = {2026}
}
备注
31 pages, extended version (with proofs) of the paper accepted at CAV'26