Thread-modular verification of parameterized programs

Abstract

In today’s computing world, multi-threaded programs have become common-place. Their asynchronous execution style makes manual reasoning about their properties intricately hard, if not impossible. Thus, algorithmic tools to verify their proper operation are highly sought after.Often, it is necessary to verify multi-threaded programs not just for a fixed number of concurrent threads: Parameterized programs are composed of an arbitrary, unbounded number of concurrent, infinite-state threads to account for these settings. The challenge for fully-automated analyses is then to show or derive properties that hold for all possible numbers of threads of these programs. More formally, the verification problem becomes universally quantified over the unbounded number of concurrent threads. There exist a few state-of-the-art approaches to parameterized program analysis. These approaches rely on intricate abstractions and complicated proof techniques that impede automation, and thus hamper the adoption of parameterized program analysis in practice. In this thesis, we introduce novel abstraction techniques as an alternative to the existing, heavy proof machinery. Our abstractions leverage thread-modular reasoning to reduce parameterized program analysis to the analysis of sequential programs. Thread-modular reasoning has previously been used to lessen the verification burden for fixed-size concurrent programs. In this thesis, we extend this idea to parameterized pro- grams. The result of our thread-modular abstractions is a sequential program; this abstract program can then be verified by existing powerful proof procedures for sequential programs. Our abstractions are designed such that results on the abstracted, sequential program translate back onto the original parameterized program for any number of concurrent threads. We thus facilitate the re-use of existing verification tools for sequential software and leverage them for our goal of parameterized program verification. Our investigation shows that standard state-of-the-art thread-modular reasoning is too weak to derive meaningful results on parameterized programs. We thus introduce two novel methods for instrumenting thread-modular abstractions with auxiliary counter variables that capture additional information about the state of the original parameterized program. This instrumentation is inspired by counter abstraction, a technique that has previously been successfully used for the analysis of finite-state protocols. In this thesis, we extend this idea to infinite-state software. In particular, in this thesis we introduce automated, push-button verification algorithms to prove both safety and liveness properties of parameterized programs. In addition, we present an automated bound analysis that performs automated complexity analysis of pa- rameterized programs, and apply it to derive and prove – to our knowledge for the first time – time complexity results of widely-used concurrent data structures.