{'fraction_non_alphanumeric': 0.028985507246376812, 'fraction_numerical': 0.0, 'mean_word_length': 5.364055299539171, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Threads as Resource for Concurrency Verification

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.