Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strong Linearizability using Primitives with Consensus Number 2

Hagit Attiya, Armando Castañeda, Constantin Enea

TL;DR

The paper examines whether primitives with consensus number 2 can yield wait-free or lock-free strongly-linearizable implementations of concurrent objects. It develops positive results for objects with consensus number 1 and several 2-consensus objects (via readable test&set, fetch&increment, and sets), and provides a strong impossibility result showing that certain 2-consensus-based implementations would collapse to solving $k$-set agreement, preventing lock-free strong linearizability for some objects (e.g., queues, stacks). The constructions rely on novel uses of atomic snapshots and forward simulations to achieve strong linearizability, while the impossibility arguments connect strong linearizability to agreement problems. Overall, the work maps the potential and limits of achieving strong linearizability from realistic primitives, offering both constructive methods and fundamental barriers with significant implications for concurrent object design and randomized program guarantees.

Abstract

A powerful tool for designing complex concurrent programs is through composition with object implementations from lower-level primitives. Strongly-linearizable implementations allow to preserve hyper-properties, e.g., probabilistic guarantees of randomized programs. However, the only known wait-free strongly-linearizable implementations for many objects rely on compare&swap, a universal primitive that allows any number of processes to solve consensus. This is despite the fact that these objects have wait-free linearizable implementations from read / write primitives, which do not support consensus. This paper investigates a middle-ground, asking 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, as well as relaxed variants thereof.

Strong Linearizability using Primitives with Consensus Number 2

TL;DR

The paper examines whether primitives with consensus number 2 can yield wait-free or lock-free strongly-linearizable implementations of concurrent objects. It develops positive results for objects with consensus number 1 and several 2-consensus objects (via readable test&set, fetch&increment, and sets), and provides a strong impossibility result showing that certain 2-consensus-based implementations would collapse to solving -set agreement, preventing lock-free strong linearizability for some objects (e.g., queues, stacks). The constructions rely on novel uses of atomic snapshots and forward simulations to achieve strong linearizability, while the impossibility arguments connect strong linearizability to agreement problems. Overall, the work maps the potential and limits of achieving strong linearizability from realistic primitives, offering both constructive methods and fundamental barriers with significant implications for concurrent object design and randomized program guarantees.

Abstract

A powerful tool for designing complex concurrent programs is through composition with object implementations from lower-level primitives. Strongly-linearizable implementations allow to preserve hyper-properties, e.g., probabilistic guarantees of randomized programs. However, the only known wait-free strongly-linearizable implementations for many objects rely on compare&swap, a universal primitive that allows any number of processes to solve consensus. This is despite the fact that these objects have wait-free linearizable implementations from read / write primitives, which do not support consensus. This paper investigates a middle-ground, asking 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, as well as relaxed variants thereof.
Paper Structure (12 sections, 17 theorems, 1 figure, 2 algorithms)

This paper contains 12 sections, 17 theorems, 1 figure, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Strongly-linearizable implementations of objects with consensus number 1
  4. Max register
  5. Atomic snapshots
  6. Simple Types
  7. Strongly-linearizable implementations of objects with consensus number 2
  8. Readable multi-shot test&set
  9. Fetch&Increment
  10. Sets
  11. Impossibility of strongly-linearizable implementation from 2-consensus objects
  12. Discussion

Key Result

Theorem 1

There is a wait-free strongly-linearizable implementation of a max register using fetch&add.

Figures (1)

  • Figure 1: Summary of our constructions: objects with consensus number 2 appear in orange while objects with consensus number 1 appear in yellow; solid arrows indicate wait-free implementations, while dashed arrows indicate lock-free implementations.

Theorems & Definitions (29)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • proof
  • Theorem 4
  • Theorem 5
  • proof
  • Theorem 6
  • proof
  • Corollary 7
  • ...and 19 more