Pattern-based verification for multithreaded programs

Javier Esparza, Pierre Ganty, Tomáš Poch

Research output: Contribution to journalArticlepeer-review

17 Scopus citations

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.

Original languageEnglish
Article number9
JournalACM Transactions on Programming Languages and Systems (TOPLAS)
Volume36
Issue number3
DOIs
StatePublished - 1 Aug 2014

Keywords

  • Algorithms
  • Languages
  • Reliability
  • Verification

Fingerprint

Dive into the research topics of 'Pattern-based verification for multithreaded programs'. Together they form a unique fingerprint.

Cite this