Scholarlink

<p>When a concrete concurrent object <i>refines</i> another, more abstract object, the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This approach is sound for <i>trace properties</i> of the program, but not for <i>hyperproperties</i>, including many security properties and probability distributions of events. We define <i>strong observational refinement</i>, a strengthening of refinement that preserves hypersafety properties, and prove that it is <i>equivalent</i> to the existence of <i>forward simulations</i>. We show that strong observational refinement generalizes <i>strong linearizability</i>, a restriction of <i>linearizability</i>, the prevalent consistency condition for implementing concurrent objects. Our results imply that strong linearizability is also equivalent to existence of forward simulations, and show that strongly linearizable implementations can be composed both horizontally and vertically. This paper also investigates whether there are wait-free strongly-linearizable implementations from realistic primitives such as test&amp;set or fetch&amp;add, whose consensus number is 2. We show that many objects with consensus number 1 have wait-free strongly-linearizable implementations from fetch&amp;add. We also show that several objects with consensus number 2 have wait-free or lock-free implementations from other objects with consensus number 2. In contrast, we prove that even when fetch&amp;add, swap and test&amp;set primitives are used, some objects with consensus number 2 do not have lock-free strongly-linearizable implementations. This includes queues and stacks, and relaxed variants thereof.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Preserving hyperproperties of programs using primitives with consensus number 2

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年8月6日

查看全文
  • Hagit Attiya,
  • Armando Castañeda,
  • Constantin Enea

摘要

When a concrete concurrent object refines another, more abstract object, the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This approach is sound for trace properties of the program, but not for hyperproperties, including many security properties and probability distributions of events. We define strong observational refinement, a strengthening of refinement that preserves hypersafety properties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability, a restriction of linearizability, the prevalent consistency condition for implementing concurrent objects. Our results imply that strong linearizability is also equivalent to existence of forward simulations, and show that strongly linearizable implementations can be composed both horizontally and vertically. This paper also investigates whether there are wait-free strongly-linearizable implementations from realistic primitives such as test&set or fetch&add, whose consensus number is 2. We show that many objects with consensus number 1 have wait-free strongly-linearizable implementations from fetch&add. We also show that several objects with consensus number 2 have wait-free or lock-free implementations from other objects with consensus number 2. In contrast, we prove that even when fetch&add, swap and test&set primitives are used, some objects with consensus number 2 do not have lock-free strongly-linearizable implementations. This includes queues and stacks, and relaxed variants thereof.