Recursive Mutexes in Separation Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908799145607168 |
|---|---|
| author | Du, Ke Mansky, William Giarrusso, Paolo G. Malecha, Gregory |
| author_facet | Du, Ke Mansky, William Giarrusso, Paolo G. Malecha, Gregory |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_22557 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Recursive Mutexes in Separation Logic Du, Ke Mansky, William Giarrusso, Paolo G. Malecha, Gregory Programming Languages Logic in Computer Science 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. |
| title | Recursive Mutexes in Separation Logic |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2601.22557 |