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.

翻译：互斥锁（即锁）在分离逻辑中已有充分研究，可通过保护不变式或原子性改变锁状态两种方式予以规范。本文针对面向对象语言（如C++与Java）中常见的变体——递归互斥锁，建立了相同范式的规范体系。递归互斥锁允许同一线程多次获取，本文提出的规范统一处理所有获取/释放操作，客户端仅需在访问锁不变式时确认自身是否持有该互斥锁。