Sciweavers

Share
MEMOCODE
2010
IEEE

Modular verification of synchronization with reentrant locks

8 years 3 months ago
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.
Tevfik Bultan, Fang Yu, Aysu Betin-Can
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where MEMOCODE
Authors Tevfik Bultan, Fang Yu, Aysu Betin-Can
Comments (0)
books