Modular verification of synchronization with reentrant locks

We present a modular approach for verification of synchronization behavior in concurrent programs that use reentrant locks. Our approach decouples the verification of the lock implementation from the verification of the threads that use the lock. This decoupling is achieved using lock interfaces that characterize the allowable execution order for the lock operations. We use a thread modular verification approach to check that each thread obeys the lock interface. We verify the lock implementation assuming that the threads behave according to the lock interface. We demonstrate that this approach can be used to verify synchronization behavior in Java programs that use reentrant lock implementations for synchronization.