Title: Deadlock-free channels and locks
Authors: Leino, K. Rustan M.
Müller, Peter
Smans, Jan
Issue Date: Jan-2010
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW573
Abstract: 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.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW573.pdfDocument Published 305KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.