• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>12th International Conference on CONCUR 2001 - Concurrency Theory, 12th, Aug 20-25, 2001, Aalborg, Denmark >Extending Memory Consistency of Finite Prefixes to Infinite Computations
【24h】

Extending Memory Consistency of Finite Prefixes to Infinite Computations

机译：将有限前缀的内存一致性扩展到无限计算

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

摘要

Infinite computations are widely used to model arbitrarily long computations of infinite-state systems. Certain properties have both a finitary version, applying only to finite prefixes of computations, and an infinitary version. It is tempting to verify these properties for finite computations only, and then conclude that the infinitary version of the property holds too. This generalization is sound for safety properties, but to verify non-safety properties "by prefixes", one must justify the generalization step. This paper studies how this can be done for sequential consistency of shared memory protocols. In the related literature, this generalization is sometimes done informally, if at all. We define, independently of any specific shared memory algorithm, sufficient conditions so that sequential consistency can be verified by finite prefixes. These conditions are expected to be satisfied by any reasonable shared memory system, regardless of the consistency model.
机译：无限计算被广泛用于对无限状态系统的任意长的计算进行建模。某些属性既有最终版本（仅适用于有限的计算前缀），也有最终版本。试图仅对有限的计算验证这些属性，然后得出结论，该属性的非限定形式也成立。这种概括对于安全属性是合理的，但是要“通过前缀”验证非安全属性，必须证明概括步骤是正确的。本文研究如何实现共享内存协议的顺序一致性。在相关文献中，这种归纳有时是非正式的（如果有的话）。我们独立于任何特定的共享内存算法定义足够的条件，以便可以通过有限前缀来验证顺序一致性。不论一致性模型如何，任何合理的共享内存系统都有望满足这些条件。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号