Reasoning about Java's Reentrant Locks

This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permissionaccounting separation logic. As usual, each lock is associated with a resource invariant, i.e., when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that re

• Type: Conference
• Year: 2008
• Where: APLAS
• Authors: Christian Haack, Marieke Huisman, Clément Hurlin
• Keywords: APLAS 2008, Concurrent Java-like Language, Programming Languages, Reentrant Locks, Verification Technique