Hyperproperty-Preserving Register Specifications (Extended Version)

TL;DR

The paper addresses the challenge of verifying hyperproperties for concurrent shared-memory registers, where standard linearizability preserves safety but not hyperproperties. It introduces two complete, non-atomic specifications, $WSR$ (Write Strong Register) and $DR$ (Decisive Register), to capture a broad class of implementations and enable hyperproperty reasoning; it proves forward simulations from write-strongly-linearizable implementations to $WSR$, and from multi-writer $ olinebreak[4]{ ext{ ormalsize ABD}}$-style implementations to $DR$, establishing a refinement-based framework for hyperproperty preservation. The work shows that $WSR$ is complete for write-strongly-linearizable registers and that $DR$ is complete for a wider family (including multi-writer $ ext{ABD}$), thereby enabling tractable verification of hyperproperties in crash-resilient shared-memory simulations. These results clarify which hyperproperties are guaranteed when simulating shared memory in crash-resilient message-passing systems and provide practical, automatable tools for reasoning about complex register implementations. Overall, the paper advances the theoretical understanding and practical verification of hyperproperties in concurrent systems by connecting forward simulations to hyperproperty preservation through tailored, complete specifications.

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.

Figures (3)

• Figure 2: Client programs (upper part) and corresponding trace sets (lower part) that, if an adversary can generate them, violate the hyperproperty "$a=b$ with probability $\frac{1}{2}$"
• Figure 3: Atomic ($\mathtt{ATR}\xspace$)
• Figure 4: Summary of examples