Recursive Mutexes in Separation Logic

TL;DR

This paper extends concurrent separation logic to recursive mutexes, addressing the gap where reentrant locks require reasoning that is uniform across locked and unlocked paths. It introduces a fractional handle $\ell \mapsto_q \mathsf{rmutex} \gamma P$ and a per-thread $\mathsf{holds} \gamma t n P$, with $n$ counting reentries, a borrowing rule, and a fixed-argument technique to avoid re-quantification across lock boundaries. The contributions are a formal recursive-mutex specification, a borrowing mechanism that separates access from ownership, and a fixing-arguments approach, demonstrated through verification of C++ concurrency libraries using BRiCk for ISO:2024:IIP. The work enables more natural verification of real-world, reentrant-lock usage and aims to broaden the verified surface of the C++ standard library, with potential impact on practical software engineering and tool support for concurrent reasoning.

Abstract

Mutexes (i.e., locks) are well understood in separation logic, and can be specified in terms of either protecting an invariant or atomically changing the state of the lock. In this abstract, we develop the same styles of specifications for \emph{recursive} mutexes, a common variant of mutexes in object-oriented languages such as C++ and Java. A recursive mutex can be acquired any number of times by the same thread, and our specifications treat all acquires/releases uniformly, with clients only needing to determine whether they hold the mutex when accessing the lock invariant.

Figures (1)

• Figure 1: An example using recursive mutexes.