• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议> >Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
【24h】

Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates

机译：具有协作更新的并发对象的自动线性化证明

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

摘要

An execution containing operations performing queries or updating a concurrent object is linearizable w.r.t an abstract implementation (called specification) iff for each operation, one can associate a point in time, called linearization point, such that the execution of the operations in the order of their linearization points can be reproduced by the specification. Finding linearization points is particularly difficult when they do not belong to the operations's actions. This paper addresses this challenge by introducing a new technique for rewriting the implementation of the concurrent object and its specification such that the new implementation preserves all executions of the original one, and its linearizability (w.r.t. the new specification) implies the linearizability of the original implementation (w.r.t. the original specification). The rewriting introduces additional combined methods to obtain a library with a simpler linearizability proof, i.e., a library whose operations contain their linearization points. We have implemented this technique in a prototype, which has been successfully applied to examples beyond the reach of current techniques, e.g., Stack Elimination and Fetch&Add.
机译：包含执行查询或更新并发对象的操作的执行可线性化，如果每个操作都有一种抽象实现（称为规范），则可以将一个时间点（称为线性化点）关联起来，以使操作按其执行顺序执行线性化点可以由规范复制。当线性化点不属于操作的动作时，找到它们特别困难。本文通过引入一种新技术来重写并发对象及其规范的实现，从而解决了这一挑战，以便新实现保留原始对象的所有执行，并且它的线性化能力（写入新的规范）意味着原始实现的线性化（写了原始规范）。重写引入了附加的组合方法以获得具有更简单的线性化证明的库，即，其操作包含其线性化点的库。我们已经在原型中实现了该技术，该原型已成功应用于超出当前技术范围的示例，例如Stack Elimination和Fetch＆Add。

著录项

  • 来源
    《》|2013年|174-190|共17页
  • 会议地点 Saint Petersburg(RU)
  • 作者

    Cezara Dragoi; Ashutosh Gupta; Thomas A. Henzinger;

  • 作者单位

    Institute of Science and Technology Austria, Klosterneuburg;

    Institute of Science and Technology Austria, Klosterneuburg;

    Institute of Science and Technology Austria, Klosterneuburg;

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

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号