基于展开的偏序归约
计算机科学中的逻辑
2015-07-06 v1 编程语言
摘要
偏序归约（POR）与网展开是两种应对由并发引起的状态空间爆炸的替代方法。在本文中，我们提出将两种方法相结合以融合各自的优势。我们首先为抽象执行模型定义了以任意独立性关系为参数的展开语义。在此基础上，我们的主要贡献是一种新颖的无状态 POR 算法，该算法在每个 Mazurkiewicz 踪迹中最多探索一次执行，且总体上可呈指数级减少探索次数，从而实现一种形式的超最优性。此外，我们基于展开的 POR 能够处理非终止执行并融合了状态缓存。在包含忙等待等场景的基准测试中，实验表明，与最先进的 DPOR 相比，执行次数得到了显著减少。
引用
@article{arxiv.1507.00980,
title = {Unfolding-based Partial Order Reduction},
author = {César Rodríguez and Marcelo Sousa and Subodh Sharma and Daniel Kroening},
journal= {arXiv preprint arXiv:1507.00980},
year = {2015}
}
备注
Long version of a paper with the same title appeared on the proceedings of CONCUR 2015