The complexity of predicting atomicity violations

Azadeh Farzan, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We study the prediction of runs that violate atomicity from a single run, or from a regular or pushdown model of a concurrent program. When prediction ignores all synchronization, we show predicting from a single run (or from a regular model) is solvable in time O(n+k.c k ) where n is the length of the run (or the size of the regular model), k is the number of threads, and c is a constant. This is a significant improvement from the simple O(n k·2 k2)algorithm that results from building a global automaton and monitoring it. We also show that, surprisingly, the problem is decidable for model-checking recursive concurrent programs without synchronizations. Our results use a novel notion of a profile: we extract profiles from each thread locally and compositionally combine their effects to predict atomicity violations. For threads synchronizing using a set of locks , we show that prediction from runs and regular models can be done in time . Notice that we are unable to remove the factor k from the exponent on n in this case. However, we show that a faster algorithm is unlikely: more precisely, we show that prediction for regular programs is unlikely to be fixed-parameter tractable in the parameters by proving it is W[1]-hard. We also show, not surprisingly, that prediction of atomicity violations on recursive models communicating using locks is undecidable.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 15th International Conference, TACAS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc.
Pages155-169
Number of pages15
DOIs
StatePublished - Nov 9 2009
Event15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 - York, United Kingdom
Duration: Mar 22 2009Mar 29 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5505 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009
CountryUnited Kingdom
CityYork
Period3/22/093/29/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The complexity of predicting atomicity violations'. Together they form a unique fingerprint.

  • Cite this

    Farzan, A., & Madhusudan, P. (2009). The complexity of predicting atomicity violations. In Tools and Algorithms for the Construction and Analysis of Systems - 15th International Conference, TACAS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc. (pp. 155-169). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5505 LNCS). https://doi.org/10.1007/978-3-642-00768-2_14