DiVinE Multi-Core - A Parallel LTL Model-Checker
DiVinE Multi-Core - A Parallel LTL Model-Checker
复制标题
DiVinE 多核 - 并行 LTL 模型检查器
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
P. Ročkai
中科院分区：
文献类型：
--
作者：
J. Barnat;L. Brim;P. Ročkai
我们提供了一种用于并行共享内存LTL模型检查和可及性分析的工具。该工具基于使用共享内存专门针对多核和多CPU环境的分布式内存算法重新实现。我们展示了平行算法如何允许该工具利用当代硬件的功率，该硬件基于单个系统中CPU核心数量的增加，而不是增加单个CPU核心的速度。
We present a tool for parallel shared-memory enumerative LTL model-checking and reachability analysis. The tool is based on distributed-memory algorithms reimplemented specifically for multi-core and multi-cpu environments using shared memory. We show how the parallel algorithms allow the tool to exploit the power of contemporary hardware, which is based on increasing number of CPU cores in a single system, as opposed to increasing speed of a single CPU core.