Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models

TL;DR

This paper verifies the correctness and optimizes the implementation of compact NUMA-aware locks on modern weak memory architectures, revealing discrepancies in Linux's lock implementations across different memory models.

Contribution

It provides a detailed verification of the CNA lock algorithm on WMMs and identifies necessary barriers, also analyzing Linux qspinlock's correctness on various architectures.

Findings

Linux qspinlock is incorrect under LKMM but correct on ARMv8 and Power.

Proper barriers are crucial for correctness on WMMs.

The paper offers optimized barrier placement for CNA locks.

Abstract

Developing concurrent software is challenging, especially if it has to run on modern architectures with Weak Memory Models (WMMs) such as ARMv8, Power, or RISC-V. For the sake of performance, WMMs allow hardware and compilers to aggressively reorder memory accesses. To guarantee correctness, developers have to carefully place memory barriers in the code to enforce ordering among critical memory operations. While WMM architectures are growing in popularity, identifying the necessary and sufficient barriers of complex synchronization primitives is notoriously difficult. Unfortunately, publications often consider barriers to be just implementation details and omit them. In this technical note, we report our efforts in verifying the correctness of the Compact NUMA-Aware (CNA) lock algorithm on WMMs. The CNA lock is of special interest because it has been proposed as a new slowpath for Linux qspinlock, the main spinlock in Linux. Besides determining a correct and efficient set of barriers for the original CNA algorithm on WMMs, we investigate the correctness of Linux qspinlock and the latest Linux CNA patch (v15) on the memory models LKMM, ARMv8, and Power. Surprisingly, we have found that Linux qspinlock and, consequently, Linux CNA are incorrect according to LKMM, but are still correct when compiled to ARMv8 or Power.