DocumentCode
177165
Title
Behaviour Inference for Deadlock Checking
Author
Pun, Ka I. ; Steffen, Martin ; Stolz, Volker
Author_Institution
Dept. of Inf., Univ. of Oslo, Oslo, Norway
fYear
2014
fDate
1-3 Sept. 2014
Firstpage
106
Lastpage
113
Abstract
This paper extends our behavioural type and effect system for detecting deadlocks by polymorphism and formalizing type inference (with respect to lock types). Our inference is defined for a simple concurrent, first-order language. From the inferred effects, after suitable abstractions to keep the state space finite, we either obtain the verdict that the program will not deadlock, or that it may deadlock. We show soundness and completeness of the type inference.
Keywords
concurrency control; inference mechanisms; state-space methods; system recovery; behaviour inference; behavioural type; deadlock checking; deadlock detection; first-order language; formalizing type inference; polymorphism type inference; state space finite; Abstracts; Calculus; Context; Inference algorithms; Standards; Syntactics; System recovery; behavioural type system; deadlock checking; polymorphism; unification;
fLanguage
English
Publisher
ieee
Conference_Titel
Theoretical Aspects of Software Engineering Conference (TASE), 2014
Conference_Location
Changsha
Type
conf
DOI
10.1109/TASE.2014.23
Filename
6976575
Link To Document