Pattern-based verification for multithreaded programs

Abstract

Pattern-based verification checks the correctness of program executions that follow a given pattern, a regular expression over the alphabet of program transitions of the form w∗1. . . w∗n. For multithreaded programs, the alphabet of the pattern is given by the reads and writes to the shared storage. We study the complexity of pattern-based verification for multithreaded programs with shared counters and finite variables. While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs (even without counters), we show that pattern-based verification is NP-complete for both classes, even in the presence of counters.We then conduct a multiparameter analysis to study the complexity of the problem on its three natural parameters (number of threads+counters+variables, maximal size of a thread, size of the pattern) and on two parameters related to thread structure (maximal number of procedures per thread and longest simple path of procedure calls). We present an algorithm that for a fixed number of threads, counters, variables, and pattern size solves the verification problem in stO(lsp+[log(pr+1)]) time, where st is the maximal size of a thread, pr is the maximal number of procedures per thread, and lsp is the longest simple path of procedure calls.