Threads As Resource For Concurrency Verification
PEPM(2015)
摘要
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.
更多查看译文
关键词
Threads as Resource,Concurrency Verification,First-class Threads,Separation Logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络