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.

• Type: Conference
• Year: 2010
• Where: ESOP
• Authors: Jan Smans, K. Rustan M. Leino, Peter Müller
• Keywords: Approach Prevents Deadlocks, ESOP 2010, Message Passing, Programming Languages, Useful Concurrency Pattern