• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering and formal methods >Linearizability and Causality
【24h】

Linearizability and Causality

机译：线性化和因果关系

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

摘要

Most work on the verification of concurrent objects for shared memory assumes sequential consistency, but most multicore processors support only weak memory models that do not provide sequential consistency. Furthermore, most verification efforts focus on the linearizability of concurrent objects, but there are existing implementations optimized to run on weak memory models that are not linearizable. In this paper, we address these problems by introducing causal linearizability, a correctness condition for concurrent objects running on weak memory models. Like linearizability itself, causal linearizability enables concurrent objects to be composed, under weak constraints on the client's behaviour. We specify these constraints by introducing a notion of operation-race freedom, where programs that satisfy this property are guaranteed to behave as if their shared objects were in fact linearizable. We apply these ideas to objects from the Linux kernel, optimized to run on TSO, the memory model of the x86 processor family.
机译：验证共享内存的并发对象的大多数工作都假定顺序一致性，但是大多数多核处理器仅支持不提供顺序一致性的弱内存模型。此外，大多数验证工作都集中在并发对象的线性化上，但是现有的实现已被优化以在不可线性化的弱内存模型上运行。在本文中，我们通过引入因果线性化来解决这些问题，因果线性化是在弱内存模型上运行的并发对象的正确性条件。像线性化本身一样，因果线性化可以使并发对象在客户行为的弱约束下得以组合。我们通过引入操作竞赛自由度的概念来指定这些约束，其中保证满足此属性的程序的行为就好像其共享库实际上是可线性化的一样。我们将这些想法应用于Linux内核中的对象，这些对象经过优化可在TSO（x86处理器系列的内存模型）上运行。

著录项

  • 来源
  • 会议地点 Vienna(AU)
  • 作者

    Simon Doherty; John Derrick;

  • 作者单位

    Department of Computing, University of Sheffield, Sheffield, UK;

    Department of Computing, University of Sheffield, Sheffield, UK;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号