### 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 language | English (US) |
---|---|

Title of host publication | 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. |

Pages | 155-169 |

Number of pages | 15 |

DOIs | |

State | Published - Nov 9 2009 |

Event | 15th 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 2009 → Mar 29 2009 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 5505 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 15th 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 |
---|---|

Country | United Kingdom |

City | York |

Period | 3/22/09 → 3/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

*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