Title: Deadlock-free channels and locks
Authors: Leino, K. Rustan M.
Müller, Peter
Smans, Jan #
Issue Date: 22-Mar-2010
Publisher: Springer-Verlag
Host Document: 19th European Symposium on Programming vol:6012 pages:407-426
Conference: European Symposium on Programming edition:19 location:Paphos, Cyprus date:March 22-26, 2010
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.
ISBN: 978-3-642-11956-9
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
# (joint) last author

Files in This Item:
File Description Status SizeFormat
krml200.pdf Published 216KbAdobe PDFView/Open


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

© Web of science