• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IEEE Transactions on Parallel and Distributed Systems >Verifying sequential consistency on shared-memory multiprocessors by model checking
【24h】

Verifying sequential consistency on shared-memory multiprocessors by model checking

机译：通过模型检查来验证共享内存多处理器上的顺序一致性

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

摘要

The memory model of a shared-memory multiprocessor is a contract between the designer and the programmer of the multiprocessor. A memory model is typically implemented by means of a cache-coherence protocol. The design of this protocol is one of the most complex aspects of multiprocessor design and is consequently quite error-prone. However, it is imperative to ensure that the cache-coherence protocol satisfies the shared-memory model. We present a novel technique based on model checking to tackle this difficult problem for the important and well-known shared-memory model of sequential consistency. Surprisingly, verifying sequential consistency is undecidable in general, even for finite-state cache-coherence protocols. In practice, cache-coherence protocols satisfy the properties of causality and data independence. Causality is the property that values of read events flow from values of write events. Data independence is the property that all traces can be generated by renaming data values from traces where the written values are pairwise distinct. We show that, if a causal and data independent system also has the property that the logical order of write events to each location is identical to their temporal order, then sequential consistency is decidable. We present a novel model checking algorithm to verify sequential consistency on such systems for a finite number of processors and memory locations and an arbitrary number of data values.
机译：共享内存多处理器的内存模型是多处理器的设计者与程序员之间的约定。通常通过高速缓存一致性协议来实现存储器模型。该协议的设计是多处理器设计最复杂的方面之一，因此很容易出错。但是，必须确保高速缓存一致性协议满足共享内存模型。我们提出一种基于模型检查的新颖技术，以解决重要且众所周知的顺序一致性共享内存模型的这一难题。出乎意料的是，即使对于有限状态缓存一致性协议，通常也无法确定验证顺序一致性。实际上，缓存一致性协议满足因果关系和数据独立性的属性。因果关系是读取事件的值从写入事件的值流动而来的属性。数据独立性是可以通过重命名写入值成对不同的跟踪中的数据值来生成所有跟踪的属性。我们证明，如果一个因果关系和数据无关的系统还具有以下特性：写入每个位置的事件的逻辑顺序与它们的时间顺序相同，那么顺序一致性是可以确定的。我们提出了一种新颖的模型检查算法，以验证此类系统上有限数量的处理器和内存位置以及任意数量的数据值的顺序一致性。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号