Hyperproperty-Preserving Register Specifications (Extended Version)
Yoav Ben Shimon, Ori Lahav, Sharon Shoham

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
