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 permission-accounting 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 resources are not re-acquired upon
reentrancy, thus avoiding the introduction of new resources in the
system. To be able to express flexible locking policies, we combine the
verification logic with value-parametrized classes. Verified programs satisfy
the following properties: data race freedom, absence of null-dereferencing and
partial correctness. The verification technique is illustrated on several
examples, including a challenging lock-coupling algorithm.