FDR3: a parallel refinement checker for CSP
FDR3: a parallel refinement checker for CSP
复制标题
FDR3：CSP 的并行细化检查器
DOI：
10.1007/s10009-015-0377-y
复制
发表时间：
2015
影响因子：
1.5
通讯作者：
Gibson-Robinson T
中科院分区：
文献类型：
--
作者：
Gibson-Robinson T
故障发散精化3(FDR3)是CSP精化检查器FDR2的完全重写，其中包含大量增强功能。在本文中，我们描述了FDR3在高水平上的操作，并对几个更重要的创新进行了详细的描述。FDR3有一种新的并行精化检查算法，该算法能够随着内核数量的增加而实现近乎线性的加速比。该算法不仅在共享内存系统上线性扩展，而且在分布式系统(即集群)上也线性扩展。特别是，本文给出的实验结果表明，与顺序情况相比，FDR3在16核(即1024核)的集群上可以获得超过1000倍的加速比：我们在超级计算机上获得了类似的性能改进，更有趣的是，在商用云计算提供商上也获得了类似的性能改进。我们还给出了将FDR3与相关工具进行比较的实验结果，并表明(据我们所知)FDR3在能够超越主存的界限方面是独一无二的。本文还描述了FDR3用来构造其CSP进程的内部表示的新算法，这是有效地进行模型检查进程代数所要解决的关键问题之一。
Failures divergence refinement 3 (FDR3) is a complete rewrite of the CSP refinement checker FDR2 that incorporates a significant number of enhancements. In this paper, we describe the operation of FDR3 at a high level and give a detailed description of several of the more important innovations. FDR3 has a new parallel refinement-checking algorithm that is able to achieve a near linear speedup as the number of cores increases. This algorithm scales linearly not only on shared-memory systems, but also on distributed systems (i.e. clusters). In particular, this paper presents experimental results that show FDR3 can achieve a speedup factor in excess of 1000 versus the sequential case on a cluster of 64, 16-core machines (i.e. 1024 cores): we obtain similar performance improvements on a supercomputer and, more interestingly, on a commodity cloud computing provider. We also present experimental results that compare FDR3 to related tools, and indicate that (as far as we know) FDR3 is unique in being able to scale beyond the bounds of main memory. This paper also describes the new algorithm that FDR3 uses to construct its internal representation of CSP processes, one of the key problems to solve in order to efficiently model-check process algebras.
登录
查看更多内容
DOI：
10.1007/978-3-642-54862-8_14
发表时间：
2014-04
期刊：
--
影响因子：
--
作者：
G. Lowe
通讯作者：
G. Lowe
DOI：
10.1016/s0167-6423(00)00023-x
发表时间：
2001-05
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
A. Mota;A. Sampaio
通讯作者：
A. Mota;A. Sampaio
通过优先级缓慢抽象
DOI：
10.1007/978-3-642-39698-4_20
发表时间：
2013
期刊：
Formal Methods in Computer Aided Design
影响因子：
--
作者：
A. W. Roscoe;Philippa J. Hopcroft
通讯作者：
Philippa J. Hopcroft
DOI：
--
发表时间：
1989
期刊：
影响因子：
--
作者：
Corporate Inmos Limited
通讯作者：
Corporate Inmos Limited
操作语义的乐趣和利润
DOI：
10.1007/11423348_16
发表时间：
2004
影响因子：
8.4
作者：
M. Goldsmith
通讯作者：
M. Goldsmith