• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >To Parallelize or to Optimize?
【24h】

To Parallelize or to Optimize?

机译：并行化还是优化？

获取原文
获取原文并翻译 | 示例
       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Model checking is a popular and successful technique for verifying complex digital systems. Carrying this technique-and its underlying state-space generation algorithms-beyond its current limitations presents itself with a number of alternatives. Our focus is on parallelization which is made attractive by the current trend in hardware architectures towards multi-core, multi-processor systems. The main obstacle in this endeavour is that, in particular, symbolic state-space generation algorithms are notoriously hard to parallelize. In this article, we describe the process of taking a sequential symbolic state-space generation algorithm, namely a generic, symbolic BFS algorithm, through a sequence of optimizations that leads up to the Saturation algorithm and follow the impact these sequential algorithms have on their parallel counterparts. In particular, we develop a parallel version of Saturation, discuss the challenges faced in its design and conduct extensive experimental studies of its implementation. We employ rigorous analysis tools and techniques for measuring and evaluating parallel overheads and the quality of the parallelization. The outcome of these studies is that the performance of a parallel symbolic state-space generation algorithm is almost impossible to predict and highly dependent on the model to which it is applied. In most situations, perceivable speed-ups are hard to achieve, but real-world applications where our technique produces significant improvements do exist. Nevertheless, it appears that time is better invested in optimizing sequential symbolic model checking algorithms rather than parallelizing them.
机译：模型检查是一种用于验证复杂数字系统的流行且成功的技术。超越当前的局限性，采用这项技术及其潜在的状态空间生成算法会给自己带来许多选择。我们专注于并行化，并行化由于当前硬件架构向多核，多处理器系统的发展趋势而变得有吸引力。这项工作的主要障碍是，尤其是众所周知，符号状态空间生成算法很难并行化。在本文中，我们描述了通过一系列优化来采用顺序符号状态空间生成算法（即通用符号BFS算法）的过程，该优化过程导致饱和算法并遵循这些顺序算法对其并行性的影响同行。特别是，我们开发了并行版本的饱和度，讨论了其设计面临的挑战，并对其实施进行了广泛的实验研究。我们采用严格的分析工具和技术来测量和评估并行开销和并行化的质量。这些研究的结果是，并行符号状态空间生成算法的性能几乎是无法预测的，并且高度依赖于所应用的模型。在大多数情况下，很难实现明显的提速，但是确实存在我们的技术可以带来显着改善的实际应用。但是，似乎最好将时间投入到优化顺序符号模型检查算法上，而不是并行化它们。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号