关于弱内存并发的基于SAT/SMT的符号编码的偏序语义
计算机科学中的逻辑
2015-04-02 v1
摘要
并发系统众所周知难以分析，而弱内存架构等技术进步极大地加剧了该问题。这重新引发了将偏序语义作为形式化验证技术理论基础的兴趣。其中，符号技术已被证明在发现并发相关错误方面特别有效，因为它们可以利用高度优化的决策过程（如 SAT/SMT 求解器）。本文给出了关于弱内存并发的基于 SAT/SMT 的符号编码的偏序语义的新基础性结果。特别地，我们给出了一个决策过程的理论基础，该过程能够处理带有最小不动点算子的并发程序片段。此外，我们证明了宽松顺序一致性的某种偏序语义等价于 Alglave 等人提出的三个被广泛研究的弱内存公理的合取。该等价的一个重要后果是，用于有界模型检测的符号编码渐近更小，其偏序约束数量仅为二次，而最先进的三次大小编码为三次。
引用
@article{arxiv.1504.00037,
title = {On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency},
author = {Alex Horn and Daniel Kroening},
journal= {arXiv preprint arXiv:1504.00037},
year = {2015}
}
备注
15 pages, 3 figures