Paper Info
Title
Threads as Resource for Concurrency Verification
Abstract
In mainstream languages, threads are first-class in that they can be dynamically created, stored in data structures, passed as parameters, and returned from procedures. However, existing verification systems support reasoning about threads in a restricted way: threads are often represented by unique tokens that can neither be split nor shared. In this paper, we propose \"threads as resource\" to enable more expressive treatment of first-class threads. Our approach allows the ownership of a thread (and its resource) to be flexibly split, combined, and (partially) transferred across procedure and thread boundaries. We illustrate the utility of our approach in handling three problems. First, we use \"threads as resource\" to verify the multi-join pattern, i.e. threads can be shared among concurrent threads and joined multiple times in different threads. Second, using inductive predicates, we show how our approach naturally captures the threadpool idiom where threads are stored in data structures. Lastly, we present how thread liveness can be precisely tracked. To demonstrate the feasibility of our approach, we implemented it in a tool, called ThreadHIP, on top of an existing ParaHIP verifier. Experimental results show that ThreadHIP is more expressive than ParaHIP while achieving comparable verification performance.
Year
DOI
Venue
2015
10.1145/2678015.2682540
PEPM
Keywords
Field
DocType
separation logic,threads as resource,specifying and verifying and reasoning about programs,parallel programming,concurrency verification,first-class threads
Programming language,Computer science,Parallel computing,Java concurrency,Gang scheduling,Thread (computing),Readers–writers problem,Process (computing),Concurrent data structure,Monitor,Green threads
Conference
Citations 
PageRank 
References 
2
0.36
19
Authors
3
Name
Order
Citations
PageRank
Duy-Khanh Le1121.92
Wei-Ngan Chin286863.37
Yong Meng Teo356454.77