Locality and Singularity for Store-Atomic Memory Models

TL;DR

This paper introduces locality and singularity properties for store-atomic memory models, reducing the complexity of robustness checks and enabling automated verification of concurrent programs under relaxed memory models.

Contribution

It establishes two completeness results, locality and singularity, that simplify robustness verification by focusing on specific minimal violating computations.

Findings

Linear-size translation of robustness to SC-reachability

Automated verification of PGAS algorithms

Outperforms existing tools for TSO robustness checking

Abstract

Robustness is a correctness notion for concurrent programs running under relaxed consistency models. The task is to check that the relaxed behavior coincides (up to traces) with sequential consistency (SC). Although computationally simple on paper (robustness has been shown to be PSPACE-complete for TSO, PGAS, and Power), building a practical robustness checker remains a challenge. The problem is that the various relaxations lead to a dramatic number of computations, only few of which violate robustness. In the present paper, we set out to reduce the search space for robustness checkers. We focus on store-atomic consistency models and establish two completeness results. The first result, called locality, states that a non-robust program always contains a violating computation where only one thread delays commands. The second result, called singularity, is even stronger but restricted to programs without lightweight fences. It states that there is a violating computation where a single store is delayed. As an application of the results, we derive a linear-size source-to-source translation of robustness to SC-reachability. It applies to general programs, regardless of the data domain and potentially with an unbounded number of threads and with unbounded buffers. We have implemented the translation and verified, for the first time, PGAS algorithms in a fully automated fashion. For TSO, our analysis outperforms existing tools.