Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-319-02444-8_21
Title: An expressive framework for verifying deadlock freedom
Authors: Le, D.-K.
Chin, W.-N. 
Teo, Y.-M. 
Keywords: Concurrency
Deadlock
Specification
Verification
Issue Date: 2013
Source: Le, D.-K.,Chin, W.-N.,Teo, Y.-M. (2013). An expressive framework for verifying deadlock freedom. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8172 LNAI : 287-302. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-319-02444-8_21
Abstract: This paper presents an expressive specification and verification framework for ensuring deadlock freedom of shared-memory concurrent programs that manipulate locks. We introduce a novel delayed lockset checking technique to guarantee deadlock freedom of programs with interactions between thread and lock operations. With disjunctive formulae, we highlight how an abstraction based on precise lockset can be supported in our framework. By combining our technique with locklevels, we form a unified formalism for ensuring deadlock freedom from (1) double lock acquisition, (2) interactions between thread and lock operations, and (3) unordered locking. The proposed framework is general, and can be integrated with existing specification logics such as separation logic. Specifically, we have implemented this framework into a prototype tool, called ParaHIP, to automatically verify deadlock freedom and correctness of concurrent programs against user-supplied specifications. © 2013 Springer International Publishing.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/78013
ISBN: 9783319024431
ISSN: 03029743
DOI: 10.1007/978-3-319-02444-8_21
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

2
checked on Feb 20, 2018

Page view(s)

20
checked on Feb 16, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.