多核环境下BDD操作的高效可达性分析与模型检查

"这篇论文探讨了在多核处理器环境下对BDD（Binary Decision Diagrams，二进制决策图）操作的并行化处理，以优化可达性分析和模型检查的性能。作者提出了一种无锁哈希表和无锁记忆表的实现，名为Sylvan的多核BDD包，并在48核机器上展示了其在模型检查器LTSmin中的应用，实现了超过30倍的加速比。此外，他们还改进了符号可达性算法，减少内存需求高达40%。" 正文: 在计算机科学中，二进制决策图（BDD）是一种用于表示和操作布尔函数的有效数据结构。它们在形式验证，特别是在模型检查中扮演着关键角色。模型检查是一种自动验证技术，用于确定给定系统是否满足特定的属性。在模型检查中，可达性分析是核心部分，它确定从初始状态出发，通过系统转换所能达到的所有可能状态。 传统的可达性分析在处理大型系统时面临挑战，因为存储所有状态所需的内存可能会迅速增长。针对这一问题，论文作者提出了针对多核硬件的并行BDD操作，旨在提升性能。过去的尝试通常侧重于并行执行多个独立的BDD操作，而本文则专注于并行化BDD操作本身，以克服共享内存中的通信成本难题。 为了解决这个问题，研究者扩展了无锁哈希表，使其能够支持BDD操作和垃圾收集。无锁数据结构允许并发访问，减少了对锁定的需求，从而减少了潜在的冲突和同步开销。同时，他们实现了一种名为Wool的工作窃取框架，进一步支持了并行计算。结合这些技术，他们开发了Sylvan，一个专门针对多核环境设计的BDD库。 在实际应用中，Sylvan被集成到模型检查器LTSmin中，用于测试其在BEEM模型数据库中几个模型的可达性算法的性能。实验结果显示，某些模型在48核机器上的运行时间得到了显著缩短，加速比超过了30倍，这标志着在并行化BDD操作上的一个重要突破。 此外，作者还改进了符号可达性算法。通过修改BDD操作，他们能够在单个步骤中完成关系乘积和变量替换，提高了算法效率，并降低了内存需求最高达40%。这些改进不仅加快了可达性分析的速度，而且减轻了内存压力，这对于处理大型系统来说尤其重要。 关键词涵盖了多核计算、BDD操作、符号可达性、并行模型检查、无锁数据结构、垃圾收集、LTSmin、WOOL以及Sylvan。这项工作的贡献在于提供了一种有效的方法，以应对模型检查中对大规模系统的分析，特别是在资源有限的多核环境中。通过无锁数据结构和优化的算法，该研究为未来的形式验证工具和方法提供了重要的理论基础和实践指导。