Reference:

J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In Proc. of the 38th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, 2011.

Abstract:

Pattern-based verification checks the correctness of the program executions that follow a given em pattern, a regular expression over the alphabet of program transitions of the form w1*w2*...wn*. For multithreaded programs, the alphabet of the pattern is given by the synchronization operations between threads. We study the complexity of pattern-based verification for em abstracted multithreaded programs in which, as usual in program analysis, conditions have been replaced by nondeterminism (the technique works also for boolean programs). While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs, we show that pattern-based verification is NP-complete for both classes. We then conduct a multiparameter analysis in which we study the complexity in the number of threads, the number of procedures per thread, the size of the procedures, and the size of the pattern. We first show that no algorithm for pattern-based verification can be polynomial in the number of threads, procedures per thread, or the size of the pattern (unless P=NP). Then, using recent results about Parikh images of regular languages and semilinear sets, we present an algorithm exponential in the number of threads, procedures per thread, and size of the pattern, but polynomial in the size of the procedures.

Suggested BibTeX entry:

@inproceedings{EG11,
    author = {J. Esparza and P. Ganty},
    booktitle = {Proc. of the 38th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11},
    title = {Complexity of Pattern-based Verification for Multithreaded Programs},
    year = {2011}
}