Understanding Read-Write Wait-Free Coverings in the Fully-Anonymous Shared-Memory Model

TL;DR

This work investigates the fully-anonymous shared-memory model where processors and registers lack any naming. It introduces the notion of group solvability to extend classic tasks to anonymous settings and analyzes the eventual-pattern structure of stable views, proving that stable views form a DAG with a unique source. Leveraging this structure, it gives a wait-free snapshot algorithm using only $N$ registers, then derives adaptive renaming with $N(N+1)/2$ names and an obstruction-free consensus protocol via long-lived snapshots. The results illuminate how anonymity shapes task solvability, demonstrate that a minimal register bound suffices for several fundamental problems, and open questions about atomic snapshots and broader group-solvable tasks in fully-anonymous systems.

Abstract

In the fully-anonymous (shared-memory) model, inspired by a biological setting, processors have no identifiers and memory locations are anonymous. This means that there is no pre-existing agreement among processors on any naming of the memory locations. In this work, we ask fundamental questions about the fully-anonymous model in the hope to obtain a better understanding of the role of naming and anonymity in distributed computing. First, we ask what it means to solve a task under processor anonymity. With tasks such as renaming, the traditional notion obviously does not apply. Instead of restricting ourselves to colorless tasks, we propose using the notion of group solvability, which allows transferring any task to processor-anonymous models. Second, the difficulty with anonymity is that processors can hardly avoid covering and then overwriting each other's writes, erasing information written by their predecessors. To get to the bottom of this phenomenon, we ask what system configurations are stable when processors keep reading and writing ad infinitum. Resolving this question leads us to a wait-free solution to the snapshot task, which then allows us to solve renaming and obstruction-free consensus.

Figures (5)

• Figure 1: The write-scan algorithm in the PlusCal algorithm language. Note that the sequence of steps between any two labels (here the labels are $l0$, line 7, and $l1$, line 12) is executed atomically.
• Figure 2: Infinite execution where $p_2$ and $p_3$ keep writing incomparable sets of values. Steps 5 to 13 repeat forever after step 13. Each step, changes in the post-state are underlined.
• Figure 3: The snapshot algorithm in the PlusCal lamport_pluscal_2009 algorithm language. Each processor outputs its view when it terminates upon reaching level $N$. Note that the sequence of steps between any two labels (here the labels are $write$, line 12, and $scan$, line 17) is executed atomically. The TLC model-checker lamport_specifying_2002 is able to exhaustively explore all 3-processor executions of this algorithm, and it confirms that the algorithm solves the snapshot task wait-free.
• Figure 4: The adaptive renaming algorithm in the PlusCal algorithm language.
• Figure 5: The obstruction-free consensus algorithm in the PlusCal algorithm language. Note that the sequence of steps between any two labels (here the labels are $l0$ and $l1$) is executed atomically.

Theorems & Definitions (27)

• definition 1: Consensus
• definition 2: Snapshot
• definition 3: Adaptive Renaming
• definition 4
• definition 5: The global stabilization time, GST
• definition 6: Stable view
• definition 7: Stable-View Graph
• lemma 1
• proof
• lemma 2