Hyperproperty-Preserving Register Specifications (Extended Version)

TL;DR

This paper introduces new register specifications that preserve hyperproperties in concurrent systems, enabling reasoning about complex behaviors of various register implementations beyond traditional linearizability.

Contribution

It proposes non-atomic specifications for write strong-linearizable and decisive linearizable registers, facilitating hyperproperty reasoning for these classes.

Findings

Specifications for write strong-linearizable registers enable hyperproperty reasoning.

New class of decisive linearizability includes multi-writer ABD.

Results clarify hyperproperties in crash-resilient message-passing systems.

Abstract

Reasoning about hyperproperties of concurrent implementations, such as the guarantees these implementations provide to randomized client programs, has been a long-standing challenge. Standard linearizability enables the use of atomic specifications for reasoning about standard properties, but not about hyperproperties. A stronger correctness criterion, called strong linearizability, enables such reasoning, but is rarely achievable, leaving various useful implementations with no means for reasoning about their hyperproperties. In this paper, we focus on registers and devise non-atomic specifications that capture a wide-range of well-studied register implementations and enable reasoning about their hyperproperties. First, we consider the class of write strong-linearizable implementations, a recently proposed useful weakening of strong linearizability, which allows more intricate implementations, such as the well-studied single-writer ABD distributed implementation. We introduce a simple shared-memory register specification that can be used for reasoning about hyperproperties of programs that use write strongly-linearizable implementations. Second, we introduce a new linearizability class, which we call decisive linearizability, that is weaker than write strong-linearizability and includes multi-writer ABD, and develop a second shared-memory register specification for reasoning about hyperproperties of programs that use register implementations of this class. These results shed light on the hyperproperties guaranteed when simulating shared memory in a crash-resilient message-passing system.