Deadlock-free Channels and Locks

9 years 10 months ago
Deadlock-free Channels and Locks
The combination of message passing and locking to protect shared state is a useful concurrency pattern. However, programs that employ this pattern are susceptible to deadlock. That is, the execution may reach a state where each thread in a set waits for another thread in that set to release a lock or send a message. This paper proposes a modular verification technique that prevents deadlocks in programs that use both message passing and locking. The approach prevents deadlocks by enforcing two rules: (0) a blocking receive is allowed only if another thread holds an obligation to send and (1) each thread must perform acquire and receive operations in accordance with a global order. The approach is proven sound and has been implemented in the Chalice program verifier.
Jan Smans, K. Rustan M. Leino, Peter Müller
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where ESOP
Authors Jan Smans, K. Rustan M. Leino, Peter Müller
Comments (0)