Recursive Mutexes in Separation Logic

TL;DR

This paper extends separation logic to specify recursive mutexes, which can be acquired multiple times by the same thread, providing uniform specifications for their acquire and release operations.

Contribution

It introduces a novel specification framework for recursive mutexes in separation logic, accommodating their recursive acquisition behavior.

Findings

Unified specifications for recursive mutex acquire/release

Applicable to object-oriented languages like C++ and Java

Enhances reasoning about recursive locking in concurrent programs

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.